∀ {C₁ : Type u_6} {C₂ : Type u_4} {D : Type u_2} [inst : CategoryTheory.Category.{u_5, u_6} C₁]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C₂] [inst_2 : CategoryTheory.Category.{u_1, u_2} 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] (K₁ : CochainComplex C₁ ℤ)
  (K₂ : CochainComplex C₂ ℤ) (p q : ℤ),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso
              (F.map₂CochainComplex.obj ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) p).obj K₁)) q).hom.app
        K₂)
      ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) q).map
        ((CategoryTheory.Functor.commShiftIso (F.map₂CochainComplex.flip.obj K₂) p).hom.app K₁)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso
              (F.map₂CochainComplex.flip.obj ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) q).obj K₂)) p).hom.app
        K₁)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) p).map
          ((CategoryTheory.Functor.commShiftIso (F.map₂CochainComplex.obj K₁) q).hom.app K₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm ((F.map₂CochainComplex.obj K₁).obj K₂) p q).inv
          ((↑(CategoryTheory.CommShift₂Setup.int.ε p q)).app
            ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) q).obj
              ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) p).obj ((F.map₂CochainComplex.obj K₁).obj K₂))))))