\begin{definition}[Definition:Contravariant Power Set Functor]
Let $\mathbf{Set}$ be the category of sets.
The '''contravariant power set functor''' $\overline \PP: \mathbf{Set} \to \mathbf{Set}$ is the contravariant functor which sends:
* An object $x$ to its power set $\powerset x$.
* A morphism $f : x \to y$ to the inverse image mapping $\map {\overline \PP} f : \powerset y \to \powerset x$.
\end{definition}