Univalent foundations

Last updated

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from (although are also compatible with) the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The development of univalent foundations is closely related to the development of homotopy type theory.

Contents

Univalent foundations are compatible with structuralism, if an appropriate (i.e., categorical) notion of mathematical structure is adopted. [1]

History

The main ideas of univalent foundations were formulated by Vladimir Voevodsky during the years 2006 to 2009. The sole reference for the philosophical connections between univalent foundations and earlier ideas are Voevodsky's 2014 Bernays lectures. [2] The name "univalence" is due to Voevodsky. [3] [4] A more detailed discussion of the history of some of the ideas that contribute to the current state of univalent foundations can be found at the page on homotopy type theory (HoTT).

A fundamental characteristic of univalent foundations is that they—when combined with the Martin-Löf type theory (MLTT)—provide a practical system for formalization of modern mathematics. A considerable amount of mathematics has been formalized using this system and modern proof assistants such as Coq and Agda. The first such library called "Foundations" was created by Vladimir Voevodsky in 2010. [5] Now Foundations is a part of a larger development with several authors called UniMath. [6] Foundations also inspired other libraries of formalized mathematics, such as the HoTT Coq library [7] and HoTT Agda library, [8] that developed univalent ideas in new directions.

An important milestone for univalent foundations was the Bourbaki Seminar talk by Thierry Coquand [9] in June 2014.

Main concepts

Univalent foundations originated from certain attempts to create foundations of mathematics based on higher category theory. The closest earlier ideas to univalent foundations were the ideas that Michael Makkai denotes 'first-order logic with dependent sorts' (FOLDS). [10] The main distinction between univalent foundations and the foundations envisioned by Makkai is the recognition that "higher dimensional analogs of sets" correspond to infinity groupoids and that categories should be considered as higher-dimensional analogs of partially ordered sets.

Originally, univalent foundations were devised by Vladimir Voevodsky with the goal of enabling those who work in classical pure mathematics to use computers to verify their theorems and constructions. The fact that univalent foundations are inherently constructive was discovered in the process of writing the Foundations library (now part of UniMath). At present, in univalent foundations, classical mathematics is considered to be a "retract" of constructive mathematics, i.e., classical mathematics is both a subset of constructive mathematics consisting of those theorems and constructions that use the law of the excluded middle as their assumption and a "quotient" of constructive mathematics by the relation of being equivalent modulo the axiom of the excluded middle.

In the formalization system for univalent foundations that is based on Martin-Löf type theory and its descendants such as Calculus of Inductive Constructions, the higher dimensional analogs of sets are represented by types. The collection of types is stratified by the concept of h-level (or homotopy level). [11]

Types of h-level 0 are those equal to the one point type. They are also called contractible types.

Types of h-level 1 are those in which any two elements are equal. Such types are called "propositions" in univalent foundations. [11] The definition of propositions in terms of the h-level agrees with the definition suggested earlier by Awodey and Bauer. [12] So, while all propositions are types, not all types are propositions. Being a proposition is a property of a type that requires proof. For example, the first fundamental construction in univalent foundations is called iscontr. It is a function from types to types. If X is a type then iscontr X is a type that has an object if and only if X is contractible. It is a theorem (which is called, in the UniMath library, isapropiscontr) that for any X the type iscontr X has h-level 1 and therefore being a contractible type is a property. This distinction between properties that are witnessed by objects of types of h-level 1 and structures that are witnessed by objects of types of higher h-levels is very important in the univalent foundations.

Types of h-level 2 are called sets. [11] It is a theorem that the type of natural numbers has h-level 2 (isasetnat in UniMath). It is claimed by the creators of univalent foundations that the univalent formalization of sets in Martin-Löf type theory is the best currently-available environment for formal reasoning about all aspects of set-theoretical mathematics, both constructive and classical. [13]

Categories are defined (see the RezkCompletion library in UniMath) as types of h-level 3 with an additional structure that is very similar to the structure on types of h-level 2 that defines partially ordered sets. The theory of categories in univalent foundations is somewhat different and richer than the theory of categories in the set-theoretic world with the key new distinction being that between pre-categories and categories. [14]

An account of the main ideas of univalent foundations and their connection to constructive mathematics can be found in a tutorial by Thierry Coquand. [lower-alpha 1] A presentation of the main ideas from the perspective of classical mathematics can be found in the 2014 review by Alvaro Pelayo and Michael Warren, [17] as well as in the introduction [18] by Daniel Grayson. See also: Vladimir Voevodsky (2014). [19]

Current developments

An account of Voevodsky's construction of a univalent model of the Martin-Löf type theory with values in Kan simplicial sets can be found in a paper by Chris Kapulkin, Peter LeFanu Lumsdaine and Vladimir Voevodsky. [20] Univalent models with values in the categories of inverse diagrams of simplicial sets were constructed by Michael Shulman. [21] These models have shown that the univalence axiom is independent from the excluded middle axiom for propositions.

