{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                {φ : S ⟶ F.op.comp R} →
                  {d : M.Derivation φ} →
                    (desc :
                        {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                          M'.Derivation φ → (M ⟶ M')) →
                      autoParam
                          (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
                            (d' : M'.Derivation φ), d.postcomp (desc d') = d')
                          PresheafOfModules.Derivation.Universal.fac._autoParam →
                        autoParam
                            (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
                              (φ_1 φ' : M ⟶ M'), d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ')
                            PresheafOfModules.Derivation.Universal.postcomp_injective._autoParam →
                          d.Universal