Can a general version of the covariant powerset monad be derived from the universal property of power objects? As the title asks, I'm wondering if one can generally squeeze a "covariant power object monad" out of a topos (following the usual example in $\mathcal{Set}$ with functor part the direct image powerset functor), or if there's a nice counterexample showing why not.
I am guessing that the answer to this is negative, since I only see this monad discussed in the case of $\mathcal{Set}$ so I suspect it depends on more special properties of that category; in which case I'm curious what special properties make it work.
Edit: In particular, I understand the usual construction of the functor part, but have myself been unable to verify that the obvious candidates for the unit and multiplication actually work as such.
 A: In fact, the answer is yes. The algebras for the monad are, of course, the internal complete join semilattices.
First things first: the unit $\eta_X : X \to P X$ is given by the transpose of the morphism $X \times X \to \Omega$ that classifies the diagonal $\Delta : X \to X \times X$. To see that it is a natural transformation, it is easiest to use internal logic: given $f : X \to Y$, we want to show
$$x : X \vdash \exists_f (\eta_X (x)) = \eta_Y (f (x))$$
which by "extensionality" is equivalent to
$$x : X, y : Y \vdash y \in \exists_f (\eta_X (x)) \leftrightarrow y \in \eta_Y (f (x))$$
which by definition of $\exists_f$ is equivalent to
$$x : X, y : Y \vdash (\exists x' : X . x' \in \eta_X (x) \land f (x') = y) \leftrightarrow y \in \eta_Y (f (x))$$
which by definition of $\eta$ is equivalent to
$$x : X, y : Y \vdash (\exists x' : X . x' = x \land f (x') = y) \leftrightarrow y = f (x)$$
which is obviously a tautology.
The multiplication $\mu_X : P P X \to P X$ has a simple description in internal logic:
$$\mu_X (t) = \left\{ x : X \mid \exists s : P X . s \in t \land x \in s \right\}$$
If you unfold this, it amounts to saying that $\mu_X$ is the transpose of the morphism $P P X \times X \to \Omega$ that classifies the image of the composite
$$R \rightarrowtail P P X \times P X \times X \to P P X \times X$$
where the second arrow is the obvious projection and the first arrow is defined by the following pullback diagram,
$$\require{AMScd}
\begin{CD}
R @>>> [\ni] \times [\ni] \\
@VVV @VVV \\
P P X \times P X \times X @>>{\mathrm{id} \times \Delta \times \mathrm{id}}> P P X \times P X \times P X \times X
\end{CD}$$
where $[\ni] \rightarrowtail P P X \times P X$ and $[\ni] \rightarrowtail P X \times X$ are the universal binary relations. Of course, it would be a nightmare to verify that $\mu_X$ defined this way is natural in $X$, so it's better to stick with the description in internal logic. I leave the verification to you – naturality amounts to saying that $\exists$ commutes with $\exists$.
It remains to be shown that $\eta$ and $\mu$ satisfy the monad axioms. It should go without saying that the best way to proceed is to use internal logic. 


*

*The left unit axiom is easy enough: it translates to
$$s : P X \vdash \mu_X (\eta_{P X} (s)) = s$$
which is equivalent to
$$s : P X, x : X \vdash x \in \mu_X (\eta_{P X} (s)) \leftrightarrow x \in s$$
which expands to
$$s : P X, x : X \vdash (\exists s' : P X . s' \in \eta_{P X} (s) \land x \in s') \leftrightarrow x \in s$$
which expands to
$$s : P X, x : X \vdash (\exists s' : P X . s' = s \land x \in s') \leftrightarrow x \in s$$
which is a tautology.

*The right unit axiom is more complicated: it translates to
$$s : P X \vdash \mu_X (\exists_{\eta_X} (s)) = s$$
which is equivalent to
$$s : P X, x : X \vdash x \in \mu_X (\exists_{\eta_X} (s)) \leftrightarrow x \in s$$
which is expands to
$$s : P X, x : X \vdash (\exists s' : P X . s' \in \exists_{\eta_X} (s) \land x \in s') \leftrightarrow x \in s$$
which is expands to
$$s : P X, x : X \vdash (\exists s' : P X . \exists x' : X . x' \in s \land \eta_X (x') = s' \land x \in s') \leftrightarrow x \in s$$
which is equivalent to 
$$s : P X, x : X \vdash (\exists x' : X . x' \in s \land x \in \eta_X (x')) \leftrightarrow x \in s$$
which expands to
$$s : P X, x : X \vdash (\exists x' : X . x' \in s \land x = x') \leftrightarrow x \in s$$
which is a tautology.

*The associativity axiom is even more complicated to write out, but it is still straightforward – it amounts to the associativity of $\exists$.