Voevodsky's model is considered to be non-constructive since it uses the axiom of choice in an ineliminable way.

The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom [lower-alpha 2] and canonicity for natural numbers remains open. A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand and Simon Huber [23] with the key remaining issue being the computational property of the eliminator for the identity types. The ideas of this paper are now being developed in several directions including the development of the cubical type theory. [24]

New directions

Most of the work on formalization of mathematics in the framework of univalent foundations is being done using various sub-systems and extensions of the Calculus of Inductive Constructions (CIC).

There are three standard problems whose solution, despite many attempts, could not be constructed using CIC:

  1. To define the types of semi-simplicial types, H-types or (infty,1)-category structures on types.
  2. To extend CIC with a universe management system that would allow implementation of the resizing rules.
  3. To develop a constructive variant of the Univalence Axiom [25]

These unsolved problems indicate that while CIC is a good system for the initial phase of the development of the univalent foundations, moving towards the use of computer proof assistants in the work on its more sophisticated aspects will require the development of a new generation of formal deduction and computation systems.

See also

Notes

  1. ↑ Thierry Coquand (2014) Univalent Foundation and Constructive Mathematics [15] [16]
  2. ↑ But see Martín Hötzel Escardó's approach. [22] : 4–6 

Related Research Articles

<span class="mw-page-title-main">Axiom of choice</span> Axiom of set theory

In mathematics, the axiom of choice, abbreviated AC or AoC, is an axiom of set theory equivalent to the statement that a Cartesian product of a collection of non-empty sets is non-empty. Informally put, the axiom of choice says that given any collection of sets, each containing at least one element, it is possible to construct a new set by choosing one element from each set, even if the collection is infinite. Formally, it states that for every indexed family of nonempty sets, there exists an indexed set such that for every . The axiom of choice was formulated in 1904 by Ernst Zermelo in order to formalize his proof of the well-ordering theorem.

<span class="mw-page-title-main">Set theory</span> Branch of mathematics that studies sets

Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory — as a branch of mathematics — is mostly concerned with those that are relevant to mathematics as a whole.

In mathematics and computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.

<span class="mw-page-title-main">Vladimir Voevodsky</span>

Vladimir Alexandrovich Voevodsky was a Russian-American mathematician. His work in developing a homotopy theory for algebraic varieties and formulating motivic cohomology led to the award of a Fields Medal in 2002. He is also known for the proof of the Milnor conjecture and motivic Bloch–Kato conjectures and for the univalent foundations of mathematics and homotopy type theory.

<span class="mw-page-title-main">Institute for Advanced Study</span> Postgraduate center in Princeton, New Jersey, US

The Institute for Advanced Study (IAS) is an independent center for theoretical research and intellectual inquiry located in Princeton, New Jersey. It has served as the academic home of internationally preeminent scholars, including Albert Einstein, J. Robert Oppenheimer, Hermann Weyl, John von Neumann, and Kurt Gödel, many of whom had emigrated from Europe to the United States.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

<span class="mw-page-title-main">Universe (mathematics)</span> Collection that contains all the entities one wishes to consider in a given situation in mathematics

In mathematics, and particularly in set theory, category theory, type theory, and the foundations of mathematics, a universe is a collection that contains all the entities one wishes to consider in a given situation.

Intuitionistic type theory is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

In mathematics, particularly in homotopy theory, a model category is a category with distinguished classes of morphisms ('arrows') called 'weak equivalences', 'fibrations' and 'cofibrations' satisfying certain axioms relating them. These abstract from the category of topological spaces or of chain complexes. The concept was introduced by Daniel G. Quillen (1967).

<span class="mw-page-title-main">Agda (programming language)</span> Functional programming language

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.

In algebraic geometry and algebraic topology, branches of mathematics, A1homotopy theory or motivic homotopy theory is a way to apply the techniques of algebraic topology, specifically homotopy, to algebraic varieties and, more generally, to schemes. The theory is due to Fabien Morel and Vladimir Voevodsky. The underlying idea is that it should be possible to develop a purely algebraic approach to homotopy theory by replacing the unit interval [0, 1], which is not an algebraic variety, with the affine line A1, which is. The theory has seen spectacular applications such as Voevodsky's construction of the derived category of mixed motives and the proof of the Milnor and Bloch-Kato conjectures.

In type theory, a system has inductive types if it has facilities for creating a new type from constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

In mathematics, more specifically category theory, a quasi-category is a generalization of the notion of a category. The study of such generalizations is known as higher category theory.

<span class="mw-page-title-main">Homotopy type theory</span> Type theory in logic and mathematics

