∀ {ι : Type u_3} (V : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) {X Y : HomologicalComplex V c}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex.forget V c).comp (CategoryTheory.GradedObject.eval i)).map f)
      ((fun x =>
            CategoryTheory.Iso.refl (((HomologicalComplex.forget V c).comp (CategoryTheory.GradedObject.eval i)).obj x))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.Iso.refl (((HomologicalComplex.forget V c).comp (CategoryTheory.GradedObject.eval i)).obj x))
          X).hom
      ((HomologicalComplex.eval V c i).map f)