{ι : Type u_1} →
  {V : Type u} →
    {inst : CategoryTheory.Category.{v, u} V} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms V} →
        {c : ComplexShape ι} →
          {P : Sort u_2} →
            {X : ι → V} →
              {d : (i j : ι) → X i ⟶ X j} →
                {shape : autoParam (∀ (i j : ι), ¬c.Rel i j → d i j = 0) HomologicalComplex.shape._autoParam} →
                  {d_comp_d' :
                      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} →
                    {X' : ι → V} →
                      {d' : (i j : ι) → X' i ⟶ X' j} →
                        {shape' :
                            autoParam (∀ (i j : ι), ¬c.Rel i j → d' i j = 0) HomologicalComplex.shape._autoParam} →
                          {d_comp_d'' :
                              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} →
                            { X := X, d := d, shape := shape, d_comp_d' := d_comp_d' } =
                                { X := X', d := d', shape := shape', d_comp_d' := d_comp_d'' } →
                              (X ≍ X' → d ≍ d' → P) → P