Library UniMath.CategoryTheory.Monads.KleisliCategory
**********************************************************
Contents:
Written by: Brandon Doherty (July 2018)
- Definition of the Kleisli category of a monad.
- The canonical adjunction between a category C and the Kleisli category of a monad on C.
- Show that this definition is equivalent to the Kleisli category of a relative monad with respect to the identity functor.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Monads.Monads.
Local Open Scope cat.
Section Monad_Lemmas.
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.
End Monad_Lemmas.
Section Kleisli_Categories.
Definition Kleisli_precat_ob_mor_monad {C : precategory_data} (T : Monad_data C) :
precategory_ob_mor.
Proof.
use tpair.
- exact (ob C).
- intros X Y.
exact (X --> T Y).
Defined.
Definition Kleisli_precat_data_monad {C : precategory_data} (T : Monad_data C) :
precategory_data.
Proof.
use make_precategory_data.
- exact (Kleisli_precat_ob_mor_monad T).
- intro c.
exact (η T c).
- intros a b c f g.
exact (f · (bind g)).
Defined.
Lemma Kleisli_precat_monad_is_precat {C : precategory} (T : Monad C) :
is_precategory (Kleisli_precat_data_monad T).
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.
Definition Kleisli_precat_monad {C : precategory} (T : Monad C) : precategory := (Kleisli_precat_data_monad T,,Kleisli_precat_monad_is_precat T).
Lemma Kleisli_precat_monad_has_homsets {C : precategory} (T : Monad C)
(hs : has_homsets C) : has_homsets (Kleisli_precat_data_monad T).
Proof.
intros a b.
apply hs.
Defined.
Definition Kleisli_cat_monad {C : category} (T : Monad C): category
:= (Kleisli_precat_monad T,, Kleisli_precat_monad_has_homsets T
(homset_property C)).
Definition Left_Kleisli_functor_data {C : precategory} (T: Monad C) :
functor_data C (Kleisli_precat_monad T).
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) :
functor C (Kleisli_precat_monad T)
:= (Left_Kleisli_functor_data T,,Left_Kleisli_is_functor T).
Definition Right_Kleisli_functor_data {C : precategory} (T : Monad C) :
functor_data (Kleisli_precat_monad T) 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) :
functor (Kleisli_precat_monad T) 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.
Definition Kleisli_functors_are_adjoints {C : precategory} (T : Monad C) : are_adjoints (Left_Kleisli_functor T) (Right_Kleisli_functor T) := adj_from_nathomweq (Kleisli_homset_iso T).
Definition Left_Kleisli_is_left_adjoint {C : precategory} (T : Monad C)
: is_left_adjoint (Left_Kleisli_functor T)
:= are_adjoints_to_is_left_adjoint (Left_Kleisli_functor T)
(Right_Kleisli_functor T) (Kleisli_functors_are_adjoints T).
Definition Right_Kleisli_is_right_adjoint {C : precategory} (T : Monad C)
: is_right_adjoint (Right_Kleisli_functor T)
:= are_adjoints_to_is_right_adjoint (Left_Kleisli_functor T)
(Right_Kleisli_functor T) (Kleisli_functors_are_adjoints T).
Theorem Kleisli_adjunction_monad_eq {C : precategory} (hs : has_homsets C) (T : Monad C) : Monad_from_adjunction (Kleisli_functors_are_adjoints T) = T.
Proof.
use Monad_eq_raw_data.
- 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.