[proofplan] Given a span $b \xleftarrow{f} a \xrightarrow{g} c$, we first combine the two target objects by forming the binary coproduct $b \coprod c$. The two maps from $a$ into this coproduct, obtained by following $f$ and $g$ with the coproduct injections, are then forced to agree by taking their coequalizer. The resulting object receives maps from $b$ and $c$, and the universal property of the coproduct together with the universal property of the coequalizer gives exactly the universal property of the pushout. [/proofplan] [step:Form the coequalizer of the two induced maps into the coproduct] Let $f: a \to b$ and $g: a \to c$ be morphisms in $\mathcal{C}$. Since $\mathcal{C}$ has binary coproducts, choose a coproduct object $b \coprod c$ with coproduct injections \begin{align*} \iota_b: b \to b \coprod c, \qquad \iota_c: c \to b \coprod c. \end{align*} Define two morphisms \begin{align*} \alpha: a \to b \coprod c, \qquad \beta: a \to b \coprod c \end{align*} by \begin{align*} \alpha := \iota_b \circ f, \qquad \beta := \iota_c \circ g. \end{align*} Since $\mathcal{C}$ has coequalizers, choose a coequalizer of $\alpha$ and $\beta$: \begin{align*} q: b \coprod c \to p. \end{align*} Thus \begin{align*} q \circ \alpha = q \circ \beta, \end{align*} and for every object $x$ of $\mathcal{C}$ and every morphism $h: b \coprod c \to x$ satisfying $h \circ \alpha = h \circ \beta$, there exists a unique morphism $\overline{h}: p \to x$ such that \begin{align*} \overline{h} \circ q = h. \end{align*} [/step] [step:Define the candidate pushout cocone and verify commutativity] Define morphisms \begin{align*} j_b: b \to p, \qquad j_c: c \to p \end{align*} by \begin{align*} j_b := q \circ \iota_b, \qquad j_c := q \circ \iota_c. \end{align*} Using the definitions of $\alpha$ and $\beta$, and then the coequalizer relation for $q$, we compute \begin{align*} j_b \circ f &= q \circ \iota_b \circ f \\ &= q \circ \alpha \\ &= q \circ \beta \\ &= q \circ \iota_c \circ g \\ &= j_c \circ g. \end{align*} Therefore $(p, j_b, j_c)$ is a cocone over the span $b \xleftarrow{f} a \xrightarrow{g} c$. [/step] [step:Construct the unique mediating morphism for every compatible cocone] Let $x$ be an object of $\mathcal{C}$, and let \begin{align*} u: b \to x, \qquad v: c \to x \end{align*} be morphisms satisfying the compatibility condition \begin{align*} u \circ f = v \circ g. \end{align*} By the universal property of the coproduct $b \coprod c$, there exists a unique morphism \begin{align*} h: b \coprod c \to x \end{align*} such that \begin{align*} h \circ \iota_b = u, \qquad h \circ \iota_c = v. \end{align*} This morphism coequalizes $\alpha$ and $\beta$, because \begin{align*} h \circ \alpha &= h \circ \iota_b \circ f \\ &= u \circ f \\ &= v \circ g \\ &= h \circ \iota_c \circ g \\ &= h \circ \beta. \end{align*} By the universal property of the coequalizer $q: b \coprod c \to p$, there exists a unique morphism \begin{align*} w: p \to x \end{align*} such that \begin{align*} w \circ q = h. \end{align*} For this morphism $w$, we have \begin{align*} w \circ j_b &= w \circ q \circ \iota_b \\ &= h \circ \iota_b \\ &= u, \end{align*} and similarly \begin{align*} w \circ j_c &= w \circ q \circ \iota_c \\ &= h \circ \iota_c \\ &= v. \end{align*} [guided] We must show that every compatible pair of arrows from $b$ and $c$ factors uniquely through the object $p$ constructed from the coequalizer. Start with an arbitrary object $x$ and morphisms \begin{align*} u: b \to x, \qquad v: c \to x \end{align*} such that \begin{align*} u \circ f = v \circ g. \end{align*} The coproduct $b \coprod c$ is designed precisely to combine maps out of $b$ and $c$ into one map. Hence the universal property of the coproduct gives a unique morphism \begin{align*} h: b \coprod c \to x \end{align*} with \begin{align*} h \circ \iota_b = u, \qquad h \circ \iota_c = v. \end{align*} Now we check that this single morphism $h$ respects the equivalence imposed by the coequalizer. The two maps out of $a$ are \begin{align*} \alpha = \iota_b \circ f, \qquad \beta = \iota_c \circ g. \end{align*} Therefore \begin{align*} h \circ \alpha &= h \circ \iota_b \circ f \\ &= u \circ f \\ &= v \circ g \\ &= h \circ \iota_c \circ g \\ &= h \circ \beta. \end{align*} The middle equality is exactly the compatibility condition on the cocone $(u,v)$. Thus $h$ coequalizes $\alpha$ and $\beta$. Since $q: b \coprod c \to p$ is the coequalizer of $\alpha$ and $\beta$, every morphism out of $b \coprod c$ that coequalizes $\alpha$ and $\beta$ factors uniquely through $q$. Applying this to $h$, there is a unique morphism \begin{align*} w: p \to x \end{align*} such that \begin{align*} w \circ q = h. \end{align*} This morphism has the required values on $b$ and $c$: \begin{align*} w \circ j_b &= w \circ q \circ \iota_b \\ &= h \circ \iota_b \\ &= u, \end{align*} and \begin{align*} w \circ j_c &= w \circ q \circ \iota_c \\ &= h \circ \iota_c \\ &= v. \end{align*} So $w$ is a mediating morphism from the candidate pushout object $p$ to $x$. [/guided] [/step] [step:Prove uniqueness of the mediating morphism and conclude the pushout property] Let $w': p \to x$ be any morphism satisfying \begin{align*} w' \circ j_b = u, \qquad w' \circ j_c = v. \end{align*} Then \begin{align*} (w' \circ q) \circ \iota_b &= w' \circ q \circ \iota_b \\ &= w' \circ j_b \\ &= u, \end{align*} and \begin{align*} (w' \circ q) \circ \iota_c &= w' \circ q \circ \iota_c \\ &= w' \circ j_c \\ &= v. \end{align*} The morphism $h: b \coprod c \to x$ was the unique morphism satisfying \begin{align*} h \circ \iota_b = u, \qquad h \circ \iota_c = v, \end{align*} so the preceding two equalities imply \begin{align*} w' \circ q = h. \end{align*} But $w: p \to x$ was the unique morphism satisfying $w \circ q = h$ by the coequalizer property of $q$. Hence $w' = w$. Thus, for every compatible cocone $(u,v)$ from the span $b \xleftarrow{f} a \xrightarrow{g} c$ to an object $x$, there exists a unique morphism $w: p \to x$ with \begin{align*} w \circ j_b = u, \qquad w \circ j_c = v. \end{align*} Therefore $(p,j_b,j_c)$ is a pushout of $f$ and $g$. Since the span $b \xleftarrow{f} a \xrightarrow{g} c$ was arbitrary, $\mathcal{C}$ has all pushouts. [/step]