# Homotopy Type Theory simplex category > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

## Definition

The

simplex category $\Delta_\mathcal{U}$ of a universe $\mathcal{U}$ is the category of all inhabited finite totally ordered types in $\mathcal{U}$ whose hom types are the monotonic functions.

$\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)$