A Cartesian monoid is a monoid, with additional structure of pairing and projection operators. It was first formulated by Dana Scott and Joachim Lambek independently.
A Cartesian monoid is a structure with signature ⟨ ∗ , e , ( − , − ) , L , R ⟩ where ∗ and ( − , − ) are binary operations, L , R , and e are constants satisfying the following axioms for all x , y , z in its universe:
Monoid ∗ is a monoid with identity
e Left Projection L ∗ ( x , y ) = x Right Projection R ∗ ( x , y ) = y Surjective Pairing ( L ∗ x , R ∗ x ) = x Right Homogeneity ( x ∗ z , y ∗ z ) = ( x , y ) ∗ z The interpretation is that L and R are left and right projection functions respectively for the pairing function ( − , − ) .
