(directed enhancement of homotopy type theory with types behaving like -categories)
In dependent type theory, a hom type on a type is a dependent type which models the hom spaces of -categories.
In simplicial homotopy type theory, the hom type is defined as the extension type
where is the directed interval primitive and is the boundary of .
Last revised on May 21, 2023 at 23:06:57. See the history of this page for a list of all contributions to it.