∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_3} (c : ComplexShape ι) (i j k : ι) (X : HomologicalComplex C c),
  { τ₁ := (CategoryTheory.CategoryStruct.id X).f i, τ₂ := (CategoryTheory.CategoryStruct.id X).f j,
      τ₃ := (CategoryTheory.CategoryStruct.id X).f k, comm₁₂ := ⋯, comm₂₃ := ⋯ } =
    CategoryTheory.CategoryStruct.id { X₁ := X.X i, X₂ := X.X j, X₃ := X.X k, f := X.d i j, g := X.d j k, zero := ⋯ }