Sums form a bifunctor [dt-0036]

With these, we can define the morphism mapping for the sum bifunctor (+) : \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}. Just as with products and functions, we will overload the + notation for morphisms as well as objects in the category \mathbf {Cpo}.

DefinitionSum of functions [dt-0037]

Given functions f : A \twoheadrightarrow C and g : B \twoheadrightarrow D, we have: \begin {array}{l} f+g : (A + B)\twoheadrightarrow (C + D) \\ f+g = [\mathit {inl} \circ f, \mathit {inr} \circ g] \end {array}

Theorem [dt-0038]

+ : \mathbf {Cpo} \times \mathbf {Cpo} \rightarrow \mathbf {Cpo} is a lawful bifunctor, that is:

  1. (\lambda a. a) \times (\lambda b. b) = (\lambda x.x)
  2. (f_1 \circ g_1) \times (f_2 \circ g_2) = (f_1 \times f_2) \circ (g_1 \times g_2)

Context

    Sums [dt-0030]

    Related

      Definition. Bifunctor [dm-000M]

      Definition. Product of functions [dt-0026]

      Construction. Sum of cpos [dt-0031]

      Example. The category \mathbf {Cpo} [dt-002B]

      The function arrow is a bifunctor [dt-002W]