∀ {D : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  (φ' : S' ⟶ R) {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation' φ')
  {X Y : Dᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f)
      ((ModuleCat.restrictScalars (RingCat.Hom.hom ((R.comp (CategoryTheory.forget₂ CommRingCat RingCat)).map f))).map
        (d'.app Y).desc) =
    CategoryTheory.CategoryStruct.comp (d'.app X).desc (M'.map f)