∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C]
  (J : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} J] [Small.{u₁, u₂} J]
  [CategoryTheory.LocallySmall.{v₁, v₂, u₂} J], CategoryTheory.Limits.HasLimitsOfShape J C