Coalgebra for a comonad ($a:A\to GA$)

For a comonad, a coalgebra is a map $a:A\to GA$ satisfying ${ϵ}_{A}a=1_A$ and ${\delta }_{A}a=Gaa$. A morphism $f:(A,a)\to (B,b)$ obeys $bf=Gfa$. This is distinct from the tensor-based notion of a coalgebra in algebra.

The category ${\mathcal{E}}^G$ consists of coalgebras for a comonad and their structure-preserving morphisms. Its forgetful functor has the cofree coalgebra as right adjoint. If $\mathcal{E}$ is a topos and $G$ preserves finite limits, those limits are created by the forgetful functor, while exponentials in a coalgebra topos and the subobject classifier of a coalgebra topos can be constructed as equalizers inside cofree objects.

Let $\kappa :G\Omega \to \Omega$ classify $G\top :1\hookrightarrow G\Omega$. In the cofree coalgebra $R\Omega$, equalize the identity and $G\kappa {\delta }_{\Omega }$. A map $\chi :X\to \Omega$ classifies a subcoalgebra exactly when $\chi =\kappa G\chi x$, since this says the subobject equals the inverse image of its image under $G$. Transposition gives precisely the displayed equalizer condition.

For a finite-limit-preserving comonad on a topos, start with the cofree coalgebra on the ambient exponential $B^A$. Its underlying evaluation is $e=\mathrm{ev}(ϵ\times 1)$. Transpose the two expressions $be$ and $Ge(\delta \times a)$ first using the ambient exponential and then the cofree adjunction. Their coalgebra equalizer represents exactly the maps whose evaluations respect coalgebra structure. Thus coalgebra exponentials need not be the underlying ambient exponentials.

For a comonad, the cofree coalgebra on $X$ is $(GX,{\delta }_X)$. A map $UA\to X$ transposes to the coalgebra morphism $Gfa:A\to GX$. This gives the adjunction $U⊣R$ with the forgetful functor.