*Sheaves in Geometry and Logic* Chapter V Section 7 Theorem 2: $U$ has right adjoint, or $T$ has right adjoint?

Question

In Mac Lane and Moerdijk's Sheaves in Geometry and Logic, the following theorem is stated in Chapter V Section 7:

Theorem 2: For a category object $C$ in a category $\mathcal{E}$ with pullbacks, the forgetful functor $U : \mathcal{E}^C \to \mathcal{E}$ has a left adjoint $F$, and $U$ is monadic; that is, the category $\mathcal{E}^C$ of left $C$-objects is equivalent (actually, isomorphic to) the category of algebras for the monad $T = UF$ on $\mathcal{E}/C_0$ (cf. $\S IV.4$). Moreover, if $\mathcal{E}$ is a topos, then the functor $U$ has a right adjoint.

The theorem starts off reasonably by explicitly constructing $F$, showing that $F$ is the left adjoint of $U$, and then demonstrating that $U$ is strictly monadic.

However, the proof does not ever show that $U$ has a right ajdoint. Instead, the authors note that $T = \Sigma_{d_1} \circ d^*_0$ and then conclude that $T$ has a right adjoint with the sentence

By Theorem IV.7.2 for a topos, each of the two functors $\Sigma_{d_1}$ and $d_0^*$ has a right adjoint, and hence so does their composite $T$, as asserted in the theorem.

What is going on?

Answer 1

The proof of Theorem V.7.2 actually relies on a theorem that has not yet been proved. This is not clearly explained in the text.

Reading a bit further into Chapter V, one encounters the following theorem in section 8:

Corollary 3: If $(T, \eta, \mu)$ is a monad on the category $\mathcal{A}$ while $G$ is a right adjoint to the functor $T : \mathcal{A} \to \mathcal{A}$, then the forgetful functor $U : \mathcal{A}^T \to \mathcal{A}$ has both a left and a right adjoint.

Now recall that the text for Theorem V.7.2 wraps up by concluding that $U$ is monadic and that $T$ has a right adjoint. Since $U$ is equivalent to the forgetful functor $(\mathcal{E}/C_0)^T \to \mathcal{E}/C_0$, $U$ must therefore also have a right adjoint.