Solution (source code)

= Solution

Write the <comonad> as $(G,\epsilon,\delta)$ and its <category of coalgebras for a comonad> as $\mathcal E^G$. A <coalgebra for a comonad> is a map $a:A\to GA$ with $\epsilon_Aa=1_A$ and $\delta_Aa=Ga\,a$. A morphism $f:(A,a)\to(B,b)$ satisfies $bf=Gf\,a$. Let $U:\mathcal E^G\to\mathcal E$ be the <forgetful functor> and let $R(X)=(GX,\delta_X)$ be the <cofree coalgebra>. The <adjunction> $U\dashv R$ has the explicit correspondence
$$
f:UA\to X\quad\longleftrightarrow\quad Gf\,a:A\to R(X).
$$
We construct the three pieces of the <elementary topos> structure.

Because $G$ preserves <finite limits>, each underlying finite limiting cone has a unique coalgebra structure induced by the structures on its vertices. The counit and coassociativity equations can be checked after its jointly monic projections. Thus $U$ creates <finite limits> and reflects isomorphisms. A morphism of coalgebras is monic exactly when its underlying morphism is monic, by the diagonal criterion using the created <pullback>.

For <exponentials in a coalgebra topos>, fix coalgebras $(A,a)$ and $(B,b)$ and put $E=B^A$ in $\mathcal E$. On the cofree coalgebra $R(E)$ there is an underlying evaluation
$$
e:GE\times A\longrightarrow B,\qquad e=\operatorname{ev}(\epsilon_E\times1_A).
$$
The two maps
$$
b e,\qquad Ge\,(\delta_E\times a):GE\times A\longrightarrow GB
$$
use $G(GE\times A)\cong GGE\times GA$ in the second expression. Transpose them in $\mathcal E$ to maps $r,s:GE\rightrightarrows(GB)^A$, and then transpose across $U\dashv R$ to coalgebra morphisms $\widetilde r,\widetilde s:R(E)\rightrightarrows R((GB)^A)$. Take their <equalizer> $C$ in $\mathcal E^G$.

An underlying map $UX\times A\to B$ corresponds to a coalgebra map $h:X\to R(E)$. The equation saying that the original map is a coalgebra morphism is precisely $rh=sh$, since $\delta_Eh=Gh\,x$ for the structure $x:X\to GX$. By the cofree adjunction, this is equivalent to $\widetilde rh=\widetilde sh$, hence to unique factorization through $C$. Therefore
$$
\mathcal E^G(X,C)\cong\mathcal E^G(X\times A,B),
$$
naturally in $X$. This constructs the required <exponential object>.

For the <subobject classifier of a coalgebra topos>, let $\top:1\hookrightarrow\Omega$ be the underlying <subobject classifier>, and let $\kappa:G\Omega\to\Omega$ classify the mono $G\top:G1\cong1\hookrightarrow G\Omega$. Its cofree transpose is the coalgebra endomorphism
$$
k=G\kappa\,\delta_\Omega:R\Omega\longrightarrow R\Omega.
$$
Define $\Omega_G$ as the <equalizer> of $k$ and $1_{R\Omega}$. The transpose of $\top$ factors through this <equalizer> and gives $\top_G:1\to\Omega_G$.

Indeed, for a <subobject> $S\hookrightarrow UX$ classified by $\chi:UX\to\Omega$, the <pullback> $x^{-1}(GS)$ has characteristic map $\kappa G\chi\,x$. It is always contained in $S$, by naturality of the counit. Equality holds exactly when $x$ restricts to a coalgebra structure on $S$; its axioms then follow by composing with the <monomorphisms> $GS\hookrightarrow GX$ and $GGS\hookrightarrow GGX$. Under $U\dashv R$, the classifying map becomes $h=G\chi\,x:X\to R\Omega$. The equality of <subobjects> is $\epsilon_\Omega h=\kappa h$. Transposing this equality gives $h=kh$, so exactly the coalgebra <subobjects> correspond to maps $X\to\Omega_G$. Their <pullback> of $\top_G$ is the desired subcoalgebra, and uniqueness follows from uniqueness of $\chi$.

Thus we have <finite limits>, exponentials and a <subobject classifier>:
$$
\boxed{\mathcal E^G\text{ is an elementary topos}.}
$$
The construction does not assume that $G$ preserves the underlying exponentials or underlying <subobject classifier>.