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 ⟨*,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

  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 .