Consider the Haskell-style data type:
\textbf {data}\ \mathit {Bin} = \mathsf {Zero}\ \mathit {Bin} \mid \mathsf {Empty} \mid \mathsf {One}\ \mathit {Bin}
So, e.g. \mathsf {One}\ (\mathsf {Zero}\ (\mathsf {One}\ \mathsf {Empty})) : \mathit {Bin} .
The recursive domain equation is, expressed as a fixed point:
B \simeq \mathcal {F}(B)\quad \text {where}\ \mathcal {F}(X) = X + \mathbf {1} + X
We wish to show that \mathcal {F} is a cocontinuous endofunctor
We have a mapping \mathcal {F} on cpos the category \textbf {Cpo} functor \mathcal {F} on continuous functions the category \textbf {Cpo}
Recalling our sum construction bifunctor \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo} (Theorem [dt-0038] continuous functions \mathcal {F} can be derived from our mapping on cpos \mathcal {F} by using the morphism mapping from the sum construction (Definition [dt-0037] f : A \twoheadrightarrow B , our morphism mapping is:
\begin {array}{l}
\mathcal {F}(f) : \mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B)\\
\mathcal {F}(f) \triangleq f + \mathsf {id}_\textbf {1} + f
\end {array}
Proof that this endofunctor cocontinuous \mathit {Bin} , i.e. \llbracket \mathit {Bin} \rrbracket : \textbf {Cpo} is the least fixed point of \mathcal {F} , i.e. the colimit \omega -chain
Let us visualise this chain. Here the sum injections have been written as \textsf {Z, E, O} rather than (combinations of) \textsf {inl} and \textsf {inr} to keep the connection with the Haskell data type clear.
Thus, the n th cpo in the chain contains binary numbers with at most n defined digits. The colimit