Lemma isaset_cgraph_mor {G H : precgraph} (h : has_nodeset H) (k : has_arcset H) : isaset (cgraph_mor G H). Proof. apply isaset_total2. - exact (funspace_isaset h). - intro p₀. apply isaset_total2. + exact (funspace_isaset k). + intro p₁. apply isasetaprop. apply isaprop_is_cgraph_mor. exact h. Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.