Theorems · Definition · category theory

CategoryTheory.kleisliCatEquivKleisli

(m : Type u → Type u) →
  [inst : Monad m] →
    [inst_1 : 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.

Defined in

Mathlib.CategoryTheory.Monad.Types

Cited by

6 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonadLawfulMonad