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.

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

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_functor_obj (m : Type u → Type u) [Monad m] [LawfulMonad m] (X : CategoryTheory.KleisliCat m) :
    (CategoryTheory.eq m).functor.obj X = X
    @[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
    @[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

    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