Proposition monoidal_adjunction_from_strong_unit : is_mon_nat_trans (identity_fmonoidal M₁) (comp_fmonoidal_lax HL right_adjoint_monoidal_from_strong) η. Proof. split. - intros x y ; cbn -[L R]. rewrite id_left. rewrite !assoc'. rewrite <- (functor_comp R). refine (!_). rewrite !assoc. etrans. { apply maponpaths_2. exact (nat_trans_ax η _ _ (adjunit A x ⊗^{M₁} adjunit A y)). } rewrite !assoc'. refine (_ @ id_right _). apply maponpaths. cbn -[L R]. rewrite <- functor_comp. rewrite <- functor_id. apply maponpaths. rewrite !assoc. refine (_ @ z_iso_after_z_iso_inv (_ ,, fmonoidal_preservestensorstrongly HL _ _)). apply maponpaths_2. refine (!_ @ id_right _). use z_iso_inv_on_right ; cbn -[L R]. refine (!_). rewrite !assoc. etrans. { do 2 apply maponpaths_2. unfold functoronmorphisms1. rewrite functor_comp. rewrite !assoc. etrans. { apply maponpaths_2. refine (!_). apply (fmonoidal_preservestensornatright HL). } rewrite !assoc'. apply maponpaths. refine (!_). apply (fmonoidal_preservestensornatleft HL). } rewrite !assoc'. etrans. { do 2 apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (z_iso_inv_after_z_iso (_ ,, fmonoidal_preservestensorstrongly HL _ _)). } rewrite id_left. rewrite !assoc. etrans. { refine (!_). apply bifunctor_distributes_over_comp ; apply M₂. } refine (!_). etrans. { refine (!_). apply bifunctor_distributes_over_id ; apply M₂. } refine (!_). etrans. { apply maponpaths. apply (triangle_1_statement_from_adjunction A). } apply maponpaths_2. apply (triangle_1_statement_from_adjunction A). - unfold is_mon_nat_trans_unitlaw ; cbn -[L R]. rewrite id_left. rewrite !assoc'. refine (!(id_right _) @ _). apply maponpaths. rewrite <- functor_comp. rewrite <- functor_id. apply maponpaths. refine (!_). apply z_iso_after_z_iso_inv. 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.