∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {ι : Type w'}
  {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  CategoryTheory.PresheafIsGeneratedBy F x →
    ∀ {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F') [CategoryTheory.Epi f],
      CategoryTheory.PresheafIsGeneratedBy F' fun i => f.app (X i) (x i)