Implication Details

Claim: If a category is regular-subobject-trivial, then it has effective cocongruences.

Proof: Let $f,g : X \rightrightarrows E$ be a cocongruence. In particular, there is a morphism $r : E \to X$ with $r f = r g = \id_X$. Since $f$ is a split monomorphism, it is a regular monomorphism. By assumption, $f$ must be an isomorphism. Then $r f = \id_X$ implies that $r = f^{-1}$, and $r g = \id_X$ implies $g = f$. Hence, $f,g$ is a cokernel pair of $\id_X$.

This implication has a dual.