∀ {A : Type u'} [inst : CategoryTheory.Category.{v', u'} A] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalLocallyPresentable A κ] [CategoryTheory.Limits.HasPullbacks A] (C : Type w)
  [inst_4 : CategoryTheory.SmallCategory C],
  CategoryTheory.IsCardinalLocallyPresentable (CategoryTheory.Functor Cᵒᵖ A) κ