{P : Sort u_2} →
  {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} →
                {t : X.Hom Y} →
                  {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'} →
                                {t' : X'.Hom Y'} →
                                  S = S' →
                                    inst ≍ inst' →
                                      C = C' →
                                        inst_1 ≍ inst'_1 →
                                          inst_2 ≍ inst'_2 →
                                            inst_3 ≍ inst'_3 →
                                              X ≍ X' →
                                                Y ≍ Y' →
                                                  t ≍ t' → CategoryTheory.DifferentialObject.Hom.noConfusionType P t t'