Balanced categories with pullbacks have strong monomorphisms (source code)

= Balanced categories with pullbacks have strong monomorphisms

In a <balanced category> with <pullbacks in a category>, pull a <monomorphism> back across the bottom map of a lifting square whose left map is an <epimorphism>. The resulting monic projection is epic because its composite with the lifted top map is epic. Balancedness makes that projection invertible, producing the unique lift. Conversely, if all <monomorphisms> are <strong monomorphisms>, applying the lifting property of a bimorphism to its own square gives its inverse, so the <category> is balanced. Pullback stability of epimorphisms is not needed.