= Solution
A <coherent category> is a <regular category> with finite unions of <subobjects>, including the empty union, stable under pullback. Thus it has <finite limits>, pullback-stable regular-epimorphism/monomorphism image factorizations, and pullback-stable finite joins in each subobject lattice.
Write $U=A\vee B\hookrightarrow X$ and $C=A\wedge B=A\times_XB$. Their inclusions give a commutative square
$$
\begin{array}{ccc}C&\longrightarrow&B\\\downarrow&&\downarrow\\A&\longrightarrow&U.\end{array}
$$
To establish the <pushout> property, take arrows $a:A\to Y$, $b:B\to Y$ agreeing on $C$. Regard their graphs as subobjects of $U\times Y$ and form their union $R$. Internally, this relation says that a point of $U$ is related to its $a$-value when it lies in $A$, or to its $b$-value when it lies in $B$.
The relation is total because every point of $U$ belongs to at least one of $A,B$. It is single-valued: two witnesses in the same summand give the same value by functionality of that map; witnesses in different summands have their shared point in $C$, where the two maps agree. By the relation argument proved in Question 7's unheaded continuation, the projection $R\to U$ is both a regular epimorphism and monic, hence an isomorphism. It consequently gives a map $h:U\to Y$ restricting to $a,b$.
For uniqueness, the equalizer of two possible maps contains $A$ and $B$, hence contains their union $U$ and is all of $U$. Thus the square is a pushout, proving
$$
\boxed{A\vee B\cong A\amalg_{A\wedge B}B}.
$$
This is the <unions of subobjects are pushouts> property; it does not assume arbitrary pushouts already exist in a coherent category.
Back to article page
