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. 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.
Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering.