simplex category

The simplex category is defined as full subcategory of Category Pos, that is

1. isomorphism classes of sets \([n] = \{0,1...,n\}\) for \(n \in \mathbb{N}\) with the natural linear order as objects
2. (weakly) monotone maps \(\varphi: [n] \rightarrow [m]\)