instReflectsColimitsOfSizeForgetType

English

The forgetful functor forget from Type to the base concrete category is corepresentable.

Русский

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

LaTeX

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

Lean4

instance : ReflectsColimitsOfSize (@forget (Type u) _ ConcreteCategory.toHasForget) :=
  id_reflectsColimits

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