∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {f g : X ⟶ Y}, f = g ↔ f.val = g.val