nLab
univalent foundations for mathematics

Contents

Context

Foundations

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

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

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

(∞,1)-topos theory

Background

Definitions

Characterization

Morphisms

Extra stuff, structure and property

Models

Constructions

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

    (AB)equivalence as typesunivalence(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:ABf: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)(AB)(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 isequiv(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

Formalization libraries

Relation between higher topos theory and univalent type theory

Last revised on January 8, 2021 at 13:16:25. See the history of this page for a list of all contributions to it.