∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) [inst_2 : CategoryTheory.CategoryWithHomology C] {X Y : HomologicalComplex C c}
  (f : X ⟶ Y) (i : ι), (HomologicalComplex.gradedHomologyFunctor C c).map f i = HomologicalComplex.homologyMap f i