Definition graph_mor_id (G : pregraph) : graph_mor G G := make_graph_mor (idfun (vertex G)) (λ x y : vertex G, idfun (edge G x y)).
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.