Lemma montrafotargetbicat_tensor_comp_aux_inst1 (v w w' : V) (g : V ⟦ w, w' ⟧) (η : G · FA' v ==> FA v · G) (π : G · FA' w ==> FA w · G) (π' : G · FA' w' ==> FA w' · G): π • (# FA g ▹ G) = (G ◃ # FA' g) • π' → param_distr_bicat_pentagon_eq_body_variant_RHS v w η π • (# FA (v ⊗^{ Mon_V}_{l} g) ▹ G) = (G ◃ # FA' (v ⊗^{ Mon_V}_{l} g)) • param_distr_bicat_pentagon_eq_body_variant_RHS v w' η π'. Proof. intro Hyp'. rewrite <- (when_bifunctor_becomes_leftwhiskering Mon_V). change (montrafotargetbicat_disp v) in η. exact (montrafotargetbicat_tensor_comp_aux v w v w' (identity v) g η π η π' (id_disp η) Hyp'). 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.