Accessible categories are essentially large #
If a category C satisfies HasCardinalFilteredGenerator C κ for κ : Cardinal.{w}
(e.g. it is locally κ-presentable or κ-accessible),
then C is equivalent to a w-large category, i.e. a category whose type
of objects is in Type (w + 1) and whose types of morphisms are in Type w.
theorem
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top
{C : Type u}
[Category.{v, u} C]
{κ : Cardinal.{w}}
[Fact κ.IsRegular]
[LocallySmall.{w, v, u} C]
{P : ObjectProperty C}
[ObjectProperty.EssentiallySmall.{w, v, u} P]
(hP : P.IsCardinalFilteredGenerator κ)
:
theorem
CategoryTheory.HasCardinalFilteredGenerator.exists_equivalence
(C : Type u)
[Category.{v, u} C]
(κ : Cardinal.{w})
[Fact κ.IsRegular]
[HasCardinalFilteredGenerator C κ]
:
∃ (J : Type (w + 1)) (x : Category.{w, w + 1} J), Nonempty (C ≌ J)