∀ {D : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R}
  (d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)) {X : Dᵒᵖ} (a b : ↑(R.obj X)),
  (d X).d (a + b) = (d X).d a + (d X).d b