Definition graph_mor_comp {G H K: pregraph} (p : graph_mor G H) (q : graph_mor H K) : graph_mor G K := make_graph_mor (onvertex q ∘ onvertex p) (λ (x y : vertex G) (f : edge G x y), onedge q (pr2 p x y f)).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.