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.