Definition graph_mor (G H : pregraph) : UU := ∑ (f₀ : vertex G → vertex H), (∏ x y : vertex G, edge G x y → edge H (f₀ x) (f₀ y)).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.