∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ κ_1 : Cardinal.{w}) (e_κ : κ = κ_1)
  [inst_1 : Fact κ.IsRegular],
  CategoryTheory.IsCardinalAccessibleCategory C κ = CategoryTheory.IsCardinalAccessibleCategory C κ_1