Lemma disp_lassociator_to_rassociator_pre {a b c d : C} {f : C⟦a,b⟧} {g : C⟦b,c⟧} {h : C⟦c, d⟧} {k : C⟦a,d⟧} {x : f · (g · h) ==> k} {y : (f · g) · h ==> k} {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 : ff ;; (gg ;; hh) ==>[x] kk) (yy : (ff ;; gg) ;; hh ==>[y] kk) (q : rassociator f g h • x = y) (p := rassociator_to_lassociator_pre _ _ q : x = lassociator f g h • y) (pp : xx = transportb (λ x, _ ==>[x] _) p (disp_lassociator ff gg hh •• yy)) : disp_rassociator ff gg hh •• xx = transportb (λ x, _ ==>[x] _) q (yy). Proof. etrans. { use disp_lhs_left_invert_cell. - exact y. - apply is_invertible_2cell_rassociator. - exact yy. - apply is_disp_invertible_2cell_rassociator. - apply lassociator_to_rassociator_pre. exact p. - cbn. etrans. { apply pp. } apply maponpaths_2. apply cellset_property. } 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.