∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (K H : C) (i : K ⟶ S.X₂) (π : K ⟶ H)
  (wi : CategoryTheory.CategoryStruct.comp i S.g = 0)
  (hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i wi))
  (wπ : CategoryTheory.CategoryStruct.comp (hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π = 0)
  (hπ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π wπ)) (K_1 H_1 : C)
  (i_1 : K_1 ⟶ S.X₂) (π_1 : K_1 ⟶ H_1) (wi_1 : CategoryTheory.CategoryStruct.comp i_1 S.g = 0)
  (hi_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i_1 wi_1))
  (wπ_1 : CategoryTheory.CategoryStruct.comp (hi_1.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π_1 = 0)
  (hπ_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π_1 wπ_1)),
  ({ K := K, H := H, i := i, π := π, wi := wi, hi := hi, wπ := wπ, hπ := hπ } =
      { K := K_1, H := H_1, i := i_1, π := π_1, wi := wi_1, hi := hi_1, wπ := wπ_1, hπ := hπ_1 }) =
    (K = K_1 ∧ H = H_1 ∧ i ≍ i_1 ∧ π ≍ π_1 ∧ hi ≍ hi_1 ∧ hπ ≍ hπ_1)