Implication Details

Assumptions: binary products, coreflexive equalizers

Conclusions: equalizers

Reason: If f,g:X⇉Yf,g : X \rightrightarrows Y are two morphisms, we have a coreflexive pair (idX,f),(idX,g):X⇉X×Y(\mathrm{id}_X,f), (\mathrm{id}_X,g) : X \rightrightarrows X \times Y. A morphism with codomain XX equalizes ff and gg if and only if it equalizes (idX,f)(\mathrm{id}_X,f) and (idX,g)(\mathrm{id}_X,g). Thus, their equalizers agree.