∀ {C₁ : Type u_2} {C₂ : Type u_4} {D : Type u_8} [inst : CategoryTheory.Category.{u_1, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{u_6, u_4} C₂] [inst_2 : CategoryTheory.Category.{u_7, u_8} 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_3} {I₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (X : HomologicalComplex C₁ c₁),
  {
      app := fun K₂ =>
        HomologicalComplex₂.homMk
          (((CategoryTheory.GradedObject.mapBifunctor F I₁ I₂).map (CategoryTheory.CategoryStruct.id X).f).app K₂.X) ⋯
          ⋯,
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id (F.mapBifunctorHomologicalComplexObj c₂ X)