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