instCategory

Mathlib.CategoryTheory.Bicategory.CatEnriched

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatEnriched.instCategory

Lean4

/-- The action on objects of the `EnrichedCategory Cat` coherences proves the category axioms. -/
instance : Category (CatEnriched C)
    where
  id_comp {X Y} f := congrArg (·.obj f) (e_id_comp (V := Cat) X Y)
  comp_id {X Y} f := congrArg (·.obj f) (e_comp_id (V := Cat) X Y)
  assoc {X Y Z W} f g h := congrArg (·.obj (f, g, h)) (e_assoc (V := Cat) X Y Z W)

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

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

Разделы

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

Аффилиация

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