Lemma montrafotargetbicat_tensor_comp_aux (v w v' w': V) (f: V⟦v,v'⟧) (g: V⟦w,w'⟧) (η : montrafotargetbicat_disp v) (π : montrafotargetbicat_disp w) (η' : montrafotargetbicat_disp v') (π' : montrafotargetbicat_disp w') (Hyp: η -->[ f] η') (Hyp': π -->[ g] π'): param_distr_bicat_pentagon_eq_body_variant_RHS v w η π -->[ f ⊗^{Mon_V} g] param_distr_bicat_pentagon_eq_body_variant_RHS v' w' η' π'. Proof. hnf in Hyp, Hyp' |- *. unfold param_distr_bicat_pentagon_eq_body_variant_RHS, param_distr_bicat_pentagon_eq_body_RHS. match goal with | [ |- (?Hαinv • (?Hassoc1 • ((?Hγ • (?Hassoc2 • ?Hδ)) • (?Hassoc3 • ?Hβ)))) · ?Hε = _ ] => set (αinv := Hαinv); set (γ := Hγ); set (δ:= Hδ); set (β := Hβ); set (ε1 := Hε) end. cbn in αinv, β. match goal with | [ |- _ = ?Hε · (?Hαinv • (?Hassoc4 • ((?Hγ • (?Hassoc5 • ?Hδ) • (?Hassoc6 • ?Hβ))))) ] => set (αinv' := Hαinv); set (γ' := Hγ); set (δ':= Hδ); set (β' := Hβ); set (ε2 := Hε) end. cbn in αinv', β'. set (αinviso := lwhisker_with_μ_inv_inv2cell v w). cbn in αinviso. etrans. { apply pathsinv0. apply vassocr. } apply (lhs_left_invert_cell _ _ _ αinviso). apply pathsinv0. unfold inv_cell. set (α := lwhisker G (fmonoidal_preservestensordata FA'm v w)). cbn in α. match goal with | [ |- ?Hαcand • _ = _ ] => set (αcand := Hαcand) end. change αcand with α. clear αcand. assert (μFA'natinst := full_naturality_condition (pr2 (preservestensor_is_nattrans (fmonoidal_preservestensornatleft FA'm) (fmonoidal_preservestensornatright FA'm))) f g). cbn in μFA'natinst. unfold make_binat_trans_data in μFA'natinst. assert (μFAnatinst := full_naturality_condition (pr2 (preservestensor_is_nattrans (fmonoidal_preservestensornatleft FAm) (fmonoidal_preservestensornatright FAm))) f g). cbn in μFAnatinst. unfold make_binat_trans_data in μFAnatinst. unfold H in ε2. cbn in ε2. etrans. { apply vassocr. } apply (maponpaths (lwhisker G)) in μFA'natinst. apply pathsinv0 in μFA'natinst. etrans. { apply maponpaths_2. apply lwhisker_vcomp. } etrans. { apply maponpaths_2. unfold functoronmorphisms1. rewrite (functor_comp FA'). exact μFA'natinst. } clear ε2 μFA'natinst. etrans. { apply maponpaths_2. apply pathsinv0. apply lwhisker_vcomp. } etrans. { apply pathsinv0. apply vassocr. } etrans. { apply maponpaths. rewrite vassocr. apply maponpaths_2. unfold αinv'. apply lwhisker_vcomp. } etrans. { apply maponpaths. apply maponpaths_2. apply maponpaths. apply (pr12 (fmonoidal_preservestensorstrongly FA'm v' w')). } clear αinv αinv' αinviso α. unfold H' in ε1. cbn in ε1. cbn. rewrite lwhisker_id2. rewrite id2_left. match goal with | [ |- ?Hσ • _ = _ ] => set (σ' := Hσ) end. etrans. 2: { repeat rewrite <- vassocr. apply idpath. } apply (maponpaths (rwhisker G)) in μFAnatinst. etrans. 2: { do 5 apply maponpaths. apply pathsinv0. apply rwhisker_vcomp. } etrans. 2: { do 5 apply maponpaths. unfold functoronmorphisms1. rewrite (functor_comp FA). exact μFAnatinst. } clear β μFAnatinst ε1. etrans. 2: { do 5 apply maponpaths. apply rwhisker_vcomp. } match goal with | [ |- _ = _ • (_ • (_ • (_ • (_ • (_ • ?Hβ'twin))))) ] => set (β'twin := Hβ'twin) end. change β'twin with β'. clear β'twin. repeat rewrite vassocr. apply maponpaths_2. clear β'. unfold σ'. assert (hcomp_aux:= hcomp_hcomp' (# FA' f) (# FA' g)). unfold hcomp, hcomp' in hcomp_aux. etrans. { do 5 apply maponpaths_2. apply maponpaths. apply hcomp_aux. } clear hcomp_aux σ'. rewrite <- lwhisker_vcomp. match goal with | [ |- (((((?Hσ'1 • ?Hσ'2) • _) • _) • _) • _) • _ = _ • ?Hσ ] => set (σ'1 := Hσ'1); set (σ'2 := Hσ'2); set (σ := Hσ) end. change (η • # H' f = # H f • η') in Hyp. apply (maponpaths (rwhisker (FA' w'))) in Hyp. do 2 rewrite <- rwhisker_vcomp in Hyp. apply pathsinv0 in Hyp. assert (Hypvariant: σ'2 • lassociator G (FA' v') (FA' w') • γ' = lassociator G (FA' v) (FA' w') • (rwhisker (FA' w') η • rwhisker (FA' w') (# H' f))). { apply (maponpaths (vcomp2 (lassociator G (FA' v) (FA' w')))) in Hyp. etrans. 2: { exact Hyp. } rewrite vassocr. apply maponpaths_2. rewrite Hmorok. apply rwhisker_lwhisker. } clear Hyp. intermediate_path (σ'1 • ((σ'2 • lassociator G (FA' v') (FA' w')) • γ') • rassociator (FA v') G (FA' w') • δ' • lassociator (FA v') (FA w') G). { repeat rewrite <- vassocr. apply idpath. } rewrite Hypvariant. clear σ'2 γ' Hypvariant. assert (σ'1ok : σ'1 • lassociator G (FA' v) (FA' w') = lassociator G (FA' v) (FA' w) • (H v ◃ # FA' g)). { apply lwhisker_lwhisker. } etrans. { repeat rewrite vassocr. rewrite σ'1ok. apply idpath. } clear σ'1 σ'1ok. repeat rewrite <- vassocr. apply maponpaths. etrans. { repeat rewrite vassocr. do 4 apply maponpaths_2. apply pathsinv0. apply hcomp_hcomp'. } unfold hcomp. repeat rewrite <- vassocr. apply maponpaths. clear γ. change (π • # H' g = # H g • π') in Hyp'. apply (maponpaths (lwhisker (FA v))) in Hyp'. do 2 rewrite <- lwhisker_vcomp in Hyp'. rewrite H'morok in Hyp'. assert (Hyp'variant: δ • lassociator (FA v) (FA w) G • ((FA v ◃ # FA g) ▹ G) = ((FA v ◃ # H g) • (FA v ◃ π')) • lassociator (FA v) (FA w') G). { apply (maponpaths (fun x => x • lassociator (FA v) (FA w') G)) in Hyp'. etrans. { rewrite <- vassocr. apply maponpaths. apply pathsinv0. apply rwhisker_lwhisker. } rewrite vassocr. exact Hyp'. } clear Hyp'. set (σbetter := hcomp' (# FA f) (# FA g) ▹ G). assert (σbetterok : σ = σbetter). { apply maponpaths. apply hcomp_hcomp'. } rewrite σbetterok. clear σ σbetterok. unfold hcomp' in σbetter. set (σbetter' := ((FA v ◃ # FA g) ▹ G ) • ((# FA f ▹ FA w') ▹ G)). assert (σbetter'ok : σbetter = σbetter'). { apply pathsinv0, rwhisker_vcomp. } rewrite σbetter'ok. clear σbetter σbetter'ok. etrans. 2: { apply maponpaths. unfold σbetter'. repeat rewrite vassocr. apply maponpaths_2. apply pathsinv0. exact Hyp'variant. } clear Hyp'variant σbetter' δ. etrans. 2: { repeat rewrite vassocr. apply idpath. } match goal with | [ |- _ = (((_ • ?Hν'variant) • ?Hδ'π') • _) • _] => set (ν'variant := Hν'variant); set (δ'π' := Hδ'π') end. assert (ν'variantok: ν'variant • lassociator (FA v) G (FA' w') = lassociator (FA v) G (FA' w) • (H' v ◃ # FA' g)). { unfold ν'variant. rewrite Hmorok. apply lwhisker_lwhisker. } etrans. 2: { repeat rewrite <- vassocr. apply idpath. } apply pathsinv0. use lhs_left_invert_cell. { apply is_invertible_2cell_rassociator. } etrans. 2: { repeat rewrite vassocr. do 4 apply maponpaths_2. exact ν'variantok. } repeat rewrite <- vassocr. apply maponpaths. clear ν'variant ν'variantok. etrans. { apply maponpaths. apply rwhisker_rwhisker. } repeat rewrite vassocr. apply maponpaths_2. rewrite H'morok. etrans. { apply pathsinv0. apply hcomp_hcomp'. } clear δ'π'. unfold hcomp. apply maponpaths_2. clear δ'. cbn. rewrite rwhisker_rwhisker. rewrite <- vassocr. etrans. { apply pathsinv0, id2_right. } apply maponpaths. apply pathsinv0. apply (vcomp_rinv (is_invertible_2cell_lassociator _ _ _)). 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.