Cartesian monoid

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.^[1]

Definition

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

Monoid

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

Left Projection

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

Right Projection

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

Surjective Pairing

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

Right Homogeneity

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

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