instAB5Type

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.instAB5Type

English

The category Type with its standard structure satisfies AB5.

Русский

Категория Type удовлетворяет AB5.

LaTeX

$$$\mathrm{AB5}(\mathrm{Type})$$$

Lean4

instance : AB5 (Type v) where ofShape _ _ _ := ⟨inferInstance⟩

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

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

Разделы

Аффилиация

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