{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            CategoryTheory.ShortComplex.Homotopy φ₃ φ₄ → CategoryTheory.ShortComplex.Homotopy (φ₁ - φ₃) (φ₂ - φ₄)