ncatlab.org

univalent foundations for mathematics in nLab

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

homotopy levels

semantics

(∞,1)(\infty,1)-Topos Theory

(∞,1)-topos theory

structures in a cohesive (∞,1)-topos

Contents

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 TypeType (also often denoted 𝒰\mathcal{U}) which reflects types and their equivalences, in that for any two types A,BA,B in that universe, them being equivalent as types is equivalent to them being equivalent (“equal”) as terms of type TypeType;

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

    (A≃B)equivalence as types≃univalence(A=B)equivalence as termsin the type universe \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 ObjectObject which reflects objects and their equivalences, in that for any two objects A,BA,B them being equivalent as objects is equivalent to their classifying maps to ObjectObject 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:

Notice that:

Overview of the basic concepts

A map f:A→Bf: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:𝒰A,B:\mathcal{U}, the canonical map (A=B)→(A≃B)(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 is−equiv(f)\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 00. A type is said to be of homotopy level n+1n+1 if its identity types are of homotopy level nn.

By the univalence axiom, we often have nice characterizations of “the type of a certain kind of thing”. For instance, the type of nn-dimensional vector spaces (over a discrete field) is the classifying space of the general linear group GL(n)GL(n). Similarly, the type of nn-element sets is the classifying space of the symmetric group Σ n\Sigma_n, and the type of cyclically ordered nn-element sets is the classifying space of the cyclic group C n\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.

References

In higher topos theory

In type theory

Texts

Comprehensive introduction motivated form the concept of symmetry:

See also:

Formalization libraries

Relation between higher topos theory and univalent type theory

Last revised on December 22, 2022 at 13:27:49. See the history of this page for a list of all contributions to it.