Binary-product criterion for lifting-only strong epimorphisms (source code)

= Binary-product criterion for lifting-only strong epimorphisms

In a <category> with binary <products in a category>, a map with the <left lifting property against monomorphisms> is an <epimorphism>. If $ue=ve$, lift the square with right side $\Delta$ and bottom side $\langle u,v\rangle$. The two projections of its filler give $u=v$. This argument does not require <equalizers>.