fact: 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)).
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions