Lemma runitor_rwhisker_rwhisker {a b c d: C} (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧) : (rassociator f g (identity c) ▹ h) • ((f ◃ runitor g) ▹ h) = runitor (f · g) ▹ h. Proof. apply pathsinv0. etrans. { apply pathsinv0. apply lunitor_lwhisker. } apply (vcomp_rcancel (rassociator _ _ _ )). { apply is_invertible_2cell_rassociator. } etrans. { apply vassocl. } etrans. { apply maponpaths. apply pathsinv0, lwhisker_lwhisker_rassociator. } apply pathsinv0. etrans. { apply vassocl. } etrans. { apply maponpaths. apply pathsinv0, rwhisker_lwhisker_rassociator. } etrans. { do 3 apply maponpaths. apply pathsinv0. apply lunitor_lwhisker. } etrans. { do 2 apply maponpaths. apply pathsinv0, lwhisker_vcomp. } etrans. { apply vassocr. } etrans. { apply vassocr. } apply pathsinv0. etrans. { apply vassocr. } apply maponpaths_2. use inv_cell_eq. - use is_invertible_2cell_vcomp. + apply is_invertible_2cell_rassociator. + apply is_invertible_2cell_rassociator. - use is_invertible_2cell_vcomp. + use is_invertible_2cell_vcomp. * apply is_invertible_2cell_rwhisker. apply is_invertible_2cell_rassociator. * apply is_invertible_2cell_rassociator. + apply is_invertible_2cell_lwhisker. apply is_invertible_2cell_rassociator. - cbn. apply pathsinv0. etrans. { apply vassocr. } apply lassociator_lassociator. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.OpMorBicat. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat.