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