∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C],
  CochainComplex.singleFunctors C =
    { functor := fun n => HomologicalComplex.single C (ComplexShape.up ℤ) n,
      shiftIso := fun n a a' ha' =>
        CategoryTheory.NatIso.ofComponents
          (fun X => HomologicalComplex.Hom.isoOfComponents (fun i => CategoryTheory.eqToIso ⋯) ⋯) ⋯,
      shiftIso_zero := ⋯, shiftIso_add := ⋯ }