(directed enhancement of homotopy type theory with types behaving like -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 -categories as envisioned in directed homotopy type theory) and a notion of type universe, the directed univalence axiom for a type universe states that given two -small types and there is an equivalence of types between the hom-type and the function type :
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 be a Segal type and let be a covariant type family. The covariant type family satisfies the directed univalence axiom if given two elements and there is an equivalence of types between the hom type and the function type :
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 -categories arXiv:1705.07442
César Bardomiano Martínez, Limits and colimits of synthetic -categories arXiv:2202.12386
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)
Last revised on August 9, 2024 at 13:41:14. See the history of this page for a list of all contributions to it.