Homotopy Type Theory simplex category > history (Rev #2)

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)

Homotopy Type Theory simplex category > history (Rev #2)

Definition

See also