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.

Definition

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

Monoid

$\ast$ is a monoid with identity $e$

Left Projection

$L\ast (x,y)=x$

Right Projection

$R\ast (x,y)=y$

Surjective Pairing

$(L\ast x,R\ast x)=x$

Right Homogeneity

$(x\ast z,y\ast z)=(x,y)\ast z$

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