∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c),
  ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₂ = CategoryTheory.CategoryStruct.id (X.X j)