{S : Type u_1} →
  {inst : AddMonoidWithOne S} →
    {C : Type u} →
      {inst_1 : CategoryTheory.Category.{v, u} C} →
        {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} →
          {inst_3 : CategoryTheory.HasShift C S} →
            {X Y : CategoryTheory.DifferentialObject S C} →
              {P : Sort u_2} →
                {f : X.obj ⟶ Y.obj} →
                  {comm :
                      autoParam
                        (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) =
                          CategoryTheory.CategoryStruct.comp f Y.d)
                        CategoryTheory.DifferentialObject.Hom.comm._autoParam} →
                    {f' : X.obj ⟶ Y.obj} →
                      {comm' :
                          autoParam
                            (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f') =
                              CategoryTheory.CategoryStruct.comp f' Y.d)
                            CategoryTheory.DifferentialObject.Hom.comm._autoParam} →
                        { f := f, comm := comm } = { f := f', comm := comm' } → (f ≍ f' → P) → P