ofTypeMonad

Mathlib.CategoryTheory.Monad.Types

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ofTypeMonad

Lean4

/-- A lawful `Control.Monad` gives a category theory `Monad` on the category of types.
-/
@[simps!]
def ofTypeMonad : Monad (Type u) where
  toFunctor := ofTypeFunctor m
  η := ⟨@pure m _, fun _ _ f => funext fun x => (LawfulApplicative.map_pure f x).symm⟩
  μ := ⟨@joinM m _, fun _ _ _ => funext fun _ => joinM_map_map _ _⟩
  assoc _ := funext fun _ => joinM_map_joinM _
  left_unit _ := funext fun _ => joinM_pure _
  right_unit _ := funext fun _ => joinM_map_pure _

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru