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
.