Lemma cgraph_mor_comp_assoc {G1 G2 G3 G4 : precgraph} (p : cgraph_mor G1 G2) (q : cgraph_mor G2 G3) (r : cgraph_mor G3 G4) : cgraph_mor_comp p (cgraph_mor_comp q r) = cgraph_mor_comp (cgraph_mor_comp p q) r. Proof. induction p as (p₀,(p₁,h)). induction q as (q₀,(q₁,k)). induction r as (r₀,(r₁,l)). apply pair_path_in2. apply pair_path_in2. apply dirprod_paths; cbn. - apply funextsec. intro f. etrans. { apply pathsinv0, path_assoc. } apply maponpaths. apply pathsinv0. etrans. { apply maponpathscomp0. } apply maponpaths. apply maponpathscomp. - apply funextsec. intro f. etrans. { apply pathsinv0, path_assoc. } apply maponpaths. apply pathsinv0. etrans. { apply maponpathscomp0. } apply maponpaths. apply maponpathscomp. Defined.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.Combinatorics.Graph.