Where is choice used in "Every category monadic over Set is regular" From Johnstone's notes: If $\mathbb{T}$ is a monad on $\mathcal{C}$ whose functor part $T$ preserves covers then the functoriality of image factorisation induces a unique algebra structure on the image making it into an image in $\mathcal{C}^\mathbb{T}$.
He then says 'in particular any category monadic over Set is regular, at least if we assume axiom of choice'. I am lost at two points

*

*Why would any monad over Set necessarily preserve covers?

*How does this proof use choice, it seems to me that the choice of image (and its algebra structure) is uniquely determined given an algebra homomorphism, and the images in $\mathcal{C}$. Is the use of choice related to 1.?

 A: By the axiom of choice, every epimorphism in $\textbf{Set}$ is split.
Any functor preserves split epimorphisms, hence every monad on $\textbf{Set}$ preserves regular epimorphisms.
Thus the theorem about the regularity of categories of algebras applies.
The axiom of choice is not necessary in every case, however.
For certain monads, such as the monads associated with finitary algebraic theories, it is possible to show by other means that the category of algebras is regular.
This is related to the fact that finitary products of regular epimorphisms are regular (in a regular category).
I expect that if you try to carry out the same proof for infinitary algebraic theories you will see where the axiom of choice is (implicitly) used – but I do not know whether there are other proofs avoiding choice.
A: I will assume that you are treating $C$ as a regular category with the regular Grothendieck topology. Thus, preserving covers is equivalent to preserving regular epis.
For question 1:
Set has an interesting property, which is that epis, regular epis, and split epis are all equivalent. Epis in the category of sets are exactly surjections. In a general category, all split epis are regular epis, and all regular epis are epis, but the reverse inclusions need not hold.
So if we have any epi (that is, any surjection) $f : A \to B$, there exists some $g : B \to A$ such that $f \circ g = 1_B$. This is one statement of the axiom of choice.
Now note that split epis are preserved by any functor whatsoever. If we have a split epi $f : A \to B$, take a section $g : B \to A$. Then $F(f) \circ F(g) = F(f \circ g) = F(1_B) = 1_{F(B)}$, so $F(f)$ has section $F(g)$ and hence is a split epi.
In particular, then, the functor part of a monad on $Set$ preserves regular epimorphisms, hence preserves covers.
For question 2:
You saw above how the proof used the axiom of choice. Now, we show that the proof requires the axiom of choice. We assume that Set is a $\Pi W$ pretopos, so the proof works in any topos with NNO.
Consider a surjection $f : A \to B$. We will construct a particular monad $W$ such that $W(f)$ is a surjection if and only if $f$ has a section. By so doing, we will prove that if every monad on Set preserves surjections, then the axiom of choice must hold.
Now given a set $C$, we construct the W-type with $C$ 0-ary constructors and 1 $B$-ary constructor. That is, we construct a set $W(C)$, together with functions $\eta_C : C \to W(C)$ and $h_C : W(C)^B \to W(C)$, which is initial given such data. Clearly, $W$ can be made into a functor in the obvious way, which makes both $\eta_C$ and $h_C$ natural transformations.
Now define $\mu_C: W(W(C)) \to W(C)$ to be the unique map such that $\mu_C \circ \eta_{W(C)} = 1_{W(C)}$ and $h_C \circ (\mu_C^B) = \mu_C \circ h_{W(C)}$.
Then $(W, \eta, \mu)$ forms a monad on Set.
Now suppose that $W$ preserves surjections. Then in particular, we have that $W(f)$ is a surjection, since $f$ is.
Now there is a distinguished element $h_B(\eta_B) \in W(B)$. Since $W(f)$ is surjective, there exists some $x \in W(A)$ such that $W(f)(x) = h_B(\eta_B)$.
$\DeclareMathOperator{im}{im}$
It is now time to back up and discuss $W$-types in a bit more detail. Consider the fact that there is an obvious map $C \coprod W(C)^B \to W(C)$ built from $\eta_C$ and $h_C$. In fact, it can be shown that $k_C$ is an isomorphism; its inverse can be explicitly constructed by building the obvious maps $C \to C \coprod W(C)^B$, $(C \coprod W(C)^B)^B \to C \coprod W(C)^B$ and using the universal property of $W(C)$.
The fact that the obvious map is an isomorphism means three things: (1) $\eta_C$ and $h_C$ are injective, (2) $\im(\eta_C) \cap \im(h_C) = \emptyset$, and (3) $\im(\eta_C) \cup \im(h_C) = W(C)$.
Now let us go back to $x \in W(A)$. By (3), we have $\im(\eta_A) \cup \im(h_A) = W(A)$; since $x \in W(A)$, we have two cases. In the first case, write $x = \eta_A(c)$. Then $W(f)(x) = \eta_B(f(c)) \in \im(\eta_B)$. But $W(f)(x) = h_b(\eta_B) \in \im(h_B)$, so by (2), we have $W(f)(x) \in \im(\eta_B) \cap \im(h_B) = \emptyset$, which is a contradiction. So we know we have $x \in \im(h_A)$; write $x = h_A(y)$ for some $y \in W(A)^B$.
Then we have $W(f)(x) = W(f)(h_A(y)) = h_B(W(f) \circ y) = h_B(\eta_B)$. Therefore, we have $W(f) \circ y = \eta_B$.
Now consider some $b \in B$. Let us analyse the form of $y(b)$. We have two cases. The first is that $y(b) \in \im(h_A)$; write $y(b) = h_A(z)$. Then $\eta_B(b) = W(f)(y(b)) = W(f)(h_A(z)) = h_B(W(f) \circ z)$, but this contradicts that $\im(\eta_B) \cap \im(h_B) = \emptyset$. So we know we have $y(b) \in \im(\eta_A)$; write $y(b) = \eta_A(z)$. Then since $\eta_A$ is injective, there is a unique $z$ such that $y(b) = \eta_A(z)$. Write this $z$ as $g(b)$.
So we have defined a function $g : B \to A$ such that for all $b$, $y(b) = \eta_A(g(b))$. Then $y = \eta_A \circ g$. Therefore, we have $W(f) \circ \eta_A \circ g = \eta_B \circ f \circ g = \eta_B$. Since $\eta_B$ is injective, we have $f \circ g = 1_B$.
Therefore, we have explicitly constructed a section of $f$.
So the statement "all monads on Set preserve surjections" is equivalent to the axiom of choice.
