Construction. Sum of cpos [dt-0031]

The sum construct on cpo A + B denotes a disjoint union of two cpos with a new, dedicated \bot value: A + B = \{ (0, a) \mid a \in A \} \cup \{ (1, b) \mid b \in B \} \cup \{ \bot _{A+B} \} This construct is a cpo under the ordering: x \sqsubseteq y\;\;\text {iff}\;\;\begin {cases} \text {true} & \text {if}\ x=\bot _{A+B}\\ a \sqsubseteq a' & \text {if}\ x = (0,a)\ \text {and}\ y = (0, a') \\ b \sqsubseteq b' & \text {if}\ x = (1,b)\ \text {and}\ y = (1, b') \\ \text {false} & \text {otherwise} \end {cases} Intuitively, this says that the ordering on A + B is the same as A and B separately, except that \bot _{A+B} is less than anything.

The only directed sets are those that do not contain a mixture of elements from both A and from B, so the least upper bound operator is essentially the same as the least upper bounds for A and for B. Formally: \bigsqcup X \;\; = \;\; \begin {cases} (0,\bigsqcup \{ a \mid (0,a) \in X \}) & \text {if}\ \{ a \mid (0,a) \in X \} \neq \emptyset \\ (1,\bigsqcup \{ b \mid (1,b) \in X \}) & \text {if}\ \{ b \mid (1,b) \in X \} \neq \emptyset \\ \bot _{A+B} & \text {otherwise}\\ \end {cases}