The contravariant power-set functor is monadic

A function $X\to \mathcal{P}(Y)$ is the same as a relation $R\subseteq X\times Y$. Transposing $R$ gives a function $Y\to \mathcal{P}(X)$, and transposition is natural and involutive. By [L1] this makes the power-set functor on the opposite side its own left adjoint.

If $f^{-1}:\mathcal{P}(Y)\to \mathcal{P}(X)$ is bijective, then $f$ is surjective because otherwise $\mathrm{\varnothing }$ and a singleton outside $f[X]$ have the same preimage. It is injective because surjectivity of $f^{-1}$ realizes each singleton of $X$ as a preimage, which separates points with different singleton membership. Thus $f$ is bijective and the functor is conservative by [L2], including when $X$ is empty.

A reflexive pair in ${\mathbf{S}\mathbf{e}\mathbf{t}}^{\mathrm{o}\mathrm{p}}$ corresponds to maps $f,g:A\rightrightarrows B$ in $\mathbf{S}\mathbf{e}\mathbf{t}$ with a common retraction $r:B\to A$, so $rf=rg=1_A$. Define $E=\{a\in A:f(a)=g(a)\}$ and let $e:E\hookrightarrow A$ be inclusion. This formula supplies an equalizer for every such pair uniformly, so the opposite maps form the required specified family of reflexive coequalizers in ${\mathbf{S}\mathbf{e}\mathbf{t}}^{\mathrm{o}\mathrm{p}}$.

The square with both left and top maps $e:E\to A$, and with bottom and right maps $f,g:A\rightrightarrows B$, is a pullback: if $f(a)=g(a^{\mathrm{\prime }})$, applying $r$ gives $a=a^{\mathrm{\prime }}\in E$. Hence [L3] gives $e[e^{-1}[S]]=g^{-1}[f[S]]=S\cap e[E]$ for every $S\subseteq A$; the last equality also follows directly, while $f^{-1}[f[S]]=S$ because $rf=1_A$.

Let $H:\mathcal{P}(A)\to Z$ satisfy $H{f}^{-1}=H{g}^{-1}$. Applying this equality to $f[S]$ and using step 2.1 gives $H(S)=H(S\cap e[E])$. Define $\bar{H}:\mathcal{P}(E)\to Z$ by $\bar{H}(R)=H(e[R])$. Then $\bar{H}{e}^{-1}=H$, and this factorization is unique because $e^{-1}:\mathcal{P}(A)\to \mathcal{P}(E)$ is surjective. Thus $e^{-1}$ is the coequalizer of $f^{-1},g^{-1}$, so the power-set functor preserves every reflexive coequalizer in ${\mathbf{S}\mathbf{e}\mathbf{t}}^{\mathrm{o}\mathrm{p}}$.

Step 1.3 supplies the required coequalizer family, while steps 1.1, 1.2, and 3.1 give the left adjoint, conservativity, and preservation hypotheses of [L4]. The crude monadicity theorem therefore proves that $\mathcal{P}:{\mathbf{S}\mathbf{e}\mathbf{t}}^{\mathrm{o}\mathrm{p}}\to \mathbf{S}\mathbf{e}\mathbf{t}$ is monadic.