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

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

Definition

< simplex category

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.

Δ 𝒰 n: A:Fin 𝒰(n)isTotallyOrdered(A)×[A]\Delta_\mathcal{U} \coloneqq \sum_{n:\mathbb{N}} \sum_{A:\mathrm{Fin}_\mathcal{U}(n)} \mathrm{isTotallyOrdered}(A) \times \left[A\right]
Hom Δ 𝒰(A,B) f:ABisMonotonic(f)Hom_{\Delta_\mathcal{U}}(A, B) \coloneqq \sum_{f:A \to B} \mathrm{isMonotonic}(f)

See also

Revision on June 10, 2022 at 17:05:13 by Anonymous?. See the history of this page for a list of all contributions to it.