∀ {C : Type u} {A : Type u₁} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasFiniteLimits A]
  [inst_3 : CategoryTheory.HasSheafify J A]
  [inst_4 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A]
  [CategoryTheory.AB5OfSize.{v₂, u₂, v₁, u₁} A],
  CategoryTheory.AB5OfSize.{v₂, u₂, max u v₁, max (max (max u₁ u) v₁) v} (CategoryTheory.Sheaf J A)