Contravariant power-object functor
= Contravariant power-object functor
{title2=$P:\mathcal E^{\mathrm{op}}\to\mathcal E$}
An arrow $f:A\to B$ induces $Pf:PB\to PA$ by inverse image of predicates. Transposition of predicates on $A\times B$ gives $\mathcal E(A,PB)\cong\mathcal E(B,PA)$ and the adjunction $P^{\mathrm{op}}\dashv P$. The induced monad on the topos is double power-object formation; it is distinct from the covariant powerset monad on sets.