Proposition functor_from_kleisli_cat_monad_nat_trans_enrichment : nat_trans_enrichment (functor_from_kleisli_cat_monad_nat_trans M F γ p q) (functor_comp_enrichment Left_Kleisli_functor_enrichment functor_from_kleisli_cat_enrichment) EF. Proof. use nat_trans_enrichment_via_comp. intros x y ; cbn. rewrite precomp_arr_id, postcomp_arr_id. rewrite !id_right. unfold functor_from_kleisli_cat_enrichment_data. rewrite !assoc. rewrite <- functor_enrichment_postcomp_arr. rewrite !assoc'. rewrite <- postcomp_arr_comp. refine (!(id_right _) @ !_). apply maponpaths. refine (_ @ postcomp_arr_id _ _ _). apply maponpaths. apply p. 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.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.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.KleisliCategory. Section FunctorFromKleisli. End FunctorFromKleisli.