{C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      {J : CategoryTheory.GrothendieckTopology C} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (x : C) → R ⟶ ((CategoryTheory.Over.star x).sheafPushforwardContinuous RingCat J (J.over x)).obj (R.over x)