Margrabe's formula

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⟩$ 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 $(-,-)$.