∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangleh φ₁).mor₁
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b) =
    CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a)
      (CochainComplex.mappingCone.triangleh φ₂).mor₁