NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

lemma. monic and pullback [leinster2016basic, 5.1.32] [tt-003J]

An arrow \(X \xrightarrow {f} Y\) is monic iff the square is a pullback.

The significance of this lemma is that whenever we prove a result about limits, a result about monics will follow.