∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_3) [inst_1 : CategoryTheory.Category.{u_2, u_3} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)),
  CategoryTheory.CategoryStruct.comp
      ((HomologicalComplex.dgoToHomologicalComplex b V).map
        ((HomologicalComplex.dgoEquivHomologicalComplexUnitIso b V).hom.app X))
      ((HomologicalComplex.dgoEquivHomologicalComplexCounitIso b V).hom.app
        ((HomologicalComplex.dgoToHomologicalComplex b V).obj X)) =
    CategoryTheory.CategoryStruct.id ((HomologicalComplex.dgoToHomologicalComplex b V).obj X)