CatDat

Implication Details

Assumptions: effective congruences, extensive

Conclusions: mono-regular

Proof: 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 \coloneqq 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$.