Definition. The category $\textbf {Cpo}^\textbf {R}$ [dt-0058]

Liam O'Connor

The category $\textbf {Cpo}^\textbf {R}$ is the category where the objects are cpos, the morphisms are retraction pairs, composition is as in Definition [dt-0056] and identity is just the retraction pair $A \xtofrom [\lambda x. x]{\lambda x. x} A$ .

Definition. The category $\textbf {Cpo}^\textbf {R}$ [dt-0058]

Problem. Contravariance in the function arrow [dt-0053]

Exercise. [dt-005O]

Solution.

Definition. Retraction pair [dt-0054]

Example. Examples and counterexamples of retraction pairs [dt-0055]

Definition. Composition of retraction pairs [dt-0056]

Corollary. Derived products of retraction pairs [dt-0057]

Definition. The category $\textbf {Cpo}^\textbf {R}$ [dt-0058]

Definition. Information ordering in $\textbf {Cpo}^\textbf {R}$ [dt-0059]

Generalising to $\textbf {Cpo}^\textbf {R}$ [dt-005A]

Definition. $\omega$ -chains of cpos in the category $\mathbf {Cpo}^\textbf {R}$ [dt-005C]

Definition. Endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005D]

Definition. Upper bounds in the category $\mathbf {Cpo}^\mathbf {R}$ [dt-005G]

Definition. Colimits in the category $\mathbf {Cpo}^\mathbf {R}$ [dt-005F]

Definition. Cocontinuous endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005E]

Extending cpo Mappings to endofunctors on $\textbf {Cpo}^\mathbf {R}$ [dt-005I]

Definition. $\times$ operation for retraction pairs [dt-005J]

Definition. $\twoheadrightarrow$ operation for retraction pairs [dt-005K]

Theorem. Fixed point theorem for endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005B]

Construction. The colimit $D^\infty$ [dt-005H]

Proof.


( $y \mapsto b \mapsto z$ but $z \not \sqsubseteq y$ )	( $b \mapsto x \mapsto a$ but $a \neq b$ )