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. 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.
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.