proposition: Lemma has_homsets_graph : has_homsets graph_precategory_ob_mor.
proof: Proof. intros G H. apply isaset_graph_mor. - exact (isaset_vertex H). - exact (isaset_edge H). Defined.
imports: UniMath.Foundations.PartB UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.Graph