Implication Details

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

Proof: In general, the kernel pair of a monomorphism $f : X \to Y$ exists and is given by $$\begin{CD} X @>{\id_X}>> X \\ @V{\id_X}VV @VV{f}V \\ X @>>{f}> Y. \end{CD}$$

This implication has a dual.