Lemma Kleisli_data_eq {F : C → C} (K K' : Kleisli_Data F) (η_eq : ∏ a : C, η K a = η K' a) (bind_eq : ∏ (a b : C) (f : a --> F b), bind K f = bind K' f) : K = K'. Proof. intros. apply dirprod_paths. - change (η K = η K'). apply funextsec. intro a. apply η_eq. - apply funextsec. intro a. apply funextsec. intro b. apply funextfun. intro f. apply bind_eq. 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.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.KTriples. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.