Remark. Why the function arrow is not a covariant bifunctor [dt-002V]
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.