nLab univalent foundations for mathematics

Idea

A univalent foundations for mathematics refers to any foundational system in which universes are object classifiers, or, equivalently, satisfy the univalence axiom.

Specifically, this applies to mathematical foundations in (a) dependent type theory, or in (b) topos theory, respectively, which – apart from exactly such fine-print on the existence and nature of universes – correspond to each other under the syntax/semantics-relation between type theory and category theory.

Here, univalent foundations is in contrast to other (earlier) approaches of laying foundations in type theories or toposes, that have (only) a universe of propositions or (only) a subobject classifier, respectively, hence where only a truncated sub-class of all types/objects is reflected in the universe.

The basic idea of univalent foundations is, simply, to allow for universes that reflect all types/objects. Or rather – to avoid the notorious inconsistencies of the form of Russell's paradox/Girard's paradox – universes that reflect all those types/objects that are “small” compared to the universe. It is this technical subtlety – due to which a type/object may not be reflected in a given universe (namely if it is too large) but if it is, then it is so essentially uniquely – which motivates the term “univalent”.

The term “univalent foundations” as such was coined by Voevodsky 11, much popularized with the textbook UFIAS 12, and is usually taken to refer to mathematical foundations based on Martin-Löf dependent type theory, or similar, with the univalence axiom imposed on the type universe. But the existence of (the categorical semantics of) such “univalent type universes” in higher analogues of toposes (“∞-toposes”) was observed (and published) earlier in Lurie 09, Sec. 6.1.6, there called object classifiers and attributed to yet earlier private conversation with Charles Rezk.

That both concepts,

1. univalent$\,$universes in type theory

2. object classifiers in (elementary) ∞-toposes

do indeed correspond to each other was understood from the beginning (see Shulman 12a, lecture 3, slide 3, for the statement); based on proofs in special cases (Shulman 12b). Full proof appeared in Shulman 19.

Concretely, what makes univalent foundations univalent is the condition, respectively,

1. that there exists a type universe $Type$ (also often denoted $\mathcal{U}$) which reflects types and their equivalences, in that for any two types $A,B$ in that universe, them being equivalent as types is equivalent to them being equivalent (“equal”) as terms of type $Type$;

   the usual formal syntax for this statement of the univalence axiom is the famous expression

   $$\underset{ \color{blue} \text{equivalence as types} }{ (A \simeq B) } \underset{ \color{blue} \;\;\text{univalence}\;\; }{ \simeq } \underset{ \color{blue} \text{equivalence as terms} \atop \color{blue} \text{in the type universe} }{ (A = B) }$$

2. that there exists an object classifier $Object$ which reflects objects and their equivalences, in that for any two objects $A,B$ them being equivalent as objects is equivalent to their classifying maps to $Object$ being equivalent (homotopic).

In higher topos theory

See at object classifier (in (∞,1)-toposes).

In homotopy type theory

Voevodsky’s univalent foundations (UFIAS 12) are an extension of Martin-Löf's dependent type theory obtained by adding:

• the univalence axiom,

• propositional truncations.

Notice that:

• function extensionality is implied by the univalence axiom, so it is not necessary to assume separately;

• propositional resizing is sometimes also included as an axiom;

• the UniMath library also uses type in type, i.e., the axiom that the type universe contains itself. Strictly speaking, this makes the system inconsistent, due to Girard's paradox. But the idea is that in practice the inconsistencies are readily avoided, so that the axiom serves as a convenient hack.

• The axiom of choice is consistent with the univalent foundations of mathematics and may be assumed separately.

Overview of the basic concepts

A map $f:A\to B$ is an equivalence if it has a section and a retraction. The univalence axiom asserts that for any two types $A,B:\mathcal{U}$, the canonical map $(A=B)\to (A\simeq B)$ obtained via the induction principle of the identity type, is an equivalence.

In the univalent foundations, one can distinguish between property and structure (in general, higher structure). Being an equivalence, for instance, should be a property. There is a hierarchy of homotopy levels that starts at the level of contractible types. The next level consists of types of which each identity type is contractible. Such types are called propositions. The fact that being an equivalence is a property is proven by showing that $\mathsf{is{-}equiv}(f)$ is a proposition in the above sense.

Types of which the identity types are propositions are called sets. Many familiar types, such as the types of natural numbers, integers, and real numbers are sets in this sense, and in many subjects of algebra, such as groups, rings, modules, and so on, it is assumed that the underlying types are sets. The axiom of choice is also restricted to sets, because there are surjective maps between other types that provably do not split. For instance, the double cover of the circle has no section, while each of its fibers is inhabited by two points. We say that sets are of homotopy level $0$. A type is said to be of homotopy level $n+1$ if its identity types are of homotopy level $n$.

By the univalence axiom, we often have nice characterizations of “the type of a certain kind of thing”. For instance, the type of $n$-dimensional vector spaces (over a discrete field) is the classifying space of the general linear group $GL(n)$. Similarly, the type of $n$-element sets is the classifying space of the symmetric group $\Sigma_n$, and the type of cyclically ordered $n$-element sets is the classifying space of the cyclic group $\mathrm{C}_n$. Such observations follow from the fact that the loop space of the type of objects of a certain kind is equivalent to the type of automorphisms of that kind.

Related entries

• univalence axiom

• UniMath project

• modal homotopy type theory

• higher structures

References

In higher topos theory

• Jacob Lurie, Section 6.1.6 of: Higher Topos Theory (attributed there to Charles Rezk)

In type theory

Texts

Comprehensive introduction motivated form the concept of symmetry:

• Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson: Symmetry (2021) $[$pdf$]$

See also:

• Univalent foundations webpage

• Vladimir Voevodsky, Univalent foundations, talk at IAS 2011 (pdf)

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (web, pdf, PM wiki version)

• David Corfield, Modal homotopy type theory, Oxford University Press 2020 (ISBN: 9780198853404) doi:10.1093/oso/9780198853404.001.0001

Formalization libraries

• UniMath

• Coq HoTT library

• Agda HoTT library

• Martin Escardo, Introduction to Univalent Foundations of Mathematics with Agda. (ArXiv, web, GitHub)

• Egbert Rijke, Introduction to Homotopy Type Theory (GitHub)

Relation between higher topos theory and univalent type theory

• Michael Shulman, Minicourse on Homotopy Type Theory 2012 (webpage)

• Michael Shulman, The univalence axiom for inverse diagrams (arXiv:1203.3253).

• Michael Shulman, All $(\infty,1)$-toposes have strict univalent universes (arXiv:1904.07004).