∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [inst_4 : F.Additive]
  (h : HomotopyEquiv C D), (F.mapHomotopyEquiv h).inv = (F.mapHomologicalComplex c).map h.inv