proposition: Lemma montrafotargetbicat_disp_leftunitor_data: disp_leftunitor_data montrafotargetbicat_disp_tensor montrafotargetbicat_disp_unit.
proof: Proof. hnf. 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. match goal with | [ |- ?Hl1 • (_ • (?Hl2 • (_ • (_ • (?Hl3 • (_ • (?Hl4 • (_ • (?Hl5 • ?Hl6))))))))) = ?Hr1 • _] => set (l1 := Hl1); set (l2 := Hl2); set (l3 := Hl3); set (l4 := Hl4); set (l5 := Hl5); set (l6 := Hl6); set (r1 := Hr1) end. change (H v ==> H' v) in η. set (l1iso := lwhisker_with_μ_inv_inv2cell I_{Mon_V} v). apply (lhs_left_invert_cell _ _ _ l1iso). cbn. apply (lhs_left_invert_cell _ _ _ (is_invertible_2cell_lassociator _ _ _)). cbn. set (l2iso := lwhisker_rwhisker_with_ϵ_inv_inv2cell v). apply (lhs_left_invert_cell _ _ _ l2iso). cbn. etrans. 2: { repeat rewrite vassocr. rewrite <- rwhisker_lwhisker_rassociator. apply maponpaths_2. repeat rewrite <- vassocr. apply maponpaths. unfold r1. 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 l1 l2 l1iso l2iso r1. etrans. { do 2 apply maponpaths. rewrite vassocr. apply maponpaths_2. apply rwhisker_rwhisker_alt. } clear l3. cbn. etrans. { do 2 apply maponpaths. repeat rewrite vassocr. do 3 apply maponpaths_2. rewrite <- vassocr. apply maponpaths. apply hcomp_hcomp'. } clear l4. unfold hcomp'. etrans. { repeat rewrite <- vassocr. do 4 apply maponpaths. rewrite vassocr. rewrite <- rwhisker_rwhisker. repeat rewrite <- vassocr. apply maponpaths. unfold l5, 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 l5 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.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Categories.Dialgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Monoidal.Displayed.MonoidalSections UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal UniMath.Bicategories.MonoidalCategories.Actions UniMath.Bicategories.MonoidalCategories.ActionBasedStrength UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfCats