Proposition is_strong_left_adjoint_on_tensor_laws : is_inverse_in_precat (fmonoidal_preservestensordata HL x y) is_strong_left_adjoint_on_tensor. Proof. assert (η (x ⊗_{M₁} y) = (η x ⊗^{M₁} η y) · fmonoidal_preservestensordata HR (L x) (L y) · #R (fmonoidal_preservestensordata HL x y)) as pη. { refine (!(id_left _) @ pr1 Hη x y @ _). rewrite !assoc'. apply idpath. } assert (fmonoidal_preservestensordata HL (R(L x)) (R(L y)) · #L (fmonoidal_preservestensordata HR (L x) (L y)) · ε (L x ⊗_{M₂} L y) = ε (L x) ⊗^{M₂} ε (L y)) as pε. { refine (pr1 Hε (L x) (L y) @ _). apply id_right. } split ; unfold is_strong_left_adjoint_on_tensor. - rewrite functor_comp. rewrite !assoc. etrans. { do 2 apply maponpaths_2. unfold functoronmorphisms1. cbn -[L R]. rewrite functor_comp. rewrite !assoc. etrans. { apply maponpaths_2. refine (!_). apply fmonoidal_preservestensornatright. } rewrite !assoc'. apply maponpaths. refine (!_). apply fmonoidal_preservestensornatleft. } rewrite !assoc'. etrans. { do 2 apply maponpaths. rewrite !assoc. exact pε. } rewrite !assoc. etrans. { refine (!_). apply bifunctor_distributes_over_comp ; apply M₂. } etrans. { apply maponpaths_2. apply (triangle_1_statement_from_adjunction A). } etrans. { apply maponpaths. apply (triangle_1_statement_from_adjunction A). } apply bifunctor_distributes_over_id ; apply M₂. - rewrite !assoc'. etrans. { apply maponpaths. refine (!_). apply (nat_trans_ax ε). } cbn -[L R]. rewrite !assoc. rewrite <- functor_comp. etrans. { apply maponpaths_2. apply maponpaths. exact (!pη). } 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.