∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (f f_1 : K.toGradedObject ⟶ L.toGradedObject) (e_f : f = f_1)
  (comm₁ :
    ∀ (i₁ i₁' : I₁) (i₂ : I₂),
      c₁.Rel i₁ i₁' →
        CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.d i₁ i₁').f i₂) =
          CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (f (i₁', i₂)))
  (comm₂ :
    ∀ (i₁ : I₁) (i₂ i₂' : I₂),
      c₂.Rel i₂ i₂' →
        CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.X i₁).d i₂ i₂') =
          CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (f (i₁, i₂'))),
  HomologicalComplex₂.homMk f comm₁ comm₂ = HomologicalComplex₂.homMk f_1 ⋯ ⋯