An introduction to univalent foundations for mathematicians. (English) Zbl 1461.03012

Grayson, Daniel R.

Bull. Am. Math. Soc., New Ser. 55, No. 4, 427-450 (2018).

Summary: We offer an introduction for mathematicians to the univalent foundations of Vladimir Voevodsky, aiming to explain how he chose to encode mathematics in type theory and how the encoding reveals a potentially viable foundation for all of modern mathematics that can serve as an alternative to set theory.

MSC:

03B38	Type theory
03B35	Mechanization of proofs and logical operations
03G30	Categorical logic, topoi
18A15	Foundations, relations to logic and deductive systems
55U35	Abstract and axiomatic homotopy theory in algebraic topology

Keywords:

homotopy type theory; type theory; identity type; univalence axiom; univalent mathematics

Software:

GitHub; Automath; HoTT; kepler98; cart-cube; Coq; UniMath; Lean; cubicaltt; RedPRL

References:

[1]	HoTT-Agda Homotopy Type Theory in Agda, an Agda library of formalized proofs, available at https://github.com/HoTT/HoTT-Agda.
[2]	Lean Lean theorem prover, a proof assistant together with a library of formalized proofs, available at https://github.com/leanprover/lean.
[3]	RedPRL RedPRL, a proof assistant for Computational Cubical Type Theory together with a library of formalized proofs, available at http://www.redprl.org/.
[4]	HoTT The HoTT Library, a Coq library of formalized proofs, available at https://github.com/HoTT/HoTT.
[5]	Ahrens, Benedikt; Kapulkin, Krzysztof; Shulman, Michael, Univalent categories and the Rezk completion, Math. Structures Comput. Sci., 25, 5, 1010-1039 (2015) · Zbl 1362.18003
[6]	1703.09050 Mathieu Anel, Georg Biedermann, Eric Finster, and Andr\'e Joyal, A generalized Blakers-Massey theorem, 2017, preprint available at http://arxiv.org/abs/1703.09050. · Zbl 1456.18017
[7]	1703.09632 Mathieu Anel, Georg Biedermann, Eric Finster, and Andre\'e Joyal, Goodwillie’s calculus of functors and higher topos theory, 2017, preprint available at http://arxiv.org/abs/1703.09632. · Zbl 1423.18009
[8]	cart-cube Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou, Robert Harper, and Daniel R. Licata, Cartesian cubical type theory, 2017, available at https://github.com/dlicata335/cart-cube/raw/master/cart-cube.pdf.
[9]	harper-et-al-2 Carlo Angiuli and Robert Harper, Computational higher type theory II: Dependent cubical realizability, 2016, preprint available at http://arxiv.org/abs/1606.09638.
[10]	harper-et-al-1 Carlo Angiuli, Robert Harper, and Todd Wilson, Computational higher type theory I: Abstract cubical realizability, 2016, preprint available at http://arxiv.org/abs/1604.08873. · Zbl 1380.68112
[11]	harper-et-al-3 Carlo Angiuli, Kuen-Bang Hou, and Robert Harper, Computational higher type theory III: Univalent universes and exact equality, 2017, preprint available at http://arxiv.org/abs/#11712.01800.
[12]	Appel, K.; Haken, W., Every planar map is four colorable. I. Discharging, Illinois J. Math., 21, 3, 429-490 (1977) · Zbl 0387.05009
[13]	Appel, K.; Haken, W.; Koch, J., Every planar map is four colorable. II. Reducibility, Illinois J. Math., 21, 3, 491-567 (1977) · Zbl 0387.05010
[14]	10.2307/986491 Kenneth I. Appel, The use of the computer in the proof of the four color theorem, Proc. Amer. Philos. Soc. 128 (1984), no. 1, 35-39.
[15]	Awodey, Steve; Warren, Michael A., Homotopy theoretic models of identity types, Math. Proc. Cambridge Philos. Soc., 146, 1, 45-55 (2009) · Zbl 1205.03065
[16]	Awodey, Steven; Bauer, Andrej, Propositions as \textup{[}types\textup{]}, J. Logic Comput., 14, 4, 447-471 (2004) · Zbl 1050.03016
[17]	1610.04591 Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, and Bas Spitters, The HoTT Library: A formalization of homotopy type theory in Coq, 2016, preprint available at http://arxiv.org/abs/1610.04591.
[18]	Beilinson, A., I. M. Gelfand and his seminar-a presence, Notices Amer. Math. Soc., 63, 3, 295-298 (2016) · Zbl 1338.01027
[19]	Bernays, Paul, A system of axiomatic set theory. Part II, J. Symbolic Logic, 6, 1-17 (1941) · Zbl 0026.20502
[20]	Bezem, Marc; Coquand, Thierry; Huber, Simon, A model of type theory in cubical sets. 19th International Conference on Types for Proofs and Programs, LIPIcs. Leibniz Int. Proc. Inform. 26, 107-128 (2014), Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern · Zbl 1359.03009
[21]	1606.05916 Guillaume Brunerie, On the homotopy groups of spheres in homotopy type theory, 2016, Ph.D. thesis, preprint available at http://arxiv.org/abs/1606.05916. · Zbl 1477.03035
[22]	1710.10307 Guillaume Brunerie, The James construction and \(\pi_4(\mathbbS^3)\) in homotopy type theory, 2017, preprint available at http://arxiv.org/abs/1710.10307; Journal of Automated Reasoning (to appear). · Zbl 1477.03035
[23]	1802.02191 Ulrik Buchholtz and Kuen-Bang (Favonia) Hou, Cellular cohomology in homotopy type theory, February, 2018, preprint available at http://arxiv.org/abs/1802.02191.
[24]	harper-et-al-4 Evan Cavallo and Robert Harper, Computational higher type theory IV: Inductive types, 2018, preprint available at http://arxiv.org/abs/1801.01568.
[25]	cubicaltt Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\"ortberg, Experimental implementation of cubical type theory, the proof assistant cubical, written in Haskell, available at https://github.com/mortberg/cubicaltt. · Zbl 1434.03036
[26]	1611.02108 Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\"ortberg, Cubical type theory: A constructive interpretation of the univalence axiom (2015), to appear in the post-proceedings of TYPES 2015. Preprint avaiable at https://arxiv.org/abs/1611.02108. · Zbl 1434.03036
[27]	Coquand, Thierry, Th\'eorie des types d\'ependants et axiome d’univalence, Ast\'erisque, 367-368, Exp. No. 1085, x, 367-386 (2015) · Zbl 1356.03002
[28]	de Bruijn, N. G., The mathematical language AUTOMATH, its usage, and some of its extensions. Symposium on Automatic Demonstration, Versailles, 1968, 29-61 (1970), Lecture Notes in Mathematics, Vol. 125. Springer, Berlin
[29]	Gonthier, Georges, Formal proof-the four-color theorem, Notices Amer. Math. Soc., 55, 11, 1382-1393 (2008) · Zbl 1195.05026
[30]	10.1007/978-3-642-39634-2_14 Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Francois Garillot, St\'ephane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Th\'ery, A machine-checked proof of the odd order theorem, Interactive Theorem Proving (Berlin, Heidelberg) (Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, eds.), Springer Berlin Heidelberg, 2013, pp. 163-179. · Zbl 1317.68211
[31]	Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Le Truong Hoang; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland, A formal proof of the Kepler conjecture, Forum Math., Pi, 5, e2, 29 pp. (2017) · Zbl 1379.52018
[32]	Hou, Kuen-Bang; Shulman, Michael, The Seifert-van Kampen theorem in homotopy type theory. Computer Science Logic 2016, LIPIcs. Leibniz Int. Proc. Inform. 62, Art. No. 22, 16 pp. (2016), Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern · Zbl 1370.03015
[33]	1605.03227 Kuen-Bang Hou (Favonia) Hou, Eric Finster, Dan Licata, and Peter LeFanu Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory, 2016, preprint available at http://arxiv.org/abs/1605.03227. · Zbl 1395.55011
[34]	1211.2851 Chris Kapulkin and Peter LeFanu Lumsdaine, The simplicial model of univalent foundations (after Voevodsky), 2012, preprint available at http://arxiv.org/abs/1211.2851. · Zbl 1452.03038
[35]	1610.00037 Chris Kapulkin and Peter LeFanu Lumsdaine, The homotopy theory of type theories, 2016, preprint available at http://arxiv.org/abs/1610.00037. · Zbl 1452.03038
[36]	1203.2553 Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky, Univalence in simplicial sets, 2012, preprint available at http://arxiv.org/abs/1203.2553. · Zbl 1452.03038
[37]	1709.09519 Chris Kapulkin and Karol Szumio, Internal language of finitely complete \((\infty ,1)\)-categories, 2017, preprint available at http://arxiv.org/abs/1709.09519.
[38]	Licata, Daniel R.; Shulman, Michael, Calculating the fundamental group of the circle in homotopy type theory. 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), 223-232 (2013), IEEE Computer Soc., Los Alamitos, CA · Zbl 1369.03097
[39]	1705.07088 Peter LeFanu Lumsdaine and Mike Shulman, Semantics of higher inductive types, 2017, preprint available at http://arxiv.org/abs/1705.07088.
[40]	Makkai, M., Towards a categorical foundation of mathematics. Logic Colloquium ’95 (Haifa), Lecture Notes Logic 11, 153-190 (1998), Springer, Berlin · Zbl 0896.03051
[41]	Martin-L\"of, Per, Hauptsatz for the intuitionistic theory of iterated inductive definitions. Proceedings of the Second Scandinavian Logic Symposium, Univ. Oslo, Oslo, 1970, Studies in Logic and the Foundations of Mathematics 63, 179-216 (1971), North-Holland, Amsterdam
[42]	Martin-L\`“of, Per, An intuitionistic theory of types: predicative part. Logic Colloquium ”73, Bristol, 1973, Studies in Logic and the Foundations of Mathematics 80, 73-118 (1975), North-Holland, Amsterdam
[43]	Martin-L\"of, Per, Constructive mathematics and computer programming. Logic, Methodology and Philosophy of Science, VI, Hannover, 1979, Stud. Logic Found. Math. 104, 153-175 (1982), North-Holland, Amsterdam
[44]	mcall David McAllester, Morphoid type theory, a typed platonic foundation for mathematics, preprint available at http://arxiv.org/abs/1407.7274.
[45]	peano-principia Ioseph Peano, Arithmetices principia, Fratres Bocca, 1889.
[46]	RezkBM Charles Rezk, Proof of the Blakers-Massey theorem, available at https://faculty.math.illinois.edu/ rezk/freudenthal-and-blakers-massey.pdf.
[47]	Russell, Bertrand, Mathematical logic as based on the theory of types, Amer. J. Math., 30, 3, 222-262 (1908) · JFM 39.0085.03
[48]	Swansea-Shulman Michael Shulman, Minicourse on homotopy type theory, slides from a talk, available at http://home.sandiego.edu/ shulman/hottminicourse2012/, 2012.
[49]	1509.07584 Michael Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, 2015, preprint available at http://arxiv.org/abs/1509.07584. · Zbl 1390.03014
[50]	1703.03007 Michael Shulman, Homotopy type theory: the logic of space, 2017, preprint available at http://arxiv.org/abs/1703.03007.
[51]	Coq The Coq Development Team, The Coq proof assistant, Available at https://coq.inria.fr/. · Zbl 1342.68280
[52]	1802.01170 Coquand Thierry, Simon Huber, and Anders M\"ortberg, On higher inductive types in cubical type theory, 2018, preprint available at http://arxiv.org/abs/1802.01170. · Zbl 1452.03036
[53]	Tsem4 D. Tsementzis, A meaning explanation for HoTT, (2016), Available at http://philsci-archive.pitt.edu/12824/.
[54]	Tsementzis, Dimitris, Univalent foundations as structuralist foundations, Synthese, 194, 9, 3583-3617 (2017) · Zbl 1400.03023
[55]	Tsem2 Dimitris Tsementzis, What is a higher-level set?, Philosophia Mathematica (2017), (forthcoming), Available at https://academic.oup.com/philmat/article-abstract/2895117/What-is-a-Higher-Level-Set.
[56]	Tsem3 D. Tsementzis and H. Halvorson, Foundations and philosophy, Philosopher’s Imprint (forthcoming) (2017), Available at http://philsci-archive.pitt.edu/13504/.
[57]	The Univalent Foundations Program, Homotopy type theory, xiv+589 pp. (2013), The Univalent Foundations Program, Princeton, NJ; Institute for Advanced Study (IAS), Princeton, NJ · Zbl 1298.03002
[58]	Foundations Vladimir Voevodsky, Foundations: Development of the univalent foundations of mathematics in Coq, a Coq library of formalized proofs, available at https://github.com/vladimirias/Foundations. · Zbl 1361.68192
[59]	VV-resizing Vladimir Voevodsky, Resizing rules-Their use and semantic justification, slides from a talk available at https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2011_Bergen.pdf, 2011.
[60]	40 Vladimir Voevodsky, B-systems, 2014, preprint available at http://arxiv.org/abs/1410.5389.
[61]	42 Vladimir Voevodsky, C-system of a module over a monad on sets, 2014, preprint available at http://arxiv.org/abs/1407.3394.
[62]	VV-IHP-talk Vladimir Voevodsky, Univalent foundations-new type-theoretic foundations of mathematics, slides from a talk at IHP, Paris, on April 22, 2014, available at https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_04_22_slides.pdf, 2014.
[63]	Voevodsky, Vladimir, A C-system defined by a universe category, Theory Appl. Categ., 30, Paper No. 37, 1181-1215 (2015) · Zbl 1436.03311
[64]	Voevodsky, Vladimir, An experimental library of formalized mathematics based on the univalent foundations, Math. Structures Comput. Sci., 25, 5, 1278-1294 (2015) · Zbl 1361.68192
[65]	103 Vladimir Voevodsky, Martin-L\"of identity types in the C-systems defined by a universe category, 2015, preprint available at http://arxiv.org/abs/1505.06446, pp. 1-51.
[66]	104 Vladimir Voevodsky, Products of families of types in the C-systems defined by a universe category, 2015, preprint available at http://arxiv.org/abs/1503.07072.
[67]	110 Vladimir Voevodsky, Lawvere theories and Jf-relative monads, (2016), 1-21, preprint available at http://arxiv.org/abs/1601.02158.
[68]	Voevodsky, Vladimir, Products of families of types and \((\Pi,\lambda)\)-structures on C-systems, Theory Appl. Categ., 31, Paper No. 36, 1044-1094 (2016) · Zbl 1380.03072
[69]	Voevodsky, Vladimir, Subsystems and regular quotients of C-systems. A panorama of mathematics: pure and applied, Contemp. Math. 658, 127-137 (2016), Amer. Math. Soc., Providence, RI · Zbl 1452.03040
[70]	Voevodsky, Vladimir, C-systems defined by universe categories: presheaves, Theory Appl. Categ., 32, Paper No. 3, 53-112 (2017) · Zbl 1453.03067
[71]	Voevodsky, Vladimir, The \((\Pi, \lambda)\)-structures on the C-systems defined by universe categories, Theory Appl. Categ., 32, Paper No. 4, 113-121 (2017) · Zbl 1383.03056
[72]	UniMath Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al., UniMath-a computer-checked library of univalent mathematics, available at http://UniMath.org.