Categories of presheaves are locally presentable

If A is a locally κ-presentable category and C is a small category, we show that Cᵒᵖ ⥤ A is also locally κ-presentable, under the additional assumption that A has pullbacks (a condition which should be automatically satisfied (TODO)).

instance CategoryTheory.Presheaf.instIsCardinalPresentableFunctorOppositeFreeYonedaOfHasColimitsOfSize {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [Limits.HasCoproducts A] (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : C) (M : A) [IsCardinalPresentable M κ] : IsCardinalPresentable (freeYoneda X M) κ

instance CategoryTheory.Presheaf.instIsCardinalPresentableFunctorOppositeTypeObjUliftYonedaOfHasColimitsOfSize {C : Type u} [SmallCategory C] [Limits.HasColimitsOfSize.{w, w, max u u', max (u + 1) (u' + 1)} (Type (max u u'))] (κ : Cardinal.{w}) [Fact κ.IsRegular] (X : C) : IsCardinalPresentable (uliftYoneda.{u', u, u}.obj X) κ

theorem CategoryTheory.Presheaf.isStrongGenerator {A : Type u'} [Category.{v', u'} A] {P : ObjectProperty A} (hP : P.IsStrongGenerator) [Limits.HasCoproducts A] [Limits.HasPullbacks A] (C : Type w) [SmallCategory C] : (ObjectProperty.ofObj fun (T : C × Subtype P) => freeYoneda T.1 ↑T.2).IsStrongGenerator

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

instance CategoryTheory.Presheaf.instIsLocallyPresentableFunctorOppositeOfHasPullbacks {A : Type u'} [Category.{v', u'} A] [IsLocallyPresentable.{w, v', u'} A] [Limits.HasPullbacks A] (C : Type w) [SmallCategory C] : IsLocallyPresentable.{w, max v' w, max (max (max u' w) v') w} (Functor Cᵒᵖ A)