∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {x y : S₁.HomotopyEquiv S₂},
  x.hom = y.hom →
    x.inv = y.inv → x.homotopyHomInvId ≍ y.homotopyHomInvId → x.homotopyInvHomId ≍ y.homotopyInvHomId → x = y