CatDat

Implication Details

Claim: If a category has kernel pairs and is right cancellative, then it is left cancellative.

Proof: Let $f : X \to Y$ be a morphism with kernel pair $E \rightrightarrows X$. The diagonal $X \to E$ is a split monomorphism. By assumption on the category, it is also an epimorphism. Thus, it is an isomorphism. Therefore, $$\begin{CD} X @>{\id_X}>> X \\ @V{\id_X}VV @VV{f}V \\ X @>>{f}> Y. \end{CD}$$ is a pullback, so $f$ is a monomorphism.