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