{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        CategoryTheory.Functor (SheafOfModules R) (CategoryTheory.Sheaf J AddCommGrpCat)