Cartesian comonad (source code)

= Cartesian comonad
{c}
{title2=$(G,\varepsilon,\delta)$}

In the finite-limit setting, a Cartesian comonad is a <comonad> whose underlying endofunctor preserves <finite limits>. Its <category of coalgebras for a comonad> has finite limits created by the <forgetful functor>. On an <elementary topos>, equalizer constructions of <exponentials in a coalgebra topos> and the <subobject classifier of a coalgebra topos> make that coalgebra category an elementary topos.