Properties of the truncated simplex category

We prove that for n > 0, the inclusion functor from the n-truncated simplex category to the untruncated simplex category, and the inclusion functor from the n-truncated to the m-truncated simplex category, for n ≤ m are initial.

instance SimplexCategory.Truncated.initial_inclusion {n : ℕ} [NeZero n] : (inclusion n).Initial

For 0 < n, the inclusion functor from the n-truncated simplex category to the untruncated simplex category is initial.

theorem SimplexCategory.Truncated.initial_incl {n m : ℕ} [NeZero n] (hm : n ≤ m) : (incl n m hm).Initial

For 0 < n ≤ m, the inclusion functor from the n-truncated simplex category to the m-truncated simplex category is initial.