If A and B are cpos, the set of continuous functions A \twoheadrightarrow B is a cpo under the pointwise ordering: f \sqsubseteq g\;\; \text {iff}\;\; \forall a \in A.\ f(a) \sqsubseteq g(a) The intuition of this ordering in terms of information is that we increase the information content of a function overall by increasing the information content of any (or many) argument values. To prove this, we must show:

1. A \twoheadrightarrow B has a least element. \bot _{A \twoheadrightarrow B} is the constant function that returns \bot _B, i.e. \lambda a.\ \bot _B.
2. \bigsqcup X exists for all directed X \subseteq A \twoheadrightarrow B. Our lub of a set of continuous functions \bigsqcup X is the function \Phi where: \Phi (a) = \bigsqcup \{ f(a) \mid f \in X\} We must show a number of properties of this lub \Phi . Specifically:
   1. \bigsqcup \{ f(a) \mid f \in X\} exists in B.

      Proof.

      • Liam O'Connor

      We want to show that the set \{ f(a) \mid f \in X\} is directed. Take two values g(a), h(a) \in \{ f(a) \mid f \in X\}. Since X is directed, there exists a function k \in X such that g \sqsubseteq k and h \sqsubseteq k. By applying the definition of \sqsubseteq for functions above, we have g(a) \sqsubseteq k(a) and h(a) \sqsubseteq k(a). Thus k(a) is an upper bound of these two values g(a), h(a), and thus \{ f(a) \mid f \in X\} is directed, and thus its lub exists since B is a cpo.
   2. \Phi (a) = \bigsqcup \{ f(a) \mid f \in X \} is continuous.

      Proof.

      • Liam O'Connor

      Using the alternative characterisation of continuity

      \begin {array}{lclr} \Phi (\bigsqcup Y) &=& \bigsqcup \{ f(\bigsqcup Y) \mid f \in X \} & \text {(defn. $\Phi $)}\\ & = & \bigsqcup \{\bigsqcup \{ f(y) \mid y \in Y \} \mid f \in X \} & \text {($f$ is continuous)}\\ & = & \bigsqcup \{\bigsqcup \{ f(y) \mid f \in X \} \mid y \in Y \} & \text {(swap lubs)}\\ & = & \bigsqcup \{ \Phi (y) \mid y \in Y \} & \text {(defn. $\Phi $)}\\ \end {array} Monotonicity is similar to prove.
   3. \Phi is an upper bound for X \subseteq A \twoheadrightarrow B.

      Proof.

      • Liam O'Connor

      Let g \in X. Then for any a \in A we have g(a) \in \{ f(a) \mid f \in X\}. Now, by 2a and lubs, we have g(a) \sqsubseteq \bigsqcup \{ f(a) \mid f \in X \}, which by the definition of \Phi gives g(a) \sqsubseteq \Phi (a). Hence, by the definition of \sqsubseteq on functions, we can conclude g \sqsubseteq \Phi .
   4. \Phi is the least upper bound for X.

      Proof.

      • Liam O'Connor

      Let g \in A \twoheadrightarrow B be an upper bound for X \subseteq A \twoheadrightarrow B. Then (using \sqsubseteq on functions) g(a) is an upper bound for \{f(a) \mid f \in X\} for all a \in A. Now, by 2a and lubs, we have \bigsqcup \{f(a) \mid f \in X\} \sqsubseteq g(a), i.e. \Phi (a) \sqsubseteq g(a), which, by the definition of \sqsubseteq on functions, allows us to conclude \Phi \sqsubseteq g.

At each step "upwards" on this cpo, one arrow that ends in \bot now points to a non-\bot value (moving up the cpo \mathbb {B}_\bot ).

For the \twoheadrightarrow operator on cpos (Definition [dt-002F]) to be the object mapping for a bifunctor \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo} like \times is (see Corollary [dt-002C]), we would need to define a morphism mapping f \twoheadrightarrow g that, given two functions f : A \twoheadrightarrow B and g : C \twoheadrightarrow D, gives a function (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D). But such a function is not implementable: \begin {array}{l} f \twoheadrightarrow g : (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D) \\ (f \twoheadrightarrow g)(h)(b) =\ \textcolor {red}{???}\\ \end {array} In the above hole \textcolor {red}{???}, h : A \twoheadrightarrow C and b \in B. Given the value b \in B, none of our functions f, g or h take elements of B, so there would be no way to produce the D value required. This is because our function f : A \twoheadrightarrow B goes the wrong way. If f were a function B \twoheadrightarrow A, things would be a lot easier.

The dual of a category \mathbf {C}, written \mathbf {C}^\mathsf {op}, is a category with the same objects as \mathbf {C} but the arrows are reversed, that is, for each morphism A \xrightarrow {m} B in \mathbf {C}, there is a morphism B \xrightarrow {m} A in \mathbf {C}^\mathsf {op}.

The operator \twoheadrightarrow introduced in Definition [dt-002F] is is the object mapping for a binary functor: (\twoheadrightarrow ) : \mathbf {Cpo}^\mathsf {op} \times \mathbf {Cpo} \rightarrow \mathbf {Cpo} The category \mathbf {Cpo}^\mathsf {op} is the dual category to \mathbf {Cpo}.

Thus, a morphism A \xrightarrow {m} B in the category \mathbf {Cpo}^\mathsf {op} is a continuous function m : B \twoheadrightarrow A. Thus, the morphism mapping for our functor must take two functions f : B \twoheadrightarrow A (the morphism from \mathbf {Cpo}^\mathsf {op}) and g : C \twoheadrightarrow D (the morphism from \mathbf {Cpo}), and produce (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D). As with products, we will overload the \twoheadrightarrow notation for this mapping as well.