Proposition monoidal_adjunction_from_strong_counit : is_mon_nat_trans (comp_fmonoidal_lax right_adjoint_monoidal_from_strong HL) (identity_fmonoidal M₂) ε. Proof. split. - intros x y ; cbn -[L R]. rewrite id_right. rewrite !(functor_comp R). rewrite !(functor_comp L). rewrite !assoc'. etrans. { do 3 apply maponpaths. apply (nat_trans_ax ε). } cbn -[L R]. rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. rewrite !assoc'. etrans. { do 2 apply maponpaths. apply (nat_trans_ax ε). } cbn -[L R]. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (triangle_1_statement_from_adjunction A). } rewrite id_left. apply (z_iso_inv_after_z_iso (_ ,, _)). - unfold is_mon_nat_trans_unitlaw ; cbn -[L R]. rewrite functor_comp. rewrite !assoc'. etrans. { do 2 apply maponpaths. apply (nat_trans_ax ε). } cbn -[L R]. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (triangle_1_statement_from_adjunction A). } rewrite id_left. exact (z_iso_inv_after_z_iso (_ ,, fmonoidal_preservesunitstrongly HL)). 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.