hasColimitsOfShape

Mathlib.CategoryTheory.Limits.Types.Colimits

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

English

There is a canonical instance HasColimitsOfShape J (Type u) for any small J, i.e., the category Type u has all colimits of shape J.

Русский

Существует канонический инстанс HasColimitsOfShape J (Type u), т.е. категория Type u имеет все колимиты формы J.

LaTeX

$$$$ HasColimitsOfShape\ J\ (Type\ u). $$$$

Lean4

instance hasColimitsOfShape [Small.{u} J] : HasColimitsOfShape J (Type u) where

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

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

Разделы

Аффилиация

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