Lean4
/-- The `Kleisli` category of a `Control.Monad` is equivalent to the `Kleisli` category of its
category-theoretic version, provided the monad is lawful.
-/
@[simps]
def eq : KleisliCat m ≌ Kleisli (ofTypeMonad m)
where
functor :=
{ obj := fun X => X
map := fun f => f
map_id := fun _ => rfl
map_comp := fun f g => by
unfold_projs
funext t
simp only [ofTypeMonad_obj, Function.comp_apply, ofTypeMonad_map, ofTypeMonad_μ_app, joinM, bind_map_left,
id_eq]
rfl }
inverse :=
{ obj := fun X => X
map := fun f => f
map_id := fun _ => rfl
map_comp := fun f g =>
by
unfold_projs
-- Porting note: Need these instances for some lemmas below.
--Should they be added as actual instances elsewhere?
letI : _root_.Monad (ofTypeMonad m).obj := show _root_.Monad m from inferInstance
letI : LawfulMonad (ofTypeMonad m).obj := show LawfulMonad m from inferInstance
funext t
simp only [ofTypeMonad_obj, Function.comp_apply, ofTypeMonad_map, ofTypeMonad_μ_app, joinM, bind_map_left,
id_eq]
rfl }
unitIso := by
refine NatIso.ofComponents (fun X => Iso.refl X) fun f => ?_
change f >=> pure = pure >=> f
simp [functor_norm]
counitIso := NatIso.ofComponents fun X => Iso.refl X
