proposition: Lemma disp_lunitor_lwhisker {a b c : C} {f : C⟦a,b⟧} {g : C⟦b,c⟧} {aa : D a} {bb : D b} {cc : D c} (ff : aa -->[f] bb) (gg : bb -->[g] cc) : (disp_rassociator _ _ _ •• (ff ◃◃ disp_lunitor gg)) = transportb (λ α, _ ==>[α] _) (lunitor_lwhisker _ _) (disp_runitor ff ▹▹ gg).
proof: Proof. etrans. { use disp_lassociator_to_rassociator_pre. - exact (runitor f ▹ g). - exact (disp_runitor ff ▹▹ gg). - apply lunitor_lwhisker. - apply pathsinv0. etrans. { apply maponpaths. apply disp_runitor_rwhisker. } etrans. { apply (transport_f_f (λ α, _ ==>[α] _)). } apply (transportf_set (λ α, _ ==>[α] _)). apply cellset_property. } apply maponpaths_2, 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