∀ {C₁ : Type u_8} {C₂ : Type u_2} {D : Type u_6} [inst : CategoryTheory.Category.{u_7, u_8} C₁]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_5, u_6} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {K₁ K₁' : HomologicalComplex C₁ c₁} (f : K₁ ⟶ K₁')
  ⦃X Y : HomologicalComplex C₂ c₂⦄ (f_1 : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.mapBifunctorHomologicalComplexObj c₂ K₁).map f_1)
      (HomologicalComplex₂.homMk (((CategoryTheory.GradedObject.mapBifunctor F I₁ I₂).map f.f).app Y.X) ⋯ ⋯) =
    CategoryTheory.CategoryStruct.comp
      (HomologicalComplex₂.homMk (((CategoryTheory.GradedObject.mapBifunctor F I₁ I₂).map f.f).app X.X) ⋯ ⋯)
      ((F.mapBifunctorHomologicalComplexObj c₂ K₁').map f_1)