{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          {motive : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ → Sort u} →
            ((h₀ : S₁.X₁ ⟶ S₂.X₁) →
                (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) →
                  (h₁ : S₁.X₂ ⟶ S₂.X₁) →
                    (h₂ : S₁.X₃ ⟶ S₂.X₂) →
                      (h₃ : S₁.X₃ ⟶ S₂.X₃) →
                        (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) →
                          (comm₁ : φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁ + h₀ + φ₂.τ₁) →
                            (comm₂ :
                                φ₁.τ₂ =
                                  CategoryTheory.CategoryStruct.comp S₁.g h₂ +
                                      CategoryTheory.CategoryStruct.comp h₁ S₂.f +
                                    φ₂.τ₂) →
                              (comm₃ : φ₁.τ₃ = h₃ + CategoryTheory.CategoryStruct.comp h₂ S₂.g + φ₂.τ₃) →
                                motive
                                  { h₀ := h₀, h₀_f := h₀_f, h₁ := h₁, h₂ := h₂, h₃ := h₃, g_h₃ := g_h₃, comm₁ := comm₁,
                                    comm₂ := comm₂, comm₃ := comm₃ }) →
              (t : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) → motive t