∀ {ι : Type u_1} (W₁ : Type u_3) [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms W₁] (c : ComplexShape ι) (X : HomologicalComplex W₁ c) (i : ι),
  ((CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).hom.app X).f i = CategoryTheory.CategoryStruct.id (X.X i)