CatDat

Implication Details

Claim: If a category has binary products and has coreflexive equalizers, then it has equalizers.

Proof: If $f,g : X \rightrightarrows Y$ are two morphisms, we have a coreflexive pair $(\id_X,f), (\id_X,g) : X \rightrightarrows X \times Y$. A morphism with codomain $X$ equalizes $f$ and $g$ if and only if it equalizes $(\id_X,f)$ and $(\id_X,g)$. Thus, their equalizers agree.