proposition: Proposition is_strong_left_adjoint_on_tensor_laws : is_inverse_in_precat (fmonoidal_preservestensordata HL x y) is_strong_left_adjoint_on_tensor.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Monoidal.FunctorCategories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Structure.Symmetric