prodCategoryInstance1 — Mathlib

English

There is a category structure on the product of the category of functors with the opposite of C.

Русский

Существует структура категории на произведении категорий функторов и противоположного C.

LaTeX

$$$ \\text{Category}((C^{op} ⥤ Type v₁) × C^{op}) $$$

Lean4

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

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