proposition: 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: Proof. etrans. { use disp_lassociator_to_rassociator_post'. - exact y. - exact p. - exact yy. - exact pp. } apply maponpaths_2. apply cellset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence