Proposition monad_left_strong_to_enrichment_mu : nat_trans_enrichment (μ M) (functor_comp_enrichment (strength_to_enrichment tM) (strength_to_enrichment tM)) (strength_to_enrichment tM). 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. rewrite tensor_comp_id_l. rewrite !assoc'. apply maponpaths. rewrite !assoc. apply maponpaths_2. apply left_strong_monad_mu. } refine (!_). etrans. { rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. apply maponpaths_2. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. apply idpath. } rewrite tensor_split. rewrite !assoc'. apply maponpaths. etrans. { rewrite <- (functor_id M). rewrite !assoc. rewrite left_strength_natural. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- functor_comp. rewrite internal_beta. apply idpath. } refine (!_). etrans. { do 2 apply maponpaths. exact (!(nat_trans_ax (μ M) _ _ (internal_eval x y))). } cbn. rewrite functor_comp. rewrite !assoc'. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.StrongMonad. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.