nLab univalent foundations for mathematics

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

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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

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

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.