∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory)
      (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C))),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.counitIso.hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left