Lemma cgraph_mor_eq {G H : cgraph} (p q : cgraph_mor G H) (e₀ : ∏ x : node G, onnode p x = onnode q x) (e₁ : ∏ f : arc G, onarc p f = onarc q f) : p = q. Proof. apply cgraph_mor_eq_aux. - apply funextfun. exact e₀. - apply funextfun. exact e₁. - apply isaset_node. Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.