{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          [CategoryTheory.Limits.HasCoproducts A] →
            [CategoryTheory.HasWeakSheafify J A] → C → A → CategoryTheory.Sheaf J A