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.

Definition

A Cartesian monoid is a structure with signature ⟨ ∗ , e , ( − , − ) , L , R ⟩ {\displaystyle \langle *,e,(-,-),L,R\rangle } where ∗ {\displaystyle *} and ( − , − ) {\displaystyle (-,-)} are binary operations, L , R {\displaystyle L,R}, and e {\displaystyle e} are constants satisfying the following axioms for all x , y , z {\displaystyle x,y,z} in its universe:

Monoid

∗ {\displaystyle *} is a monoid with identity e {\displaystyle e}

Left Projection

L ∗ ( x , y ) = x {\displaystyle L*(x,\,y)=x}

Right Projection

R ∗ ( x , y ) = y {\displaystyle R*(x,\,y)=y}

Surjective Pairing

( L ∗ x , R ∗ x ) = x {\displaystyle (L*x,\,R*x)=x}

Right Homogeneity

( x ∗ z , y ∗ z ) = ( x , y ) ∗ z {\displaystyle (x*z,\,y*z)=(x,\,y)*z}

The interpretation is that L {\displaystyle L} and R {\displaystyle R} are left and right projection functions respectively for the pairing function ( − , − ) {\displaystyle (-,-)}.