proposition: 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: 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.
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.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.KleisliCategory