Proposition right_adjoint_monoidal_from_strong_laws : fmonoidal_laxlaws right_adjoint_monoidal_data_from_strong. Proof. repeat split. - intros x y₁ y₂ g ; cbn -[L R]. etrans. { rewrite !assoc. apply maponpaths_2. exact (nat_trans_ax η _ _ (R x ⊗^{M₁}_{l} # R g)). } rewrite !assoc'. cbn -[L R]. rewrite <- !(functor_comp R). do 2 apply maponpaths. refine (!_). etrans. { rewrite !assoc'. apply maponpaths. etrans. { apply maponpaths. refine (!_). exact (when_bifunctor_becomes_leftwhiskering M₂ x g). } etrans. { refine (!_). apply bifunctor_distributes_over_comp ; apply M₂. } etrans. { apply maponpaths. refine (!_). exact (nat_trans_ax ε _ _ _). } rewrite id_right. etrans. { apply maponpaths_2. exact (!(id_left (ε x))). } etrans. { apply bifunctor_distributes_over_comp ; apply M₂. } cbn -[L R]. apply maponpaths_2. exact (when_bifunctor_becomes_leftwhiskering M₂ _ _). } rewrite !assoc. apply maponpaths_2. use z_iso_inv_on_right ; cbn -[L R]. rewrite !assoc. use z_iso_inv_on_left ; cbn -[L R]. refine (!_). apply fmonoidal_preservestensornatleft. - intros x₁ x₂ y f ; cbn -[L R]. etrans. { rewrite !assoc. apply maponpaths_2. exact (nat_trans_ax η _ _ (# R f ⊗^{M₁}_{r} R y)). } rewrite !assoc'. cbn -[L R]. rewrite <- !(functor_comp R). do 2 apply maponpaths. refine (!_). etrans. { rewrite !assoc'. apply maponpaths. etrans. { apply maponpaths. refine (!_). exact (when_bifunctor_becomes_rightwhiskering M₂ y f). } etrans. { refine (!_). apply bifunctor_distributes_over_comp ; apply M₂. } etrans. { apply maponpaths_2. refine (!_). exact (nat_trans_ax ε _ _ _). } rewrite id_right. etrans. { apply maponpaths. exact (!(id_left (ε y))). } etrans. { apply bifunctor_distributes_over_comp ; apply M₂. } cbn -[L R]. apply maponpaths_2. exact (when_bifunctor_becomes_rightwhiskering M₂ _ _). } rewrite !assoc. apply maponpaths_2. use z_iso_inv_on_right ; cbn -[L R]. rewrite !assoc. use z_iso_inv_on_left ; cbn -[L R]. refine (!_). apply fmonoidal_preservestensornatright. - intros x y z ; cbn -[L R]. rewrite !assoc. etrans. { do 2 apply maponpaths_2. apply (nat_trans_ax η _ _ (_ ⊗^{ M₁}_{r} _)). } refine (!_). etrans. { apply maponpaths_2. apply (nat_trans_ax η _ _ (_ · (_ ⊗^{ M₁}_{l} _))). } rewrite !assoc'. apply maponpaths. cbn -[L R]. rewrite <- !functor_comp. apply maponpaths. rewrite !assoc'. rewrite !functor_comp. etrans. { do 2 apply maponpaths_2. apply (strong_fmonoidal_preserves_associativity HL). } rewrite !assoc'. etrans. { do 4 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. refine (!_). apply (fmonoidal_preservestensornatleft HL). } rewrite !assoc'. etrans. { do 5 apply maponpaths. rewrite !assoc. etrans. { apply maponpaths_2. apply (z_iso_inv_after_z_iso (_ ,, _)). } apply id_left. } etrans. { rewrite !functor_comp. do 4 apply maponpaths. etrans. { apply maponpaths. unfold functoronmorphisms1. rewrite whiskerscommutes ; [ | apply M₂ ]. apply idpath. } rewrite !assoc. apply maponpaths_2. etrans. { refine (!_). apply (bifunctor_leftcomp M₂). } apply maponpaths. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- !functor_comp. apply (nat_trans_ax ε). } cbn -[L R]. rewrite !assoc. apply maponpaths_2. etrans. { apply maponpaths_2. apply (triangle_1_statement_from_adjunction A). } apply id_left. } etrans. { do 3 apply maponpaths. rewrite !assoc. apply maponpaths_2. etrans. { refine (!_). apply (bifunctor_leftcomp M₂). } apply maponpaths. rewrite !assoc. etrans. { apply maponpaths_2. apply (z_iso_inv_after_z_iso (_ ,, _)). } apply id_left. } use z_iso_inv_on_right ; cbn -[L R]. refine (!_). etrans. { rewrite !assoc. do 3 apply maponpaths_2. refine (!_). apply (fmonoidal_preservestensornatright HL). } rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. etrans. { apply maponpaths_2. apply (z_iso_inv_after_z_iso (_ ,, _)). } apply id_left. } etrans. { rewrite !assoc. apply maponpaths_2. refine (assoc _ _ _ @ _). apply maponpaths_2. etrans. { refine (!_). apply (bifunctor_rightcomp M₂). } apply maponpaths. rewrite !(functor_comp L). rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- !functor_comp. apply (nat_trans_ax ε). } cbn -[L R]. rewrite !assoc. apply maponpaths_2. etrans. { apply maponpaths_2. apply (triangle_1_statement_from_adjunction A). } apply id_left. } etrans. { do 2 apply maponpaths_2. apply (bifunctor_rightcomp M₂). } rewrite !assoc'. apply maponpaths. unfold functoronmorphisms1. refine (!_). etrans. { rewrite !assoc. apply maponpaths_2. etrans. { apply maponpaths. apply (bifunctor_leftcomp M₂). } rewrite !assoc. apply maponpaths_2. apply monoidal_associatornatleftright. } rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. etrans. { apply maponpaths_2. apply monoidal_associatornatleft. } rewrite !assoc'. apply maponpaths. apply monoidal_associatornatright. } rewrite !assoc. apply maponpaths_2. refine (!_). etrans. { apply maponpaths_2. apply (bifunctor_rightcomp M₂). } rewrite whiskerscommutes ; [ | apply M₂ ]. rewrite !assoc'. rewrite whiskerscommutes ; [ | apply M₂ ]. rewrite !assoc. rewrite whiskerscommutes ; [ | apply M₂ ]. rewrite !assoc'. apply maponpaths. etrans. { refine (!_). apply (bifunctor_rightcomp M₂). } refine (!_). etrans. { refine (!_). apply (bifunctor_rightcomp M₂). } apply maponpaths. rewrite <- whiskerscommutes ; [ | apply M₂ ]. apply idpath. - intros x ; cbn -[L R]. assert (# L lu^{M₁}_{R x} = inv_from_z_iso (_ ,, fmonoidal_preservestensorstrongly HL _ _) · (inv_from_z_iso (_ ,, fmonoidal_preservesunitstrongly HL) ⊗^{ M₂}_{r} L (R x)) · lu^{M₂}_{L(R x)}) as q. { pose (fmonoidal_preservesleftunitality HL (R x)) as p. cbn -[L R] in p. rewrite <- p. rewrite !assoc. refine (!(id_left _) @ _). apply maponpaths_2. refine (!_). etrans. { apply maponpaths_2. rewrite !assoc'. apply maponpaths. refine (!(bifunctor_rightcomp M₂ _ _ _ _ _ _) @ _). etrans. { apply maponpaths. apply (z_iso_after_z_iso_inv (_ ,, _)). } apply bifunctor_rightid. } rewrite id_right. apply (z_iso_after_z_iso_inv (_ ,, _)). } refine (_ @ id_right _). rewrite <- (triangle_2_statement_from_adjunction A). rewrite !assoc. refine (!_). etrans. { apply maponpaths_2. exact (nat_trans_ax η _ _ (lu^{M₁}_{R x})). } refine (!_). rewrite !assoc'. etrans. { rewrite !assoc. do 2 apply maponpaths_2. exact (nat_trans_ax η _ _ ((η I_{ M₁} · # R _) ⊗^{ M₁}_{r} R x)). } rewrite !assoc'. apply maponpaths. cbn -[L R]. rewrite <- !functor_comp. apply maponpaths. rewrite q. rewrite !assoc'. etrans. { do 2 apply maponpaths. unfold functoronmorphisms1. rewrite !assoc'. apply maponpaths. apply monoidal_leftunitornat. } rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. refine (!_). use z_iso_inv_on_right ; cbn -[L R]. refine (!_). rewrite !assoc. etrans. { do 2 apply maponpaths_2. refine (!_). apply fmonoidal_preservestensornatright. } rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (z_iso_inv_after_z_iso (_ ,, _)). } rewrite id_left. etrans. { refine (!_). apply (bifunctor_rightcomp M₂). } apply maponpaths. rewrite functor_comp. rewrite !assoc'. etrans. { apply maponpaths. apply (nat_trans_ax ε). } rewrite !assoc. refine (_ @ id_left _). cbn -[L R]. apply maponpaths_2. apply (triangle_1_statement_from_adjunction A). - intros x ; cbn -[L R]. assert (# L ru^{M₁}_{R x} = inv_from_z_iso (_ ,, fmonoidal_preservestensorstrongly HL _ _) · (L (R x) ⊗^{M₂}_{l} inv_from_z_iso (_ ,, fmonoidal_preservesunitstrongly HL)) · ru^{M₂}_{L(R x)}) as q. { pose (fmonoidal_preservesrightunitality HL (R x)) as p. cbn -[L R] in p. rewrite <- p. rewrite !assoc. refine (!(id_left _) @ _). apply maponpaths_2. refine (!_). etrans. { apply maponpaths_2. rewrite !assoc'. apply maponpaths. refine (!(bifunctor_leftcomp M₂ _ _ _ _ _ _) @ _). etrans. { apply maponpaths. apply (z_iso_after_z_iso_inv (_ ,, _)). } apply bifunctor_leftid. } rewrite id_right. apply (z_iso_after_z_iso_inv (_ ,, _)). } refine (_ @ id_right _). rewrite <- (triangle_2_statement_from_adjunction A). rewrite !assoc. refine (!_). etrans. { apply maponpaths_2. exact (nat_trans_ax η _ _ (ru^{M₁}_{R x})). } refine (!_). rewrite !assoc'. etrans. { rewrite !assoc. do 2 apply maponpaths_2. exact (nat_trans_ax η _ _ (R x ⊗^{M₁}_{l} (η I_{ M₁} · # R _))). } rewrite !assoc'. apply maponpaths. cbn -[L R]. rewrite <- !functor_comp. apply maponpaths. pose (fmonoidal_preservesrightunitality HL (R x)) as p. rewrite q. rewrite !assoc'. etrans. { do 2 apply maponpaths. unfold functoronmorphisms1. rewrite (whiskerscommutes M₂) ; [ | apply M₂ ]. rewrite !assoc'. apply maponpaths. apply monoidal_rightunitornat. } rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. refine (!_). use z_iso_inv_on_right ; cbn -[L R]. refine (!_). rewrite !assoc. etrans. { do 2 apply maponpaths_2. refine (!_). apply fmonoidal_preservestensornatleft. } rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (z_iso_inv_after_z_iso (_ ,, _)). } rewrite id_left. etrans. { refine (!_). apply (bifunctor_leftcomp M₂). } apply maponpaths. rewrite functor_comp. rewrite !assoc'. etrans. { apply maponpaths. apply (nat_trans_ax ε). } rewrite !assoc. refine (_ @ id_left _). cbn -[L R]. apply maponpaths_2. apply (triangle_1_statement_from_adjunction A). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monads.Comonads. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monoidal.FunctorCategories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import BifunctorNotations. Import MonoidalNotations. Section MonoidalAdjunctionFromStrong. End MonoidalAdjunctionFromStrong. Section SymMonoidalAdjunctionFromStrong. End SymMonoidalAdjunctionFromStrong.