Lemma montrafotargetbicat_left_unitor_aux1 (vη : montrafotargetbicat_cat): pr2 (I_pretensor montrafotargetbicat_tensor montrafotargetbicat_unit vη) -->[monoidal_cat_left_unitor Mon_V (pr1 vη)] pr2 (functor_identity montrafotargetbicat_cat vη). Proof. unfold mor_disp. unfold trafotargetbicat_disp. hnf. induction vη as [v η]. etrans. 2: { apply maponpaths. cbn. apply idpath. } 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. rewrite hcomp_identity_left. rewrite hcomp_identity_right. 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 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 := pr1 (lax_monoidal_functor_unital FA' v)). cbn in lax_monoidal_functor_unital_inst. rewrite hcomp_identity_right in lax_monoidal_functor_unital_inst. 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 := pr1 (lax_monoidal_functor_unital FA v)). cbn in lax_monoidal_functor_unital_inst. rewrite hcomp_identity_right in lax_monoidal_functor_unital_inst. 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.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrength. Require Import UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory. 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.