nLab directed univalence axiom

Contents

 Idea

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 UU states that given two UU-small types A:UA \colon U and B:UB \colon U there is an equivalence of types between the hom-type hom U(A,B)\mathrm{hom}_U(A, B) and the function type ABA \to B:

dua U(A,B):hom U(A,B)(AB). \mathrm{dua}_U(A, B) \;\colon\; \mathrm{hom}_U(A, B) \,\simeq\, (A \to B) \,.

The definition also makes sense in analytic models of (infinity,1)-categories such as those constructed from simplicial sets.

Definition

In simplicial homotopy type theory

In simplicial homotopy type theory, let AA be a Segal type and let x:AB(x)x:A \vdash B(x) be a covariant type family. The covariant type family x:AB(x)x:A \vdash B(x) satisfies the directed univalence axiom if given two elements x:Ax \colon A and y:Ay \colon A there is an equivalence of types between the hom type hom A(x,y)\mathrm{hom}_A(x, y) and the function type B(x)B(y)B(x) \to B(y):

dua A(x,y):hom A(x,y)(B(x)B(y)). \mathrm{dua}_A(x, y) \;\colon\; \mathrm{hom}_A(x, y) \,\simeq\, (B(x) \to B(y)) \,.

See also

 References

Last revised on August 9, 2024 at 13:41:14. See the history of this page for a list of all contributions to it.