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

definition. monic [kostecki2011introduction, 2.1] [tt-000B]

An arrow \(f : X \to Y\) is monic if the diagram commutes, i.e. \(g_1 \mathbin {\bullet } f = g_2 \mathbin {\bullet } f \implies g_1 = g_2\), denoted \(f : X \rightarrowtail Y\).

"Monic" is short for "monomorphism", which is a generalization of the concept of injective (one-to-one) functions between sets.