∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q n : ℤ} (h : p + n = q),
  CochainComplex.HomComplex.Cochain.toSingleEquiv h =
    {
      toFun := fun α =>
        CategoryTheory.CategoryStruct.comp (α.v p q h) (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom,
      invFun := fun f => CochainComplex.HomComplex.Cochain.toSingleMk f h, left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }