Definition rKleisli_functors_are_relative_adjoints {C: precategory_data} {D : precategory} (hs : has_homsets D) {J : functor C D} (R: RelMonad J) : are_relative_adjoints J (Left_rKleisli_functor R) (Right_rKleisli_functor R). Proof. use tpair. - intros a b. use tpair. + simpl. apply idfun. + simpl. apply idisweq. - simpl; split. + intros a b f c h. unfold compose at 1; simpl. rewrite <- assoc. apply cancel_precomposition. apply (r_eta_r_bind R). + intros a b f c k. reflexivity. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core.