∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (φ φ_1 : M₁.presheaf ⟶ M₂.presheaf) (e_φ : φ = φ_1)
  (hφ :
    ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₁.obj X)),
      (CategoryTheory.ConcreteCategory.hom (φ.app X)) (r • m) = r • (CategoryTheory.ConcreteCategory.hom (φ.app X)) m),
  PresheafOfModules.homMk φ hφ = PresheafOfModules.homMk φ_1 ⋯