Cartesian monoid
Appearance
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 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
- MR 1611514.