{V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ X₂ : V) →
        (d₀ : X₁ ⟶ X₀) →
          (d₁ : X₂ ⟶ X₁) →
            CategoryTheory.CategoryStruct.comp d₁ d₀ = 0 →
              ((S : CategoryTheory.ShortComplex V) →
                  (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) →
                ℕ → CategoryTheory.ShortComplex V