Lemma graph_mor_comp_assoc {G1 G2 G3 G4 : pregraph} (p : graph_mor G1 G2) (q : graph_mor G2 G3) (r : graph_mor G3 G4) : graph_mor_comp p (graph_mor_comp q r) = graph_mor_comp (graph_mor_comp p q) r. Proof. induction p as (p₀,p₁). induction q as (q₀,q₁). induction r as (r₀,r₁). apply make_graph_mor_eq. intros. apply idpath. Qed.
Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Propositions.