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

edit

A Cartesian monoid is a structure with signature   where   and   are binary operations,  , and   are constants satisfying the following axioms for all   in its universe:

Monoid
  is a monoid with identity  
Left Projection
 
Right Projection
 
Surjective Pairing
 
Right Homogeneity
 

The interpretation is that   and   are left and right projection functions respectively for the pairing function  .

References

edit
  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.