∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂}
  {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (j j' : J),
  HomologicalComplex.mapBifunctorMapHomotopy.hom₂ f₁ h₂ F c j j' =
    (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).totalDesc fun i₁ i₂ x =>
      c₁.ε₂ c₂ c (i₁, c₂.prev i₂) •
        CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂))
          (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (h₂.hom i₂ (c₂.prev i₂)))
            (L₁.ιMapBifunctorOrZero L₂ F c i₁ (c₂.prev i₂) j'))