Lemma precategory_Kleisli_axioms (C : category) : is_precategory (precategory_Kleisli_Data C). Proof. repeat split; simpl; intros. - apply (invmap (Kleisli_Mor_equiv _ _ )). apply funextsec. intros x. apply id_left. - apply (invmap (Kleisli_Mor_equiv _ _ )). apply funextsec. intros x. apply id_right. - apply (invmap (Kleisli_Mor_equiv _ _ )). apply funextsec. intros x. apply assoc. - apply (invmap (Kleisli_Mor_equiv _ _ )). apply funextsec. intros x. apply assoc'. 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.