The Univalence Axiom

In intensional type theory with a universe \mathcal{U}, the univalence axiom stipulates that propositional equalities are type-theoretically equivalent to the type of (type-theoretic) equivalences.

More rigorously, for any two types A, B\ \textbf{type} we can define by path induction a function of type

  \textbf{idtoequiv} : (A =_\mathcal{U} B) \to A \simeq B

where

• A =_\mathcal{U} B is the identity type of the universe from A to B
• A \simeq B is the type of equivalences from A to B

The univalence axiom asserts that \textbf{idtoequiv} itself is an equivalence of types. People usually write

  \textbf{ua} : A \simeq B \to (A =_\mathcal{U} B)

for the quasi-inverse of \textbf{idtoequiv}.

Univalence is known to have a number of consequences, including:

• function extensionality
• propositional extensionality

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).

Book-HoTT

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 \textsf{ua} 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': \textsf{ua} is a stuck term. It is possible to prove many results about it, e.g. that for any equivalence f : A \simeq B and family \lambda X. X : \mathcal{U} \to \mathcal{U} and x : P(A) we have a proof of

	\textsf{transport}_{\lambda X. X}\ (\textsf{ua}\ f)\ x =_B f(x)

However, this is a propositional equality, and cannot be reflected into the definitional equality so as to make univalence compute.

Function extensionality

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:

• an account in Ch 4 of the HoTT book
• a proof by Dan Licata

Cubical type theory

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 (\infty, 1)-Grothendieck topos.

References

• 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 (!).

@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