categoryOfEnrichedCategoryType

Mathlib.CategoryTheory.Enriched.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.categoryOfEnrichedCategoryType

Lean4

/-- Construct an honest category from a `Type v`-enriched category.
-/
def categoryOfEnrichedCategoryType (C : Type u₁) [𝒞 : EnrichedCategory (Type v) C] : Category.{v} C
    where
  Hom := 𝒞.Hom
  id X := eId (Type v) X PUnit.unit
  comp f g := eComp (Type v) _ _ _ ⟨f, g⟩
  id_comp f := congr_fun (e_id_comp (Type v) _ _) f
  comp_id f := congr_fun (e_comp_id (Type v) _ _) f
  assoc f g h := (congr_fun (e_assoc (Type v) _ _ _ _) ⟨f, g, h⟩ :)

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

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

Разделы

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

Аффилиация

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