Implication Details

Assumptions: effective congruences, extensive

Reason: Let $\alpha : A \hookrightarrow B$ be a monomorphism. Let $B'$ be a copy of $B$ , and likewise let $A'$ be a copy of $A$ . Consider the congruence on $B + B'$ generated by $y \sim y'$ for $y \in A$ . Formally, we define $E := B + B' + A + A'$ and define the two morphisms $f, g : E \rightrightarrows B + B'$ by extending the identity on $B + B'$ and $\begin{align*} f(y) & = \alpha(y), & f(y') & = \alpha(y)', \\ g(y) & = \alpha(y)', & g(y') & = \alpha(y), \end{align*}$ on generalized elements. Extensivity can be used to show that $f, g$ are jointly monomorphic. Clearly, the pair $f, g$ is reflexive and symmetric. For transitivity, one once again uses extensivity. By assumption, there is a morphism $h : B + B' \to C$ such that $f, g$ is the kernel pair of $h$ , that is, two generalized elements $x, y \in B + B'$ satisfy $h(x) = h(y)$ if and only if $x = f(e)$ , $y = g(e)$ for some $e \in E$ . In particular, for $x \in B$ , we have $h(x) = h(x')$ if and only if $x = f(e)$ , $x' = g(e)$ for some $e \in E$ . By disjointness of coproducts, we must necessarily have $e \in A$ , and $x = \alpha(e)$ . This shows that $\alpha$ is the equalizer of $h \circ i_1, h \circ i_2 : B \rightrightarrows C$ .