fact: Definition sub_precategories (C : category) := total2 (fun C' : (hsubtype (ob C)) × (∏ a b:ob C, hsubtype (a --> b)) => is_sub_precategory (pr1 C') (pr2 C')).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos