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

References

↑ Statman, Rick (1997), "On Cartesian monoids", Computer science logic (Utrecht, 1996), Lecture Notes in Computer Science, vol. 1258, Berlin: Springer, pp. 446–459, doi:10.1007/3-540-63172-0_55, MR 1611514.

[1] Statman, Rick (1997), "On Cartesian monoids", Computer science logic (Utrecht, 1996), Lecture Notes in Computer Science, vol. 1258, Berlin: Springer, pp. 446–459, doi:10.1007/3-540-63172-0_55, MR 1611514.