∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₃ ⟶ S₁),
  (CategoryTheory.CategoryStruct.comp ψ φ₁).τ₂ =
    CategoryTheory.CategoryStruct.comp S₃.g (CategoryTheory.CategoryStruct.comp ψ.τ₃ h.h₂) +
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ψ.τ₂ h.h₁) S₂.f +
      (CategoryTheory.CategoryStruct.comp ψ φ₂).τ₂