fact: Definition subprecategory_of_monics_mor {c' c : C} (f : c' --> c) (isM : isMonic f) : subcategory_of_monics⟦subprecategory_of_monics_ob c', subprecategory_of_monics_ob c⟧ := tpair _ f isM.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Core.Functors