{ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} →
          (X : ι → V) →
            (d : (i j : ι) → X i ⟶ X j) →
              autoParam (∀ (i j : ι), ¬c.Rel i j → d i j = 0) HomologicalComplex.shape._autoParam →
                autoParam
                    (∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d i j) (d j k) = 0)
                    HomologicalComplex.d_comp_d'._autoParam →
                  HomologicalComplex V c