Corollary. Derived properties of cpo products [dt-002C]

The universal property is called such because all the familiar properties of products follow from it – thinking in pictures helps to see how (Indeed, the universal property characterises products up to isomorphism):

  1. \pi _0 \circ (f \times g) = f \circ \pi _0
  2. \pi _1 \circ (f \times g) = g \circ \pi _1
  3. (f \times g) \circ \langle h , i \rangle = \langle f \circ h, g \circ i \rangle
  4. \langle f , g \rangle \circ h = \langle f \circ h, g \circ h \rangle
  5. \mathsf {id}_A \times \mathsf {id}_B = \mathsf {id}_{A \times B} \quad (*)
  6. (f \circ g) \times (h \circ i) = (f \times h) \circ (g \times i) \quad (**)

These last two statements (*) and (**) show that \times is a bifunctor on the category \textbf {Cpo}, i.e., a functor \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}.