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