∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Preadditive V}
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {hom : (i j : ι) → C.X i ⟶ D.X j}
  {zero : autoParam (∀ (i j : ι), ¬c.Rel j i → hom i j = 0) Homotopy.zero._autoParam}
  {comm : autoParam (∀ (i : ι), f.f i = (dNext i) hom + (prevD i) hom + g.f i) Homotopy.comm._autoParam}
  {hom_1 : (i j : ι) → C.X i ⟶ D.X j}
  {zero_1 : autoParam (∀ (i j : ι), ¬c.Rel j i → hom_1 i j = 0) Homotopy.zero._autoParam}
  {comm_1 : autoParam (∀ (i : ι), f.f i = (dNext i) hom_1 + (prevD i) hom_1 + g.f i) Homotopy.comm._autoParam},
  { hom := hom, zero := zero, comm := comm } = { hom := hom_1, zero := zero_1, comm := comm_1 } → hom = hom_1