********************************************************** Contents:
• Definition of the Kleisli category of a monad.
• The canonical adjunction between a category C and the Kleisli category of a monad on C.
TODO:
• Show that this definition is equivalent to the Kleisli category of a relative monad with respect to the identity functor.
Written by: Brandon Doherty (July 2018)

Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.

Local Open Scope cat.

Lemma bind_comp_η {C : precategory} {T : Monad C} {a b : C} (f : C a , b) :
bind (f · (η T) b) = # T f.
Proof.
unfold bind; rewrite functor_comp.
rewrite <- assoc.
rewrite <- id_right.
apply cancel_precomposition.
apply bind_η.
Qed.

Lemma bind_identity {C : precategory} {T : Monad C} (a : C) :
bind (identity (T a)) = (μ T) a.
Proof.
unfold bind.
rewrite functor_id.
apply id_left.
Qed.

Section Kleisli_Categories.

precategory_ob_mor.
Proof.
use tpair.
- exact (ob C).
- intros X Y.
exact (X --> T Y).
Defined.

precategory_data.
Proof.
use make_precategory_data.
- intro c.
exact (η T c).
- intros a b c f g.
exact (f · (bind g)).
Defined.

Proof.
apply is_precategory_one_assoc_to_two.
split.
- split.
+ intros a b f.
unfold identity; unfold compose; cbn.
apply η_bind.
+ intros a b f.
unfold identity; unfold compose; cbn.
rewrite <- id_right.
apply cancel_precomposition.
apply bind_η.
- intros a b c d f g h.
unfold compose; cbn.
rewrite <- bind_bind.
apply assoc.
Defined.

(hs : has_homsets C) : has_homsets (Kleisli_precat_data_monad T).
Proof.
intros a b.
apply hs.
Defined.

(homset_property C)).

Definition Left_Kleisli_functor_data {C : precategory} (T: Monad C) :
Proof.
use make_functor_data.
- apply idfun.
- intros a b f; unfold idfun.
exact (f · (η T) b).
Defined.

Lemma Left_Kleisli_is_functor {C : precategory} (T: Monad C) :
is_functor (Left_Kleisli_functor_data T).
Proof.
split.
- intro a.
unfold Left_Kleisli_functor_data; cbn.
apply id_left.
- intros a b c f g.
unfold Left_Kleisli_functor_data; cbn.
do 2 (rewrite <- assoc).
apply cancel_precomposition.
apply pathsinv0.
apply η_bind.
Defined.

Definition Left_Kleisli_functor {C : precategory} (T : Monad C) :
:= (Left_Kleisli_functor_data T,,Left_Kleisli_is_functor T).

Definition Right_Kleisli_functor_data {C : precategory} (T : Monad C) :
Proof.
use make_functor_data.
- exact T.
- intros a b.
apply bind.
Defined.

Lemma Right_Kleisli_is_functor {C : precategory} (T : Monad C) :
is_functor (Right_Kleisli_functor_data T).
Proof.
use tpair.
- intro a.
unfold Right_Kleisli_functor_data; unfold identity;
unfold functor_on_morphisms; cbn.
apply bind_η.
- intros a b c f g; cbn.
apply pathsinv0.
apply bind_bind.
Defined.

Definition Right_Kleisli_functor {C : precategory} (T : Monad C) :
:= (Right_Kleisli_functor_data T,,Right_Kleisli_is_functor T).

Definition Kleisli_functor_left_right_compose {C : precategory}
(hs : has_homsets C) (T : Monad C) :
(Left_Kleisli_functor T) (Right_Kleisli_functor T) = T.
Proof.
use functor_eq.
- exact hs.
- use functor_data_eq_from_nat_trans.
+ intro a; apply idpath.
+ intros a b f; cbn.
rewrite id_right.
rewrite id_left.
apply bind_comp_η.
Defined.

Definition Kleisli_homset_iso {C : precategory} (T : Monad C) : natural_hom_weq (Left_Kleisli_functor T) (Right_Kleisli_functor T).
Proof.
use tpair.
- intros a b; cbn.
apply idweq.
- cbn; unfold idfun; split.
+ intros.
rewrite <- assoc.
apply cancel_precomposition.
apply η_bind.
+ reflexivity.
Defined.

Proof.
- exact hs.
- apply total2_paths_equiv; use tpair.
+ cbn.
reflexivity.
+ cbn.
apply total2_paths_equiv; use tpair.
× cbn.
apply total2_paths_equiv; use tpair.
-- cbn.
do 2 (apply funextsec; intro).
apply funextfun; intro f.
cbn.
apply bind_comp_η.
-- cbn.
rewrite transportf_const.
unfold idfun.
apply funextsec; intro c.
apply bind_identity.
× cbn.
rewrite transportf_const.
reflexivity.
Defined.

End Kleisli_Categories.