∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ)
  (hX : CategoryTheory.Limits.IsInitial X) {M N : PresheafOfModules R} (f : M ⟶ N) (Y : Cᵒᵖ)
  (x y : ↑((PresheafOfModules.forgetToPresheafModuleCatObj X hX M).obj Y)),
  (CategoryTheory.ConcreteCategory.hom (f.app Y)) (x + y) =
    (CategoryTheory.ConcreteCategory.hom (f.app Y)) x + (CategoryTheory.ConcreteCategory.hom (f.app Y)) y