∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (x : CochainComplex.HomComplex.Cocycle K L n),
  CochainComplex.HomComplex.CohomologyClass.mk (-x) = -CochainComplex.HomComplex.CohomologyClass.mk x