= Cartesian closure for a finite-limit-preserving comonad
{c}
Let $G$ be a <Cartesian comonad> on a <Cartesian category> that is <Cartesian closed>. Its <forgetful functor> creates finite limits. For coalgebras $(A,a)$ and $(B,b)$, set $D=B^A$, $W=(GB)^A$. Transpose $G D\times A\xrightarrow{1\times a}GD\times GA\cong G(D\times A)\xrightarrow{G\operatorname{ev}}GB$ to $q:GD\to W$, and put $p=b^A\epsilon_D:GD\to W$. Their <cofree coalgebra> transposes $Gp\delta_D,Gq\delta_D:R(D)\rightrightarrows R(W)$ have a coalgebra equalizer. A map into this equalizer is exactly a map $C\times A\to B$ respecting coalgebra structures, so it is the required <exponential object>. No subobject classifier on the base category is needed.
Back to article page
