Generalising to \textbf {Cpo}^\textbf {R} [dt-005A]
All of our other notions for \textbf {Cpo} naturally generalise to a setting with retraction pairs \textbf {Cpo}^\textbf {R}: least elements, \omega -chains, upper bounds, colimits, cocontinuous endofunctors and so on.
Definition\omega -chains of cpos in the category \mathbf {Cpo}^\textbf {R} [dt-005C]
An \omega -chain of cpos in the category \mathbf {Cpo}^\textbf {R} consists of a family of cpos \{D_i \mid i \in \mathbb {N} \}, together with a family of retraction pairs D_i \xtofrom [g_i]{f_i} D_{i+1}, shown below:
DefinitionEndofunctors on \textbf {Cpo}^\textbf {R} [dt-005D]
An endofunctor on the category \textbf {Cpo}^\textbf {R} is a functor \textbf {Cpo}^\textbf {R} \rightarrow \textbf {Cpo}^\textbf {R}, i.e. a mapping \mathcal {F} on cpos together with a mapping \mathcal {F} on retraction pairs, such that:
- If (f,g) is a retraction pair A \xtofrom [g]{f} B then \mathcal {F}(f,g) is a retraction pair \mathcal {F}(A)\xtofrom []{} \mathcal {F}(B)
- \mathcal {F}(\mathsf {id}_A : A\xtofrom []{} A) = \mathsf {id}_{\mathcal {F}(A)} : \mathcal {F}(A)\xtofrom []{} \mathcal {F}(A)
- \mathcal {F}(f \circ g) = \mathcal {F}(f) \circ \mathcal {F}(g) (where \circ is composition of retraction pairs)
DefinitionUpper bounds in the category \mathbf {Cpo}^\mathbf {R} [dt-005G]
A cpo A is an upper bound of an \omega -chain of cpos A_i in the category \mathbf {Cpo}^\textbf {R} if there is a family of retraction pairs A_i \xtofrom [g_i]{f_i} A such that the following diagram commutes (i.e. for all i \in \mathbb {N}, (f_i, g_i) = (f_{i+1},g_{i+1}) \circ (s_i,t_i), where \circ is composition of retraction pairs):
DefinitionColimits in the category \mathbf {Cpo}^\mathbf {R} [dt-005F]
A cpo A is the colimit of an \omega -chain of cpos A_i if is both an upper bound, i.e. there exists retraction pairs (f_i,g_i) : A_i \xtofrom []{} A, and for any other upper bound B, for which there will exist retraction pairs (m_i,n_i) : A_i \xtofrom []{} B, there exists a unique retraction pair A \xtofrom [k']{k} B such that (m_i,n_i) = (k,k') \circ (f_i,g_i) for all i \in \mathbb {N}, where \circ is composition of retraction pairs. Viewed diagramatically, it is the same as Definition [dt-004S] where continuous functions are replaced by retraction pairs.
DefinitionCocontinuous endofunctors on \textbf {Cpo}^\textbf {R} [dt-005E]
An endofunctor \mathcal {F} is cocontinuous iff it preserves colimits of \omega -chains of cpos. That is, given a chain where A is a colimit: