category_theory.regular_mono source