∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (X : CategoryTheory.SimplicialObject C),
  CategoryTheory.CategoryStruct.comp
      (SimplicialObject.opFunctor.map (SimplicialObject.opFunctorCompOpFunctorIso.symm.hom.app X))
      (SimplicialObject.opFunctorCompOpFunctorIso.hom.app (SimplicialObject.opFunctor.obj X)) =
    CategoryTheory.CategoryStruct.id (SimplicialObject.opFunctor.obj X)