{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          {D : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_1, u_2} D] →
              [inst_3 : CategoryTheory.Preadditive D] →
                CochainComplex.HomComplex.Cochain K L n →
                  (Φ : CategoryTheory.Functor C D) →
                    [inst_4 : Φ.Additive] →
                      CochainComplex.HomComplex.Cochain ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)
                        ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) n