(directed enhancement of homotopy type theory with types behaving like $(\infty,n)$-categories)

In dependent type theory, a hom type on a type $A$ is a dependent type $\mathrm{hom}_A(x, y)$ which models the hom spaces of $\infty$-categories.

In simplicial homotopy type theory, the hom type is defined as the extension type

$\mathrm{hom}_A(x, y) \coloneqq \langle \Delta^1 \to A \vert_{[x,y]}^{\partial \Delta^1} \rangle$

where $\Delta^1$ is the directed interval primitive $\mathbb{2}$ and $\partial \Delta^1$ is the boundary of $\Delta^1$.

- simplicial homotopy type theory
- directed homotopy type theory
- identity type
- function type
- directed univalence
- Segal type, Rezk type
- covariant type family

- Emily Riehl, Michael Shulman,
*A type theory for synthetic $\infty$-categories*$[$arXiv:1705.07442$]$

Last revised on May 21, 2023 at 23:06:57. See the history of this page for a list of all contributions to it.