fact: Definition make_precategory_ob_mor (ob : UU)(mor : ob -> ob -> UU) : precategory_ob_mor := tpair _ ob mor.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations