 Contravariant power-object functor

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}}⊣P$. The induced monad on the topos is double power-object formation; it is distinct from the covariant powerset monad on sets.