instMonadicRightAdjointAlgebraForget

Mathlib.CategoryTheory.Monad.Adjunction

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

Lean4

noncomputable instance (T : Monad C) : MonadicRightAdjoint T.forget
    where
  L := T.free
  adj := T.adj
  eqv := { }

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

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

Разделы

Аффилиация

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