Definition onedge {G H : pregraph} (p : graph_mor G H) {x y : vertex G} : edge G x y → edge H (onvertex p x) (onvertex p y) := pr2 p x y.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.