{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} →
          (t : S₁.HomotopyEquiv S₂) →
            ((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 }) →
              motive t