Lemma forgetKleisli_faithful (C : category) : faithful (forgetfunctor_Kleisli C). Proof. intros T T'. simpl. apply isinclbetweensets. - apply isaset_total2. + apply impred_isaset. intros. apply C. + intros. apply isasetaprop. apply isaprop_Kleisli_Mor_laws. - apply isaset_nat_trans. apply C. - intros α α' p. apply Kleisli_Mor_eq. apply funextsec. intro c. change (pr1 (nat_trans_kleisli_mor α) c = pr1 (nat_trans_kleisli_mor α') c). now rewrite p. 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.