∀ {C₁ : Type u_8} {C₂ : Type u_6} {D : Type u_2} [inst : CategoryTheory.Category.{u_7, u_8} C₁]
  [inst_1 : CategoryTheory.Category.{u_4, u_6} C₂] [inst_2 : CategoryTheory.Category.{u_1, u_2} 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_5} {I₂ : Type u_3} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [F.PreservesZeroMorphisms]
  (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (i₁ i₁' : I₁),
  ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), (fun i₁ i₁' i₂ => (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) i₁ i₁' i₂ = 0