proposition: Lemma isaset_cgraph_mor {G H : precgraph} (h : has_nodeset H) (k : has_arcset H) : isaset (cgraph_mor G H).
proof: 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.
imports: UniMath.MoreFoundations.Propositions