fact: Definition precategory_source (C : precategory_ob_mor) : total_morphisms C -> ob C := λ abf, pr1 (pr1 abf).
imports: UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Setcategories