∀ {ι : Type u_1} {V : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D),
  (HomotopyCategory.quotient V c).map (Quot.out ((HomotopyCategory.quotient V c).map f)) =
    (HomotopyCategory.quotient V c).map f