In mathematical logic and computer science, homotopy type theory refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.

Thomas Streicher is an Austrian mathematician who is a Professor of Mathematics at Technische Universität Darmstadt. He received his PhD in 1988 from the University of Passau with advisor Manfred Broy.

Pursuing Stacks is an influential 1983 mathematical manuscript by Alexander Grothendieck. It consists of a 12-page letter to Daniel Quillen followed by about 600 pages of research notes.

In type theory, the identity type represents the concept of equality. It is also known as propositional equality to differentiate it from "judgemental equality". Equality in type theory is a complex topic and has been the subject of research, such as the field of homotopy type theory.

Michael "Mike" Shulman is an American associate professor of mathematics at the University of San Diego who works in category theory and higher category theory, homotopy theory, logic as applied to set theory, and computer science.

In type theory, a polynomial functor is a kind of endofunctor of a category of types that is intimately related to the concept of inductive and coinductive types. Specifically, all W-types are initial algebras of such functors.

Mikhail Kapranov, is a Russian mathematician, specializing in algebraic geometry, representation theory, mathematical physics, and category theory. He is currently a professor of the Kavli Institute for the Physics and Mathematics of the Universe at the University of Tokyo.

References

  1. ↑ Awodey, Steve (2014). "Structuralism, Invariance, and Univalence" (PDF). Philosophia Mathematica . 22 (1): 1–11. CiteSeerX   10.1.1.691.8113 . doi:10.1093/philmat/nkt030.
  2. ↑ Voevodsky, Vladimir (September 9–10, 2014). "Foundations of mathematics — their past, present and future". The 2014 Paul Bernays Lectures. ETH Zurich. See item 11 at Voevodsky Lectures
  3. ↑ univalence axiom in nLab
  4. ↑ Martín Hötzel Escardó (October 18, 2018) A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom
  5. ↑ Foundations library, see https://github.com/vladimirias/Foundations
  6. ↑ UniMath library, see https://github.com/UniMath/UniMath
  7. ↑ HoTT Coq library, see https://github.com/HoTT/HoTT
  8. ↑ HoTT Agda library, see https://github.com/HoTT/HoTT-Agda
  9. ↑ Coquand's Bourbaki Lecture Paper and Video
  10. ↑ Makkai, M. (1995). "First Order Logic with Dependent Sorts, with Applications to Category Theory" (PDF). FOLDS.
  11. 1 2 3 See Pelayo & Warren 2014 , p. 611
  12. ↑ Awodey, Steven; Bauer, Andrej (2004). "Propositions as [types]" . J. Log. Comput. 14 (4): 447–471. doi:10.1093/logcom/14.4.447.
  13. ↑ Voevodsky 2014 , Lecture 3, slide 11
  14. ↑ See Ahrens, Benedikt; Kapulkin, Chris; Shulman, Michael (2015). "Univalent categories and the Rezk completion". Mathematical Structures in Computer Science. 25 (5): 1010–1039. arXiv: 1303.0584 . doi:10.1017/S0960129514000486. S2CID   1135785.
  15. ↑ Coquand (2014) part 1
  16. ↑ Coquand (2014) part 2
  17. ↑ Pelayo, Álvaro; Warren, Michael A. (2014). "Homotopy type theory and Voevodsky's univalent foundations". Bulletin of the American Mathematical Society. 51 (4): 597–648. arXiv: 1210.5658 . doi: 10.1090/S0273-0979-2014-01456-9 .
  18. ↑ Grayson, Daniel R. (2018). "An introduction to univalent foundations for mathematicians". Bulletin of the American Mathematical Society. 55 (4): 427–450. arXiv: 1711.01477 . doi:10.1090/bull/1616. S2CID   32293255.
  19. ↑ Vladimir Voevodsky (2014) Experimental library of univalent formalization of mathematics
  20. ↑ Kapulkin, Chris; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir (2012). "The Simplicial Model of Univalent Foundations". arXiv: 1211.2851 [math.LO].
  21. ↑ Shulman, Michael (2015). "Univalence for inverse diagrams and homotopy canonicity". Mathematical Structures in Computer Science. 25 (5): 1203–1277. arXiv: 1203.3253 . doi:10.1017/S0960129514000565. S2CID   13595170.
  22. ↑ Martín Hötzel Escardó (October 18, 2018) A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom
  23. ↑ Bezem, M.; Coquand, T.; Huber, S. "A model of type theory in cubical sets" (PDF).
  24. ↑ Altenkirch, Thorsten; Kaposi, Ambrus, A syntax for cubical type theory (PDF)
  25. ↑ V. Voevodsky, Univalent Foundations Project (a modified version of an NSF grant application), p. 9
Libraries of formalized mathematics
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.