instCategoryStruct

Mathlib.CategoryTheory.Bicategory.CatEnriched

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

Lean4

/-- Any enriched category has an underlying category structure defined by `ForgetEnrichment`.
This is equivalent but not definitionally equal the category structure constructed here, which is
more canonically associated to the data of an `EnrichedCategory Cat` structure. -/
instance : CategoryStruct (CatEnriched C) where
  Hom X Y := X ⟶[Cat] Y
  id X := (eId Cat X).obj ⟨⟨()⟩⟩
  comp {X Y Z} f g := (eComp Cat X Y Z).obj (f, g)

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

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

Разделы

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

Аффилиация

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