∀ {C₁ : Type u_4} {C₂ : Type u_2} {D : Type u_6} [inst : CategoryTheory.Category.{u_3, u_4} C₁]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_5, u_6} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
  {X₂ Y₂ : CochainComplex C₂ ℤ} (g : X₂ ⟶ Y₂), CategoryTheory.NatTrans.CommShift (F.map₂CochainComplex.flip.map g) ℤ