enrichedCategoryTypeEquivCategory

English

Equivalence between enriched categories over Type v and ordinary categories.

Русский

Эквиваленция между обогащенными категориями над Type v и обычными категориями.

LaTeX

$$$EnrichedCategory(Type(v), C) \simeq Category(C)$$$

Lean4

/-- We verify that an enriched category in `Type u` is just the same thing as an honest category.
-/
def enrichedCategoryTypeEquivCategory (C : Type u₁) : EnrichedCategory (Type v) C ≃ Category.{v} C
    where
  toFun _ := categoryOfEnrichedCategoryType C
  invFun _ := enrichedCategoryTypeOfCategory C

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