Lemma has_homsets_graph : has_homsets cgraph_precategory_ob_mor. Proof. intros G H. apply isaset_cgraph_mor. - exact (isaset_node H). - exact (isaset_arc H). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.Combinatorics.CGraph.