Power-object monadicity
= Power-object monadicity
{title2=$\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>.