proposition: Proposition monoidal_adjunction_from_strong_counit : is_mon_nat_trans (comp_fmonoidal_lax right_adjoint_monoidal_from_strong HL) (identity_fmonoidal M₂) ε.
proof: 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.
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