proposition: Lemma montrafotargetbicat_tensor_comp_aux (v w v' w': Mon_V) (f: Mon_V⟦v,v'⟧) (g: Mon_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 η π -->[# tensor (f,, g: pr1 Mon_V ⊠ pr1 Mon_V ⟦ v,, w, v',, w' ⟧)] param_distr_bicat_pentagon_eq_body_variant_RHS v' w' η' π'.
proof: Proof. unfold mor_disp in Hyp, Hyp' |- *. 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', β'. change ((αinv • (lassociator G ((pr11 FA') v) (FA' w) • ((γ • (rassociator (FA v) G ((pr11 FA') w) • δ)) • (lassociator (FA v) (FA w) G • β)))) • ε1 = ε2 • (αinv' • (lassociator G ((pr11 FA') v') (FA' w') • ((γ' • (rassociator (FA v') G ((pr11 FA') w') • δ')) • (lassociator (FA v') (FA w') G • β'))))). 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 (lax_monoidal_functor_μ FA' (v,, w))). cbn in α. match goal with | [ |- ?Hαcand • _ = _ ] => set (αcand := Hαcand) end. change αcand with α. clear αcand. set (fg := (f #, g)). assert (μFA'natinst := nat_trans_ax (lax_monoidal_functor_μ FA') _ _ fg). simpl in μFA'natinst. assert (μFAnatinst := nat_trans_ax (lax_monoidal_functor_μ FA) _ _ fg). simpl in μFAnatinst. set (ε2better := lwhisker G (# (functor_composite tensor FA') fg)). transparent assert (ε2betterok : (ε2 = ε2better)). { cbn. apply hcomp_identity_left. } rewrite ε2betterok. 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. exact μFA'natinst. } clear ε2 μFA'natinst ε2better ε2betterok. 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. set (μFA'pointwise := nat_z_iso_pointwise_z_iso (strong_monoidal_functor_μ FA') (v',, w')). apply (z_iso_inv_after_z_iso μFA'pointwise). } clear αinv αinv' αinviso α. set (ε1better := rwhisker G (# (functor_composite tensor FA) fg)). transparent assert (ε1betterok : (ε1 = ε1better)). { cbn. apply hcomp_identity_right. } rewrite ε1betterok. 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. exact μFAnatinst. } clear β μFAnatinst ε1 ε1better ε1betterok. 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 σ'. rewrite hcomp_hcomp'. unfold hcomp'. clear σ'. 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 ((pr11 FA') v') (FA' w') • γ' = lassociator G ((pr11 FA') v) (FA' w') • (rwhisker (FA' w') η • rwhisker (FA' w') (# H' f))). { apply (maponpaths (vcomp2 (lassociator G ((pr11 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 ((pr11 FA') v') (FA' w')) • γ') • rassociator (FA v') G ((pr11 FA') w') • δ' • lassociator (FA v') (FA w') G). { repeat rewrite <- vassocr. apply idpath. } rewrite Hypvariant. clear σ'2 γ' Hypvariant. assert (σ'1ok : σ'1 • lassociator G ((pr11 FA') v) (FA' w') = lassociator G ((pr11 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) ((pr11 FA) w) G • ((FA v ◃ # (pr11 FA) g) ▹ G) = ((FA v ◃ # H g) • (FA v ◃ π')) • lassociator (FA v) ((pr11 FA) w') G). { apply (maponpaths (fun x => x • lassociator (FA v) ((pr11 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 ((pr11 FA') w') = lassociator ((pr11 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.
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.PrecategoryBinProduct UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalTensored UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal UniMath.Bicategories.MonoidalCategories.Actions UniMath.Bicategories.MonoidalCategories.ActionBasedStrength UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfCats