nLab hom type



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


In simplicial homotopy type theory

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

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

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


Last revised on December 12, 2023 at 14:44:36. See the history of this page for a list of all contributions to it.