Documentation

Mathlib.CategoryTheory.Monad.Types

Convert from Monad (i.e. Lean's Type-based monads) to CategoryTheory.Monad #

This allows us to use these monads in category theory.

source
@[simp]
theorem CategoryTheory.ofTypeMonad_map (m : Type u → Type u) [Monad m] [LawfulMonad m] :
∀ {X Y : Type u} (f : X ⟶ Y) (a : m X), Type u.map CategoryTheory.CategoryStruct.toQuiver (Type u) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.ofTypeMonad m).toFunctor.toPrefunctor X Y f a = f <$> a
source
@[simp]
theorem CategoryTheory.ofTypeMonad_η_app (m : Type u → Type u) [Monad m] [LawfulMonad m] {α : Type u} :
∀ (a : α), Type u.app CategoryTheory.types (Type u) CategoryTheory.types (CategoryTheory.Functor.id (Type u)) (CategoryTheory.ofTypeFunctor m) (CategoryTheory.Monad.η (CategoryTheory.ofTypeMonad m)) α a = pure a
source
@[simp]
theorem CategoryTheory.ofTypeMonad_μ_app (m : Type u → Type u) [Monad m] [LawfulMonad m] {α : Type u} (a : m (m α)) :
Type u.app CategoryTheory.types (Type u) CategoryTheory.types (CategoryTheory.Functor.comp (CategoryTheory.ofTypeFunctor m) (CategoryTheory.ofTypeFunctor m)) (CategoryTheory.ofTypeFunctor m) (CategoryTheory.Monad.μ (CategoryTheory.ofTypeMonad m)) α a = joinM a
source
@[simp]
theorem CategoryTheory.ofTypeMonad_obj (m : Type u → Type u) [Monad m] [LawfulMonad m] :
∀ (a : Type u), (CategoryTheory.ofTypeMonad m).toFunctor.obj a = m a
source
def CategoryTheory.ofTypeMonad (m : Type u → Type u) [Monad m] [LawfulMonad m] :
CategoryTheory.Monad (Type u)

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

Instances For
    source
    @[simp]
    theorem CategoryTheory.eq_inverse_map (m : Type u → Type u) [Monad m] [LawfulMonad m] :
    ∀ {X Y : CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)} (f : X ⟶ Y) (a : X), (CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)).map CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.KleisliCat m) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.eq m).inverse.toPrefunctor X Y f a = f a
    source
    @[simp]
    theorem CategoryTheory.eq_unitIso (m : Type u → Type u) [Monad m] [LawfulMonad m] :
    (CategoryTheory.eq m).unitIso = CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Iso.refl X
    source
    @[simp]
    theorem CategoryTheory.eq_inverse_obj (m : Type u → Type u) [Monad m] [LawfulMonad m] (X : CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)) :
    (CategoryTheory.eq m).inverse.obj X = X
    source
    @[simp]
    theorem CategoryTheory.eq_counitIso (m : Type u → Type u) [Monad m] [LawfulMonad m] :
    (CategoryTheory.eq m).counitIso = CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Iso.refl X
    source
    @[simp]
    theorem CategoryTheory.eq_functor_obj (m : Type u → Type u) [Monad m] [LawfulMonad m] (X : CategoryTheory.KleisliCat m) :
    (CategoryTheory.eq m).functor.obj X = X
    source
    @[simp]
    theorem CategoryTheory.eq_functor_map (m : Type u → Type u) [Monad m] [LawfulMonad m] :
    ∀ {X Y : CategoryTheory.KleisliCat m} (f : X ⟶ Y) (a : X), (CategoryTheory.KleisliCat m).map CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.eq m).functor.toPrefunctor X Y f a = f a
    source
    def CategoryTheory.eq (m : Type u → Type u) [Monad m] [LawfulMonad m] :
    CategoryTheory.KleisliCat m ≌ CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)

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

    Instances For