In intensional type theory with a universe , the univalence axiom stipulates that propositional equalities are type-theoretically equivalent to the type of (type-theoretic) equivalences.
More rigorously, for any two types we can define by path induction a function of type
where
The univalence axiom asserts that itself is an equivalence of types. People usually write
for the quasi-inverse of .
Univalence is known to have a number of consequences, including:
Both of these consequences are a form of extensionality. In fact, univalence is a very strong, higher-dimensional axiom of extensionality itself.
Univalence is compatible with the law of the excluded middle (LEM): see the 2020 note by Kapulkin and Lumsdaine.
Univalence is not compatible with the axiom of choice. The various shades of the failure of choice are discussed in the HoTT book (section 3.8).
Intensional type theory (with some number of universes...) augmented with univalence comprises a type theory usually referred to as (book) HoTT.
The problem with book-HoTT is that univalence is crudely bolted on as an axiom. That it: a constant of the aforementioned type is simply postulated. The computational behaviour of this additional constant is unspecified.
There is no clear way to 'make univalence compute': is a stuck term. It is possible to prove many results about it, e.g. that for any equivalence and family and we have a proof of
However, this is a propositional equality, and cannot be reflected into the definitional equality so as to make univalence compute.
It is well-known that univalence implies the axiom of function extensionality in book-HoTT. This seems to have first bene proven by Voevodsky.
There are at least two proofs of this fact:
As a response to the bad computational behaviour of HoTT researchers have developed cubical type theories. In many of these, univalence is a definable/provable term, yet they are computationally well-behaved.
The price to pay is that they are simply not the same logic as book-HoTT; in particular, we do not know if they can be interpreted in an arbitrary -Grothendieck topos.
The univalence axiom was first formulated by Vladimir Voevodsky (?).
See the nLab page on univalence.
Dan Licata's proof that univalence implies function extensionality.
The first model of univalence was in that in simplicial sets. Following a great tradition of groundbreaking papers in logic, this has taken a decade to appear in print (the first draft was circulated in 2012). Note that the construction of the model assumes two inaccessible cardinals (!).
Kapulkin, Chris, and Peter LeFanu Lumsdaine. 2018. ‘The Simplicial Model of Univalent Foundations (after Voevodsky)’. http://arxiv.org/abs/1211.2851. To appear in the Journal of the European Mathematical Society
@unpublished{kapulkin_2018,
title = {The {Simplicial} {Model} of {Univalent} {Foundations} (after {Voevodsky})},
url = {http://arxiv.org/abs/1211.2851},
author = {Kapulkin, Chris and Lumsdaine, Peter LeFanu},
year = {2018},
note = {To appear in the Journal of the European Mathematical Society}
}
That this model is compatible with LEM was shown in
Kapulkin, Chris, and Peter LeFanu Lumsdaine. 2020. ‘The Law of Excluded Middle in the Simplicial Model of Type Theory’. http://arxiv.org/abs/2006.13694.