Power-object monadicity (${\mathcal{E}}^{\mathrm{op}}\simeq {\mathcal{E}}^{PP}$)

The contravariant power-object functor of an elementary topos is monadic. Its double-power unit ${\eta }_A(a)(S)=(a\in S)$ is monic, which helps prove that $P$ reflects isomorphisms. Finite equalizers and the fact that power objects turn coreflexive equalizers into coequalizers give the remaining hypotheses of the crude monadicity theorem.

For an elementary topos, existence of products in a category indexed by a fixed set is equivalent to existence of the corresponding coproducts in a category. The power-object monadicity equivalence ${\mathcal{E}}^{\mathrm{op}}\simeq {\mathcal{E}}^{PP}$ gives the forward direction because Eilenberg-Moore categories create limits. For the converse, the diagonal into the pointwise product category is a logical functor. A coproduct is its left adjoint; the adjoint lifting theorem for monad algebra functors, applied through power-object monadicity, then gives its right adjoint, namely the product. The required reflexive coequalizers on the algebra side are opposites of finite equalizers in the topos.