Definition make_graph_mor {G H : pregraph} : ∏ (f₀ : vertex G → vertex H) (f₁ : ∏ x y : vertex G, edge G x y → edge H (f₀ x) (f₀ y)), graph_mor G H := tpair _.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.