# Documentation

This allows us to use these monads in category theory.

@[simp]
theorem CategoryTheory.ofTypeMonad_map (m : Type u → Type u) [] [] :
∀ {X Y : Type u} (f : X Y) (a : m X), .map f a = f <\$> a
@[simp]
theorem CategoryTheory.ofTypeMonad_η_app (m : Type u → Type u) [] [] {α : Type u} :
∀ (a : α), .app α a = pure a
@[simp]
theorem CategoryTheory.ofTypeMonad_μ_app (m : Type u → Type u) [] [] {α : Type u} (a : m (m α)) :
.app α a =
@[simp]
theorem CategoryTheory.ofTypeMonad_obj (m : Type u → Type u) [] [] :
∀ (a : Type u), .obj a = m a
def CategoryTheory.ofTypeMonad (m : Type u → Type u) [] [] :

A lawful Control.Monad gives a category theory Monad on the category of types.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.eq_inverse_map (m : Type u → Type u) [] [] :
∀ {X Y : } (f : X Y) (a : X), .inverse.map f a = f a
@[simp]
theorem CategoryTheory.eq_unitIso (m : Type u → Type u) [] [] :
.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : ) => )
@[simp]
theorem CategoryTheory.eq_inverse_obj (m : Type u → Type u) [] [] :
.inverse.obj X = X
@[simp]
theorem CategoryTheory.eq_counitIso (m : Type u → Type u) [] [] :
.counitIso =
@[simp]
theorem CategoryTheory.eq_functor_obj (m : Type u → Type u) [] [] (X : ) :
.functor.obj X = X
@[simp]
theorem CategoryTheory.eq_functor_map (m : Type u → Type u) [] [] :
∀ {X Y : } (f : X Y) (a : X), .functor.map f a = f a
def CategoryTheory.eq (m : Type u → Type u) [] [] :

The Kleisli category of a Control.Monad is equivalent to the Kleisli category of its category-theoretic version, provided the monad is lawful.

Equations
• One or more equations did not get rendered due to their size.
Instances For