instPreservesLimitsOfSizeForgetType

English

The forgetful functor forget from Type to its base concrete category preserves limits of any size.

Русский

Забывающий функтор forget из Type в базовую конкретную категорию сохраняет пределы любого размера.

LaTeX

$$$\\mathrm{PreservesLimitsOfSize}(\\mathrm{forget}:\\mathrm{Type}_u\\to\\text{ConcreteCategory})$$$

Lean4

instance : PreservesLimitsOfSize (@forget (Type u) _ ConcreteCategory.toHasForget) :=
  id_preservesLimitsOfSize

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