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

Liam O'Connor

If $\mathcal {F}$ is a mapping on cpos built up from basic cpos using the constructions $\times$ , $\otimes$ , $+$ , $\oplus$ , $(\cdot )_\bot$ , as well as $\twoheadrightarrow$ and $\mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }$ , then $\mathcal {F}$ extends to a (covariant!) cocontinuous functor on $\textbf {Cpo}^\mathbf {R}$ . We shall detail the construction for products and functions here, but the other constructions are all similar.

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

Liam O'Connor

Given two retraction pairs $(f,g)$ and $(h,i)$ , our retraction pair for their product is just the product of their embedding and projection, i.e. $(f \times h, g \times i)$ , using our product operation on continuous functions: $\dfrac {A \xtofrom [g]{f} B\quad C \xtofrom [i]{h} D}{A\times C \xtofrom [g \times i]{f \times h} B \times D}$

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

Liam O'Connor

We are given two retraction pairs $A \xtofrom [g]{f} B$ and $C \xtofrom [i]{h} D$ . To define a suitable covariant functor, we define our morphism mapping in terms of our $\twoheadrightarrow$ operation on continuous functions: $(f,g) \twoheadrightarrow (h,i) \; \triangleq \; (g\twoheadrightarrow h, f \twoheadrightarrow i)$ Note that the positions of $f$ and $g$ are swapped in the above definition. $\dfrac {A \xtofrom [g]{f} B \quad C \xtofrom [i]{h} D}{A \twoheadrightarrow C \xtofrom [f \twoheadrightarrow i]{g \twoheadrightarrow h} B \twoheadrightarrow D}$ Unlike with the category $\textbf {Cpo}$ , this functor is not contravariant but covariant: Note the positions of $A$ and $B$ are not swapped!