∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (φ : M₁.presheaf ⟶ M₂.presheaf) (X : Cᵒᵖ) (x y : ↑(M₁.1 X)),
  (CategoryTheory.ConcreteCategory.hom (φ.app X)) (x + y) =
    (CategoryTheory.ConcreteCategory.hom (φ.app X)) x + (CategoryTheory.ConcreteCategory.hom (φ.app X)) y