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 κ) : ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤

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)