(directed enhancement of homotopy type theory with types behaving like $(\infty,n)$-categories)
(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
In dependent type theory with a notion of hom type (i.e. modelling $\infty$-categories as envisioned in directed homotopy type theory) and a notion of type universe, the directed univalence axiom for a type universe $U$ states that given two $U$-small types $A \colon U$ and $B \colon U$ there is an equivalence of types between the hom-type $\mathrm{hom}_U(A, B)$ and the function type $A \to B$:
The definition also makes sense in analytic models of (infinity,1)-categories such as those constructed from simplicial sets.
In simplicial homotopy type theory, let $A$ be a Segal type and let $x:A \vdash B(x)$ be a covariant type family. The covariant type family $x:A \vdash B(x)$ satisfies the directed univalence axiom if given two elements $x \colon A$ and $y \colon A$ there is an equivalence of types between the hom type $\mathrm{hom}_A(x, y)$ and the function type $B(x) \to B(y)$:
Hoang Kim Nguyen, Directed univalence in simplicial sets, talk in Homotopy Type Theory Electronic Seminar Talks (March 2023) [video, slides]
Emily Riehl, Michael Shulman, A type theory for synthetic $\infty$-categories $[$arXiv:1705.07442$]$
César Bardomiano Martínez, Limits and colimits of synthetic $\infty$-categories $[$arXiv:2202.12386$]$
Last revised on May 21, 2023 at 23:29:31. See the history of this page for a list of all contributions to it.