proposition: Lemma cgraph_mor_id_left {G H : precgraph} (p : cgraph_mor G H) : cgraph_mor_comp (cgraph_mor_id G) p = p.
proof: Proof. induction p as (p₀,(p₁,h)). apply pair_path_in2. apply pair_path_in2. apply dirprod_paths. - apply funextsec. intro f. cbn. apply pathscomp0rid. - apply funextsec. intro f. cbn. apply pathscomp0rid. Defined.
imports: UniMath.MoreFoundations.Propositions