Lemma montrafotargetbicat_disp_leftunitorinv_data: disp_leftunitorinv_data montrafotargetbicat_disp_tensor montrafotargetbicat_disp_unit. Proof. intros v η. cbn. unfold param_distr_bicat_pentagon_eq_body_variant_RHS, montrafotargetbicat_disp_unit, param_distr_bicat_triangle_eq_variant0_RHS, param_distr_bicat_pentagon_eq_body_RHS. do 3 rewrite <- rwhisker_vcomp. repeat rewrite <- vassocr. apply pathsinv0. match goal with | [ |- ?Hl1 • (?Hl2 • (_ • (?Hl3 • (_ • (_ • (?Hl4 • (_ • (?Hl5 • (_ • ?Hl6))))))))) = _ • ?Hr2] => set (l1 := Hl1); set (l2 := Hl2); set (l3 := Hl3); set (l4 := Hl4); set (l5 := Hl5); set (l6 := Hl6); set (r2 := Hr2) end. change (H v ==> H' v) in η. set (l1iso := lwhisker_with_invlunitor_inv2cell v). apply (lhs_left_invert_cell _ _ _ l1iso). cbn. set (l2iso := lwhisker_with_μ_inv_inv2cell I_{Mon_V} v). apply (lhs_left_invert_cell _ _ _ l2iso). cbn. apply (lhs_left_invert_cell _ _ _ (is_invertible_2cell_lassociator _ _ _)). cbn. set (l3iso := lwhisker_rwhisker_with_ϵ_inv_inv2cell v). apply (lhs_left_invert_cell _ _ _ l3iso). cbn. match goal with | [ |- _ = ?Hl3inv • (_ • (?Hl2inv • (?Hl1inv • _)))] => set (l1inv := Hl1inv); set (l2inv := Hl2inv); set (l3inv := Hl3inv) end. clear l1 l2 l3 l1iso l2iso l3iso. etrans. 2: { repeat rewrite vassocr. do 4 apply maponpaths_2. unfold l3inv. apply rwhisker_lwhisker_rassociator. } etrans. 2: { do 2 apply maponpaths_2. repeat rewrite <- vassocr. apply maponpaths. unfold l2inv, l1inv. do 2 rewrite lwhisker_vcomp. apply maponpaths. rewrite vassocr. assert (lax_monoidal_functor_unital_inst := fmonoidal_preservesleftunitality FA'm v). cbn in lax_monoidal_functor_unital_inst. apply pathsinv0. exact lax_monoidal_functor_unital_inst. } clear l1inv l2inv l3inv. etrans. { do 2 apply maponpaths. repeat rewrite vassocr. do 3 apply maponpaths_2. apply rwhisker_rwhisker_alt. } cbn. etrans. { do 2 apply maponpaths. do 2 apply maponpaths_2. rewrite <- vassocr. apply maponpaths. apply hcomp_hcomp'. } clear l4 l5. unfold hcomp'. set (r2iso := rwhisker_with_invlunitor_inv2cell v). apply pathsinv0. apply (lhs_right_invert_cell _ _ _ r2iso). apply pathsinv0. cbn. clear r2 r2iso. etrans. { repeat rewrite <- vassocr. do 4 apply maponpaths. rewrite vassocr. rewrite <- rwhisker_rwhisker. repeat rewrite <- vassocr. apply maponpaths. unfold l6. do 2 rewrite rwhisker_vcomp. apply maponpaths. apply pathsinv0. rewrite vassocr. assert (lax_monoidal_functor_unital_inst := fmonoidal_preservesleftunitality FAm v). cbn in lax_monoidal_functor_unital_inst. apply pathsinv0. exact lax_monoidal_functor_unital_inst. } clear l6. rewrite lunitor_lwhisker. apply maponpaths. apply (lhs_left_invert_cell _ _ _ (rwhisker_with_linvunitor_inv2cell v)). cbn. rewrite lunitor_triangle. rewrite vcomp_lunitor. rewrite vassocr. apply maponpaths_2. apply (lhs_left_invert_cell _ _ _ (is_invertible_2cell_rassociator _ _ _)). cbn. apply pathsinv0, lunitor_triangle. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.MonoidalSections. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrength. Require Import UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Import Bicat.Notations. Import BifunctorNotations. Import DisplayedBifunctorNotations. Import MonoidalNotations. Section FromMonoidalSectionBicat. End FromMonoidalSectionBicat. Section FromMonoidalSection. End FromMonoidalSection.