∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (F G : CochainComplex C ℤ) (φ : F ⟶ G),
  (CochainComplex.HomComplex.Cocycle.equivHom F G) φ = CochainComplex.HomComplex.Cocycle.ofHom φ