Lemma make_graph_mor_eq {G H : pregraph} (p₀ : vertex G → vertex H) (p₁ p₁' : ∏ x y : vertex G, edge G x y → edge H (p₀ x) (p₀ y)) (e : ∏ x y (f : edge G x y), p₁ x y f = p₁' x y f) : make_graph_mor p₀ p₁ = make_graph_mor p₀ p₁'. Proof. apply pair_path_in2. apply funextsec. intro x. apply funextsec. intro y. apply funextfun. intro f. apply e. Defined.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.