## Definition ## The __simplex category__ $\Delta_\mathcal{U}$ of a universe $\mathcal{U}$ is the category of all inhabited [[finite type|finite]] [[totally ordered type]]s in $\mathcal{U}$ whose hom types are the [[monotonic function]]s. $$\Delta_\mathcal{U} \coloneqq \sum_{n:\mathbb{N}} \sum_{A:\mathrm{Fin}_\mathcal{U}(n)} \mathrm{isTotallyOrdered}(A) \times \left[A\right]$$ $$Hom_{\Delta_\mathcal{U}}(A, B) \coloneqq \sum_{f:A \to B} \mathrm{isMonotonic}(f)$$ ## See also ## * [[finite type]] * [[totally ordered type]] * [[monotonic function]] * [[simplicial type]]