proposition: Proposition monad_left_strong_to_enrichment_eta : nat_trans_enrichment (η M) (functor_id_enrichment self_enrichment) (strength_to_enrichment tM).
proof: Proof. use nat_trans_enrichment_via_comp. intros x y ; cbn. use internal_funext. intros w h. rewrite self_enrichment_precomp, self_enrichment_postcomp. etrans. { rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. apply idpath. } refine (!_). etrans. { rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. apply idpath. } rewrite tensor_comp_id_l. rewrite !assoc'. apply maponpaths. rewrite !assoc. refine (!_). etrans. { apply maponpaths_2. apply (left_strong_monad_unit tM). } exact (!(nat_trans_ax (η M) _ _ (internal_eval x y))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.StrongMonad UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed