Theorem. Commutative monoid structure for cpos [dt-002H]

Cpos form a commutative monoid "up to isomorphism" under \times and \mathbf {1} (the cpo consisting of only one element \bot ). That is, for all cpos A, B and C:

  1. A \times \mathbf {1} \simeq A
  2. A \times (B \times C) \simeq (A \times B) \times C
  3. A \times B \simeq B \times A

Proof.

The isomorphisms required are the projection \pi _0, the \mathit {juggle} function from Exercise [dt-002G], and the swap function.