Cartesian monoid

From HandWiki

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 [math]\displaystyle{ \langle *,e,(-,-),L,R\rangle }[/math] where [math]\displaystyle{ * }[/math] and [math]\displaystyle{ (-,-) }[/math] are binary operations, [math]\displaystyle{ L, R }[/math], and [math]\displaystyle{ e }[/math] are constants satisfying the following axioms for all [math]\displaystyle{ x,y,z }[/math] in its universe:

Monoid
[math]\displaystyle{ * }[/math] is a monoid with identity [math]\displaystyle{ e }[/math]
Left Projection
[math]\displaystyle{ L * (x,\,y) = x }[/math]
Right Projection
[math]\displaystyle{ R * (x,\,y) = y }[/math]
Surjective Pairing
[math]\displaystyle{ (L*x,\,R*x) = x }[/math]
Right Homogeneity
[math]\displaystyle{ (x*z,\,y*z)=(x,\,y) * z }[/math]

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

References

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