Definition forgetfunctor_Kleisli (C : category) : functor (category_Kleisli C) (functor_category C C). Proof. use make_functor. - simpl. use make_functor_data. + simpl. exact (λ T : KleisliMonad C, kleisli_functor T). + simpl. intros T T' α. exact (nat_trans_kleisli_mor α). - split. + red. intros. simpl. apply nat_trans_eq. * apply C. * intros; apply idpath. + unfold functor_compax. simpl. intros. apply nat_trans_eq. * apply C. * intros. apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.RelativeMonads.