Documentation

Mathlib.CategoryTheory.Monad.EquivMon

The equivalence between Monad C and Mon_ (C ⥤ C). #

A monad "is just" a monoid in the category of endofunctors.

Definitions/Theorems #

  1. toMon associates a monoid object in C ⥤ C to any monad on C.
  2. monadToMon is the functorial version of toMon.
  3. ofMon associates a monad on C to any monoid object in C ⥤ C.
  4. monadMonEquiv is the equivalence between Monad C and Mon_ (C ⥤ C).

To every Monad C we associated a monoid object in C ⥤ C.

Instances For

    To every monoid object in C ⥤ C we associate a Monad C.

    Instances For
      @[simp]

      Oh, monads are just monoids in the category of endofunctors (equivalence of categories).

      Instances For