Lemma isaprop_is_cgraph_mor {G H : precgraph} (p₀ : node G → node H) (p₁ : arc G → arc H) (h : has_nodeset H) : isaprop (is_cgraph_mor p₀ p₁). Proof. apply isapropdirprod; apply impred_isaprop; intro f; apply h. Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.