∀ (X : SimplexCategory),
  NonemptyFinLinOrd.ofHom (SimplexCategory.Hom.toOrderHom (CategoryTheory.CategoryStruct.id X)) =
    CategoryTheory.CategoryStruct.id (NonemptyFinLinOrd.of (Fin (X.len + 1)))