∀ {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.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {I₁ : Type u_9}
  {I₂ : Type u_3} {J : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c : ComplexShape J)
  [inst_8 : DecidableEq J] [inst_9 : TotalComplexShape c₁ c₂ c]
  [inst_10 : ∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F c]
  (K₁ : HomologicalComplex C₁ c₁) (X : HomologicalComplex C₂ c₂),
  HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁) (CategoryTheory.CategoryStruct.id X) F c =
    CategoryTheory.CategoryStruct.id (K₁.mapBifunctor X F c)