∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_3} {I₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (X : HomologicalComplex₂ C c₁ c₂),
  HomologicalComplex₂.toGradedObjectMap (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id X.toGradedObject