instEnrichedOrdinaryCategoryCat

Mathlib.CategoryTheory.Bicategory.CatEnriched

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

Lean4

/-- The category instance on `CatEnriched C` promotes it to a `Cat` enriched ordinary
category. -/
instance : EnrichedOrdinaryCategory Cat (CatEnriched C)
    where
  homEquiv := Cat.fromChosenTerminalEquiv.symm
  homEquiv_comp _ _ := (Equiv.symm_apply_eq Cat.fromChosenTerminalEquiv).mpr rfl
  homEquiv_id _ := (Equiv.symm_apply_eq Cat.fromChosenTerminalEquiv).mpr rfl

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

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

Разделы

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

Аффилиация

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