In the category of sets epimorphisms are surjective - Constructive Proof? The statement that surjective maps are epimorphisms in the category of sets can be shown in a constructive way.
What about the inverse?
Is it possible to show that every epimorphism in the category of sets is surjective without reverting to a proof by contradiction / negation?
 A: Here's a proof in constructive set theory (probably just a rephrasing of the topos theoretic proof but you might find it useful).
Let $h : A \twoheadrightarrow B$ be an epimorphism. Define
$$
C := \{\{0\}\} \cup \bigcup_{b \in B}\{\{x \in \{0\} \;|\; \exists a \in A\; h(a)=b\}\}
$$
(If the powerset axiom is available, one can alternatively use $C := \mathcal{P}(\{0\})$)
Define functions $f, g : B \rightarrow C$ as follows.
$$
f(b) := \{ x \in \{0\} \;|\; \exists a \in A\;h(a) = b \} \\
g(b) := \{0\}
$$
We clearly have $f \circ h = g \circ h$, so since $h$ is an epimorphism, we get $f = g$. Now for any $b \in B$, we have that $f(b) = g(b)$. Therefore the set $\{x \in \{0\} \;|\; \exists a \in A \; h(a) = b \}$ is inhabited, and so there exists $a$ in $A$ such that $h(a) = b$.
A: I want to write down a proof that comes naturally, in a way.  This proof assumes that you can form the quotient of a set modulo an equivalence relation, but does not require powersets.  (So it works in any pretopos.)
We have sets $ A $ and $ B $ and a function $ f $ from $ A $ to $ B $.  We know that $ f $ is an epimorphism in the category of sets, and we want to prove that $ f $ is a surjection.
Consider the cokernel pair of $ f $, that is the pushout of $ f $ along itself.  Just as epimorphisms in an abelian category have trivial cokernels, so epimorphisms in more general categories have trivial cokernel pairs.  So this is a natural thing to look at.
$$ \matrix { A & \overset { \textstyle f } \rightarrow & B \\ \llap f \downarrow & & \downarrow \rlap { k _ 1 } \\ B & \underset { \textstyle k _ 0 } \rightarrow & C } $$
The cokernel pair is a set $ C $ defined as a quotient of the disjoint union $ B \uplus B $; if $ y $ is an element of $ B $, then I'll write $ y _ 0 $ and $ y _ 1 $ for elements of $ B \uplus B $.  Then we have an equivalence relation on $ B \uplus B $ according to which $ y _ 0 $ and $ y _ 1 $ are equivalent iff $ y $ belongs to the image of $ f $, and no other equivalences exist besides the reflexive ones.  (More explicitly, $ y _ i $ and $ z _ j $ are equal iff $ y = z $ and $ i = j $ or $ y = z $ and $ y = f ( x ) $ for some $ x $.)  Then $ C $ is the quotient of $ B \uplus B $ under this equivalence relation.  The cokernel pair also comes equipped with two inclusion/quotient maps from $ B $, while I'll call $ k _ 0 $ and $ k _ 1 $; $ k _ i $ maps $ y $ to the equivalence class of $ y _ i $ in $ C $.
Given an element $ x $ in $ A $, $ k _ 0 ( f ( x ) ) = k _ 1 ( f ( x ) ) $ in $ C $ because $ f ( x ) $ is in the image of $ f $.  So since $ f $ is an epimorphism, $ k _ 0 = k _ 1 $.  This means that for every element $ y $ of $ B $, $ k _ 0 ( y ) = k _ 1 ( y ) $, so $ y $ is in the image of $ f $.
So $ f $ is surjective.
A: Theorem: Every epi is surjective.
Proof.
Let $h : A \to B$ be an epimorphism. We define maps $f, g : B \to \mathcal{P}(B)$ by
\begin{align*}
  f(b) &= \{b\} \cap \mathrm{im}(h)\\
  g(b) &= \{b\}
\end{align*}
where we recall that $\mathrm{im}(h) = \{b \in B \mid \exists a \in A \,.\, h(a) = b\}$.
For every $a \in A$ we have $f(h(a)) = \{h(a)\} = g(h(a))$, therefore $f = g$ as $h$ is epi. Now, for every $y \in B$ we have $\{y\} = g(y) = f(y) = \{y\} \cap \mathrm{im}(h)$, therefore $y \in \mathrm{im}(h)$. QED.
Supplemental 2022-01-09: Here is an improved version which uses a smaller codomain. We write $\Omega$ for the subobject classifier (the set of truth values).
Proof.
Let $h : A \to B$ be an epimorphism and $b \in B$. We define maps $f, g : B \to \Omega$ by
\begin{align*}
  f(b') &{}\mathbin{{:}{=}} (b = b' \land \exists a \in A . h(a) = b')\\
  g(b') &{}\mathbin{{:}{=}} (b = b').
\end{align*}
For every $a \in A$ we have
\begin{align*}
  f(h(a)) &\Leftrightarrow (b = h(a) \land \exists a' \in A . h(a') = h(a)) \\
 &\Leftrightarrow (b = h(a)) \\
 &\Leftrightarrow g(h(a)),
\end{align*}
therefore $f = g$ as $h$ is epi. Now
\begin{align*}
 \top &\Leftrightarrow b = b \\
 &\Leftrightarrow g(b) = f(b) \\
 &\Leftrightarrow b = b \land \exists a \in A . h(a) = b  \\
 &\Leftrightarrow \exists a \in A . h(a) = b. \quad \Box
\end{align*}
A: The statement "a morphism is a surjection iff it is an epimorphism" holds in every topos, regardless of the law of excluded middle.
The precise proof depends on your notion of "surjection" (in a topos all reasonable internal notions of a surjection coincide --- in fact, due to the above statement, one may define a surjection as an epimorphism).
Perhaps the most obvious notion is: a morphism $s \colon A \rightarrow B$ is a surjection if whenever $b \in B$ then $\underset{a\in A}\exists s(a) = b$ in the internal logic of the category. If a category is regular, then such surjections coincide with covers. And covers are another obvious notion for surjections: a morphism $s \colon A \rightarrow B$ is a surjection (i.e. cover) if in the image-factorisation $A \rightarrow s[A] \rightarrow B$ the monomorphism $s[A] \rightarrow B$ is iso.
Since every topos is a balanced category, in every topos covers coincide with epimorphisms.
