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