prodCategoryInstance2

Mathlib.CategoryTheory.Yoneda

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

English

There is a category structure on the product Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁).

Русский

Существует структура категории на произведении Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁).

LaTeX

$$$ \\text{Category}(C^{op} \\times (C^{op} \\to \\mathbf{Type})) $$$

Lean4

instance prodCategoryInstance2 : Category (Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) :=
  CategoryTheory.prod.{v₁, max u₁ v₁} Cᵒᵖ (Cᵒᵖ ⥤ Type v₁)

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

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

Разделы

Аффилиация

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