instCategoryHom

Mathlib.CategoryTheory.Bicategory.CatEnriched

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatEnrichedOrdinary.instCategoryHom

Lean4

/-- A `Cat`-enriched ordinary category comes with hom-categories `X ⟶[Cat] Y` whose underlying type
of objects is equivalent to the type `X ⟶ Y` defined by the category structure on `C`. The following
definition transfers the category structure to the latter type of objects. -/
instance {X Y : CatEnrichedOrdinary C} : Category (X ⟶ Y) where

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

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

Разделы

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

Аффилиация

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