∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.IsCardinalLocallyPresentable C κ ↔
    ∃ P,
      ∃ (_ : CategoryTheory.ObjectProperty.Small.{w, v, u} P),
        P.IsStrongGenerator ∧ P ≤ CategoryTheory.isCardinalPresentable C κ