Lemma graph_mor_id_left {G H : pregraph} (p : graph_mor G H) : graph_mor_comp (graph_mor_id G) p = p. Proof. induction p as (p₀,p₁). apply make_graph_mor_eq. intros. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.