I am supposed to prove a rather technical property which should hold in any Grothendieck Topos, but I have troubles in accomplishing this task. Here is the context for the question.
Let then $\mathscr{E}$ be a Grothendieck Topos and suppose to have spans
$$ Y_{1}\xleftarrow{h_{1}} Y_{0}\xrightarrow{h_{2}} Y_{2},\quad X_{1}\xleftarrow{k_{1}} X_{0}\xrightarrow{k_{2}} X_{2} $$
in $\mathscr{E}$. Assume given a morphism between those spans, i.e. a triple
$$ (Y_{1}\xrightarrow{f_{1}} X_{1},\ Y_{0}\xrightarrow{f_{0}} X_{0},\ Y_{2}\xrightarrow{f_{2}} X_{2}) $$
making the following diagram commutative
$$ \newcommand{\ra}[1]{\kern-1.5ex\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} \newcommand{\la}[1]{\kern-1.5ex\xleftarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} \newcommand{\ras}[1]{\kern-1.5ex\xrightarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex} \newcommand{\las}[1]{\kern-1.5ex\xleftarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex} \newcommand{\da}[1]{\bigg\downarrow\raise.5ex\rlap{\scriptstyle#1}} \begin{array}{c} Y_{1} & \la{h_1} & Y_{0} & \ra{h_2} & Y_{2} \\ \da{f_1} & & \da{f_0} & & \da{f_2} \\ X_{1} & \las{k_1} & X_{0} & \ras{k_2} & X_{2} \\ \end{array} \qquad\qquad (\dagger) $$ Suppose, in addition, that both the squares in $(\dagger)$ above are pullback squares, i.e. $Y_{0}=X_{0}\times_{X_{1}} Y_{1}$ and $Y_{0}=X_{0}\times_{X_{2}} Y_{2}$.
Now, I can take the pushout of the first and of the second row of $(\dagger)$, so as to get pushout diagrams
$$ \begin{array}{c} Y_{0} & \ra{h_2} & Y_{2} \\ \da{h_1} & & \da{\pi_{Y_{2}}} \\ Y_{1} & \ras{\pi_{Y_{1}}} & Y\\ \end{array} \quad\quad \begin{array}{c} X_{0} & \ra{k_2} & X_{2} \\ \da{k_1} & & \da{\pi_{X_{2}}} \\ X_{1} & \ras{\pi_{X_{1}}} & X\\ \end{array} $$
By functoriality of the pushout, we then get an induced map $f\colon Y\rightarrow X$ which is such that $f\circ \pi_{Y_{j}}=\pi_{X_{j}}\circ f_{j}$, for $j\in\{1,2\}$. I can then take the pullbacks (again for $j\in\{1,2\}$)
$$ \begin{array}{c} X_{0}\times_{X} Y & \ra{}& Y \\ \da{} & & \da{f} \\ X_{0} & \ras{\pi_{X_{1}}\circ\ k_{1}} & X\\ \end{array} \quad\quad \begin{array}{c} X_{j}\times_{X} Y & \ra{}& Y \\ \da{} & & \da{f} \\ X_{j} & \ras{\pi_{X_{j}}} & X\\ \end{array} \quad\quad (\ddagger) $$
Finally, I have pairs of maps $(Y_{0}\xrightarrow{f_{0}} X_{0},\ Y_{0}\xrightarrow{\pi_{Y_{1}}\circ\ h_{1}} Y)$ and $(Y_{j}\xrightarrow{f_{j}} X_{j},\ Y_{j}\xrightarrow{\pi_{Y_{j}}} Y)$, for $j\in\{1,2\}$, which are compatible with the pullbacking maps in $(\ddagger)$, so that I get maps $g_{l}\colon Y_{l}\rightarrow X_{l}\times_{X} Y$ (here $l\in\{0,1,2\}$) satisfying the prescribed commutativity properties.
Here is the question: I need to prove that each such $g_{l}$ is a regular epimorphism.
Actually, I would already be satisfied if I could prove the claim for $\mathscr{E}=\mathbf{Set}$, hopefully using some categorical arguments (i.e. topos-theoretic properties of $\mathbf{Set}$), but even an elementwise proof may be good. I am completely stuck with the task of showing this result: I have tried to write down explicitely the maps $g_{l}$ but I am unable to prove their surjectivity. I have also tried to write down some more diagrams, muttering something about the effectiveness of equivalence relations in $\mathbf{Set}$ (actually, in any Grothendieck Topos) and the fact that the pullback functors along a map $g\colon A\rightarrow B$ in $\mathbf{Set}$ (actually, in any (Grothendieck) Topos) preserve colimits between the appropriate slice categories. The idea behind this attempt was that of proving that each $g_{l}$ is the coequaliser of its kernel pair (which must be true, if the result has to hold), but I could not show this fact.
Any help (solutions or ideas) would be greately appreciated.
As discussed, it suffices to prove the claim for $\mathcal{E} = \mathbf{Set}$.
Let $x_1 \in X_1$, $y \in Y$, and suppose $\pi (x_1) = f (y)$. Consider $y$:
Thus we may assume $y = \pi (y_1)$ for some $y_1 \in Y_1$. The trick is in choosing $y_1$ so that $f_1 (y_1) = x_1$. For this, observe that there is a unique function $d : X_1 \times X_1 \to \mathbb{N} \cup \{ \infty \}$ satisfying the following conditions:
It follows from these conditions that $d$ is a metric on $X_1$. Now:
Thus, by induction on $d (f_1 (y_1), x_1)$, we deduce there is always some choice of $y_1 \in Y_1$ such that $f_1 (y_1) = x_1$. This proves that $Y_1 \to X_1 \times_X Y$ is surjective. By symmetry, $Y_2 \to X_2 \times_X Y$ is also surjective.
It remains to be shown that $Y_0 \to X_0 \times_X Y$ is surjective. Let $x_0 \in X_0$, $y \in Y$, and suppose $\pi (k_1 (x_0)) = f (y)$. By the above, there is $y_1 \in Y_1$ such that $f_1 (y_1) = k_1 (x_0)$ and $\pi (y_1) = y$. Then there is a unique $y_0 \in Y_0$ such that $h_2 (y_0) = y_1$ and $f_0 (y_0) = x_0$. This completes the proof.