∀ {ι : Type u_1} {V : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E),
  Homotopy
      (CategoryTheory.CategoryStruct.comp f.hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g.hom g.inv) f.inv))
      (CategoryTheory.CategoryStruct.id C) =
    Homotopy
      (CategoryTheory.CategoryStruct.comp f.hom
        (CategoryTheory.CategoryStruct.comp g.hom (CategoryTheory.CategoryStruct.comp g.inv f.inv)))
      (CategoryTheory.CategoryStruct.id C)