Locality of sums [dt-0039]

Liam O'Connor

We can see by the definitions of case and our constructors that $[f,g] \circ \mathit {inl} = f$ and $[f,g] \circ \mathit {inr} = g$ , or, in a commutative diagram:

Note that this diagram is like the dual of the diagram seen in the universal property for products — the arrows are reversed. That is because, generally speaking, sums are dual to products. However, because of our additional $\bot$ value, our cpo sums are only weakly universal — the $h$ arrow is not unique.

ExampleWeak universality of cpo sums [dt-003A]

Liam O'Connor

Consider this scenario with the cpos $\textbf {2} = \{ \top , \bot \}$ and $\textbf {1} = \{\bot \}$ :

In this case, setting the function

h = \lambda x.\ \top

makes the diagram commute, but

(\lambda x.\ \top ) \neq [\lambda x.\ \top , \lambda x.\ \top ]

due to the different handling of

\bot _{\textbf {1}+\textbf {1}}

DefinitionWeak universal property for cpo sums [dt-003B]

Liam O'Connor

(h \circ \mathit {inl} = f \land h \circ \mathit {inr} = g)\;\; \text {iff}\;\; [f,g] \sqsubseteq h

This property is called weak because it uses only the information ordering rather than equality on the right hand side.

WarningFailure of sum isomorphisms [dt-003C]

Liam O'Connor

The weakness of the universal property for sums means that many common isomorphisms for sums in other contexts do not hold:

$A + (B + C) \not \simeq (A + B) + C$
$(A \twoheadrightarrow C) \times (B \twoheadrightarrow C) \not \simeq (A+B) \twoheadrightarrow C$