Lemma cgraph_mor_id_left {G H : precgraph} (p : cgraph_mor G H) : cgraph_mor_comp (cgraph_mor_id G) p = p. 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.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.