fact: Definition pregraph_category : precategory := make_precategory pregraph_precategory_data is_precategory_pregraph.
imports: UniMath.Foundations.PartB UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.Graph