instReflectsLimitsOfSizeForgetType

Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

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

English

The forgetful functor forget from Type to its base concrete category is an equivalence.

Русский

Забывающий функтор из Type в базовую конкретную категорию является эквивалентностью.

LaTeX

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

Lean4

instance : ReflectsLimitsOfSize (@forget (Type u) _ ConcreteCategory.toHasForget) :=
  id_reflectsLimits

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

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

Разделы

Аффилиация

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