∀ {ι : Type u_2} {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) (h : Homotopy f g),
  (HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g