∀ {ι : Type u_3} (V : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex V c.symm} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((HomologicalComplex.unopInverse V c).comp (HomologicalComplex.unopFunctor V c)).map f)
      ((fun X =>
            HomologicalComplex.Hom.isoOfComponents
              (fun x =>
                CategoryTheory.Iso.refl
                  ((((HomologicalComplex.unopInverse V c).comp (HomologicalComplex.unopFunctor V c)).obj X).X x))
              ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            HomologicalComplex.Hom.isoOfComponents
              (fun x =>
                CategoryTheory.Iso.refl
                  ((((HomologicalComplex.unopInverse V c).comp (HomologicalComplex.unopFunctor V c)).obj X).X x))
              ⋯)
          X).hom
      ((CategoryTheory.Functor.id (HomologicalComplex V c.symm)).map f)