English
The forgetful functor forget MonCat preserves all limits of size, i.e., PreservesLimitsOfSize forget MonCat.
Русский
Забывающая функция forget MonCat сохраняет все пределы по размеру, то есть PreservesLimitsOfSize forget MonCat.
LaTeX
$$$\text{PreservesLimitsOfSize }(\text{forget MonCat})$$$
Lean4
/-- The forgetful functor from 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 (relevant_arg := 100) /-- The forgetful functor from additive 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. -/
]
noncomputable instance forget_preservesLimitsOfSize [UnivLE.{v, u}] : PreservesLimitsOfSize.{w, v} (forget MonCat.{u})
where preservesLimitsOfShape := { }
