∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d₀ : X₀ ⟶ X₁)
  (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0),
  (CochainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').X 0 = X₀