Cartesian closed monoid (source code)

= Cartesian closed monoid
{title2=$M=\operatorname{End}(D)$}

A monoid encoding a one-object product and exponential structure: pairing is inverse to the map $z\mapsto(\pi z,\pi' z)$, and currying is inverse to $y\mapsto\varepsilon\langle y\pi,\pi'\rangle$. These bijections imply pairing naturality $\langle x,y\rangle z=\langle xz,yz\rangle$ and currying naturality $(x\langle z\pi,\pi'\rangle)^*=x^*z$. The element $e=(\pi')^*$ then satisfies $ez=e$ for every $z$, hence is idempotent. Splitting $e$ supplies a terminal object and a two-object <Cartesian closed category> whose endomorphisms at the original object are $M$. For the original object to be nonterminal, $M$ must be nontrivial.