category

Mathlib.CategoryTheory.Monad.Kleisli

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Cokleisli.category

Lean4

/-- The co-Kleisli category on a comonad `U`. -/
instance category : Category (Cokleisli U)
    where
  Hom := fun X Y : C => (U : C ⥤ C).obj X ⟶ Y
  id X := U.ε.app X
  comp f g := U.δ.app _ ≫ (U : C ⥤ C).map f ≫ g

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

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

Разделы

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

Аффилиация

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