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_obj (m : Type u → Type u) [Monad m] [LawfulMonad m] :
∀ (a : Type u), (CategoryTheory.ofTypeMonad m).obj a = m a
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), (CategoryTheory.ofTypeMonad m).map f a = f <$> a
source
@[simp]
theorem CategoryTheory.ofTypeMonad_η_app (m : Type u → Type u) [Monad m] [LawfulMonad m] {α : Type u} :
∀ (a : α), (CategoryTheory.ofTypeMonad m).η.app α a = pure a
source
@[simp]
theorem CategoryTheory.ofTypeMonad_μ_app (m : Type u → Type u) [Monad m] [LawfulMonad m] {α : Type u} (a : m (m α)) :
(CategoryTheory.ofTypeMonad m).μ.app α a = joinM 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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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_unitIso (m : Type u → Type u) [Monad m] [LawfulMonad m] :
    (CategoryTheory.eq m).unitIso = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.KleisliCat m) => CategoryTheory.Iso.refl 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.eq m).functor.map f a = f a
    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.eq m).inverse.map f a = f a
    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.Kleisli (CategoryTheory.ofTypeMonad m)) => 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
    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.

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