{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (hom : S₁ ⟶ S₂) →
          (inv : S₂ ⟶ S₁) →
            CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp hom inv)
                (CategoryTheory.CategoryStruct.id S₁) →
              CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp inv hom)
                  (CategoryTheory.CategoryStruct.id S₂) →
                S₁.HomotopyEquiv S₂