proposition: Lemma assoc4_disp {C: category} {D: disp_cat C} {a b c d e: C} {da: D a} {db: D b} {dc: D c} {dd: D d} {de: D e} {f: a--> b} {g: b --> c} {h: c --> d} {i: d --> e} (df: da -->[f] db) (dg: db -->[g] dc) (dh: dc -->[h] dd) (di: dd -->[i] de) : df ;; dg ;; dh ;; di = transportb _ (assoc4 C a b c d e f g h i) (df ;; (dg ;; dh) ;; di).
proof: Proof. rewrite assoc_disp. unfold transportb. rewrite mor_disp_transportf_postwhisker. apply PartA.transportb_transpose_right. apply (maponpaths (λ e, transportf _ e _)). apply uip. apply homset_property. Qed.
imports: UniMath.Foundations.Sets UniMath.Foundations.PartD UniMath.MoreFoundations.PartA UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering