Lemma disp_lassociator_to_rassociator_post {a b c d : C} {f : C⟦a,b⟧} {g : C⟦b,c⟧} {h : C⟦c,d⟧} {k : C⟦a,d⟧} {x : k ==> (f · g) · h} {y : k ==> f · (g · h)} {aa : D a} {bb : D b} {cc : D c} {dd : D d} {ff : aa -->[f] bb} {gg : bb -->[g] cc} {hh : cc -->[h] dd} {kk : aa -->[k] dd} (xx : kk ==>[x] (ff ;; gg) ;; hh) (yy : kk ==>[y] ff ;; (gg ;; hh)) (q : x • rassociator f g h = y) (p := rassociator_to_lassociator_post _ _ q : x = y • lassociator f g h) (pp : xx = transportb (λ x, _ ==>[x] _) p (yy •• disp_lassociator ff gg hh)) : xx •• disp_rassociator ff gg hh = transportb (λ x, _ ==>[x] _) q (yy). Proof. etrans. { use disp_lassociator_to_rassociator_post'. - exact y. - exact p. - exact yy. - exact pp. } apply maponpaths_2. apply cellset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence.