English
The forgetful functor from CommMonCat to types preserves all limits; equivalently, limits can be computed in the category of types and then equipped with the appropriate monoid structure.
Русский
Забывающий функтор от CommMonCat к типам сохраняет все пределы; пределы можно вычислять в категории типов, затем на них порождают подходящую моноидную структуру.
LaTeX
$$$\operatorname{PreservesLimitsOfSize}(\mathrm{forget\, CommMonCat})$$$
Lean4
/-- The forgetful functor from commutative monoids to types preserves all limits.
This means the underlying type of a limit can be computed as a limit in the category of types. -/
@[to_additive /-- The forgetful functor from additive commutative monoids to types preserves all
limits.
This means the underlying type of a limit can be computed as a limit in the category of types. -/
]
instance forget_preservesLimitsOfSize [UnivLE.{v, u}] : PreservesLimitsOfSize.{v, v} (forget CommMonCat.{u}) where
preservesLimitsOfShape {_} _ := { }
