∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F K : HomologicalComplex C c} [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)]
  [inst_4 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K))]
  (φ₀ φ₁ : K ⟶ F) (h : Homotopy φ₀ φ₁),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K) (HomologicalComplex.cylinder.desc φ₀ φ₁ h) = φ₀