∀ (X : SSet),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (SSet.stdSimplex.obj (SimplexCategory.mk 1))) =
    CategoryTheory.CategoryStruct.id X