We claim that $A\mathbin {\textstyle \coprod _{C}}B$ is the categorical pushout of $A$ and $B$ over $C$ with respect to $\webleft (f,g\webright )$ in $\mathsf{Sets}$. First we need to check that the relevant pushout diagram commutes, i.e. that we have
Indeed, given $c\in C$, we have
\begin{align*} \webleft [\mathrm{inj}_{1}\circ f\webright ]\webleft (c\webright ) & = \mathrm{inj}_{1}\webleft (f\webleft (c\webright )\webright )\\ & = \webleft [\webleft (0,f\webleft (c\webright )\webright )\webright ]\\ & = \webleft [\webleft (1,g\webleft (c\webright )\webright )\webright ]\\ & = \mathrm{inj}_{2}\webleft (g\webleft (c\webright )\webright )\\ & = \webleft [\mathrm{inj}_{2}\circ g\webright ]\webleft (c\webright ),\end{align*}
where $\webleft [\webleft (0,f\webleft (c\webright )\webright )\webright ]=\webleft [\webleft (1,g\webleft (c\webright )\webright )\webright ]$ by the definition of the relation $\mathord {\sim }$ on $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$. Next, we prove that $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{C}B$ satisfies the universal property of the pushout. Suppose we have a diagram of the form
in $\mathsf{Sets}$. Then there exists a unique map $\phi \colon A\mathbin {\textstyle \coprod _{C}}B\to P$ making the diagram
commute, being uniquely determined by the conditions
\begin{align*} \phi \circ \mathrm{inj}_{1} & = \iota _{1},\\ \phi \circ \mathrm{inj}_{2} & = \iota _{2} \end{align*}
via
\[ \phi \webleft (x\webright )=\begin{cases} \iota _{1}\webleft (a\webright ) & \text{if $x=\webleft [\webleft (0,a\webright )\webright ]$,}\\ \iota _{2}\webleft (b\webright ) & \text{if $x=\webleft [\webleft (1,b\webright )\webright ]$} \end{cases} \]
for each $x\in A\mathbin {\textstyle \coprod _{C}}B$, where the well-definedness of $\phi $ is guaranteed by the equality $\iota _{1}\circ f=\iota _{2}\circ g$ and the definition of the relation $\mathord {\sim }$ on $A\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}B$ as follows:
-
Case 1: Suppose we have $x=\webleft [\webleft (0,a\webright )\webright ]=\webleft [\webleft (0,a'\webright )\webright ]$ for some $a,a'\in A$. Then, by Remark 2.2.4.1.3, we have a sequence
\[ \webleft (0,a\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (0,a'\webright ). \]
-
Case 2: Suppose we have $x=\webleft [\webleft (1,b\webright )\webright ]=\webleft [\webleft (1,b'\webright )\webright ]$ for some $b,b'\in B$. Then, by Remark 2.2.4.1.3, we have a sequence
\[ \webleft (1,b\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (1,b'\webright ). \]
-
Case 3: Suppose we have $x=\webleft [\webleft (0,a\webright )\webright ]=\webleft [\webleft (1,b\webright )\webright ]$ for some $a\in A$ and $b\in B$. Then, by Remark 2.2.4.1.3, we have a sequence
\[ \webleft (0,a\webright )\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (1,b\webright ). \]
In all these cases, we declare $x\sim 'y$ iff there exists some $c\in C$ such that $x=\webleft (0,f\webleft (c\webright )\webright )$ and $y=\webleft (1,g\webleft (c\webright )\webright )$ or $x=\webleft (1,g\webleft (c\webright )\webright )$ and $y=\webleft (0,f\webleft (c\webright )\webright )$. Then, the equality $\iota _{1}\circ f=\iota _{2}\circ g$ gives
\begin{align*} \phi \webleft (\webleft [x\webright ]\webright ) & = \phi \webleft (\webleft [\webleft (0,f\webleft (c\webright )\webright )\webright ]\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\iota _{1}\webleft (f\webleft (c\webright )\webright )\\ & = \iota _{2}\webleft (g\webleft (c\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\phi \webleft (\webleft [\webleft (1,g\webleft (c\webright )\webright )\webright ]\webright )\\ & = \phi \webleft (\webleft [y\webright ]\webright ), \end{align*}
with the case where $x=\webleft (1,g\webleft (c\webright )\webright )$ and $y=\webleft (0,f\webleft (c\webright )\webright )$ similarly giving $\phi \webleft (\webleft [x\webright ]\webright )=\phi \webleft (\webleft [y\webright ]\webright )$. Thus, if $x\sim 'y$, then $\phi \webleft (\webleft [x\webright ]\webright )=\phi \webleft (\webleft [y\webright ]\webright )$. Applying this equality pairwise to the sequences
\begin{align*} \webleft (0,a\webright )& \sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (0,a'\webright ),\\ \webleft (1,b\webright )& \sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim '\webleft (1,b'\webright ),\\ \webleft (0,a\webright )& \sim ’x_{1}\sim ’\cdots \sim ’x_{n}\sim ’\webleft (1,b\webright )\end{align*}
gives
\begin{align*} \phi \webleft (\webleft [\webleft (0,a\webright )\webright ]\webright ) & = \phi \webleft (\webleft [\webleft (0,a'\webright )\webright ]\webright ),\\ \phi \webleft (\webleft [\webleft (1,b\webright )\webright ]\webright ) & = \phi \webleft (\webleft [\webleft (1,b'\webright )\webright ]\webright ),\\ \phi \webleft (\webleft [\webleft (0,a\webright )\webright ]\webright ) & = \phi \webleft (\webleft [\webleft (1,b\webright )\webright ]\webright ), \end{align*}
showing $\phi $ to be well-defined.
