∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p),
  CochainComplex.HomComplex.Cochain.ofHoms ψ =
    CochainComplex.HomComplex.Cochain.mk fun p q hpq =>
      CategoryTheory.CategoryStruct.comp (ψ p) (CategoryTheory.eqToHom ⋯)