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.

DefinitionMorphism mapping for \twoheadrightarrow [dt-002X]

• Liam O'Connor

Given f : B \twoheadrightarrow A and g : C \twoheadrightarrow D, we have: \begin {array}{l} f \twoheadrightarrow g : (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D)\\ f \twoheadrightarrow g = \mathit {curry}\ (g \circ \mathit {apply} \circ (\mathsf {id} \times f))\\[2em] \text {(or, operationally:)}\\ (f \twoheadrightarrow g)(h) = g \circ h \circ f\\ \end {array}

Theorem [dt-002Y]

• Liam O'Connor

The two functor laws follow as a consequence of the universal property for functions:

1. \mathsf {id}_A \twoheadrightarrow \mathsf {id}_B = \mathsf {id}_{A \twoheadrightarrow B}
2. (f \circ g) \twoheadrightarrow (h \circ i) = (g \twoheadrightarrow h) \circ (f \twoheadrightarrow i)

Upshot.

• Liam O'Connor

Our category \textbf {Cpo} has exponentials.