∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_3}
  {c : ComplexShape ι} {K L : HomologicalComplex C c} (h : HomotopyEquiv K L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap h.hom i) (HomologicalComplex.homologyMap h.inv i) =
    CategoryTheory.CategoryStruct.id (K.homology i)