hasColimitsOfSize — Mathlib

English

There is a global instance HasColimitsOfSize for Type u, i.e., Type u has all colimits of any shape when universes permit it (subject to Unv constraints).

Русский

Существует глобальный инстанс HasColimitsOfSize для Type u, т.е. Type u имеет все колимиты любой формы при соответствующих ограничениях вселенных.

LaTeX

$$$$ [UnivLE]\ HasColimitsOfSize\ (Type\ u). $$$$

Lean4

/-- The category of types has all colimits. -/
@[stacks 002U]
instance (priority := 1300) hasColimitsOfSize [UnivLE.{v, u}] : HasColimitsOfSize.{w, v} (Type u) where

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