category

Mathlib.CategoryTheory.Category.KleisliCat

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

Lean4

instance category {m} [Monad.{u, v} m] [LawfulMonad m] : Category (KleisliCat m) := by
  refine { id_comp := ?_, comp_id := ?_, assoc := ?_ } <;> intros <;> ext <;>
    simp +unfoldPartialApp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]

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

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

Разделы

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

Аффилиация

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