(C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (n i i' : ℤ) →
        n + i = i' →
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).comp (HomologicalComplex.eval C (ComplexShape.up ℤ) i) ≅
            HomologicalComplex.eval C (ComplexShape.up ℤ) i')