An introduction to univalent foundations for mathematicians

Grayson, Daniel

doi:10.1090/bull/1616

An introduction to univalent foundations for mathematicians
HTML articles powered by AMS MathViewer

by Daniel R. Grayson PDF

Bull. Amer. Math. Soc. 55 (2018), 427-450

Abstract:

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.

References

Homotopy Type Theory in Agda, an Agda library of formalized proofs, available at https://github.com/HoTT/HoTT-Agda.
Lean theorem prover, a proof assistant together with a library of formalized proofs, available at https://github.com/leanprover/lean.
RedPRL, a proof assistant for Computational Cubical Type Theory together with a library of formalized proofs, available at http://www.redprl.org/.
The HoTT Library, a Coq library of formalized proofs, available at https://github.com/HoTT/HoTT.
Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman, Univalent categories and the Rezk completion, Math. Structures Comput. Sci. 25 (2015), no. 5, 1010–1039. MR 3340533, DOI 10.1017/S0960129514000486
Mathieu Anel, Georg Biedermann, Eric Finster, and André Joyal, A generalized Blakers-Massey theorem, 2017, preprint available at http://arxiv.org/abs/1703.09050.
Mathieu Anel, Georg Biedermann, Eric Finster, and Andreé Joyal, Goodwillie’s calculus of functors and higher topos theory, 2017, preprint available at http://arxiv.org/abs/1703.09632.
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.
Carlo Angiuli and Robert Harper, Computational higher type theory II: Dependent cubical realizability, 2016, preprint available at http://arxiv.org/abs/1606.09638.
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.
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.
K. Appel and W. Haken, Every planar map is four colorable. I. Discharging, Illinois J. Math. 21 (1977), no. 3, 429–490. MR 543792
K. Appel, W. Haken, and J. Koch, Every planar map is four colorable. II. Reducibility, Illinois J. Math. 21 (1977), no. 3, 491–567. MR 543793
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.
Steve Awodey and Michael A. Warren, Homotopy theoretic models of identity types, Math. Proc. Cambridge Philos. Soc. 146 (2009), no. 1, 45–55. MR 2461866, DOI 10.1017/S0305004108001783
Steven Awodey and Andrej Bauer, Propositions as [types], J. Logic Comput. 14 (2004), no. 4, 447–471. MR 2081047, DOI 10.1093/logcom/14.4.447
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.
A. Beilinson, I. M. Gelfand and his seminar—a presence, Notices Amer. Math. Soc. 63 (2016), no. 3, 295–298. MR 3445168, DOI 10.1090/noti1337
Paul Bernays, A system of axiomatic set theory. Part II, J. Symbolic Logic 6 (1941), 1–17. MR 3382, DOI 10.2307/2267281
Marc Bezem, Thierry Coquand, and Simon Huber, A model of type theory in cubical sets, 19th International Conference on Types for Proofs and Programs, LIPIcs. Leibniz Int. Proc. Inform., vol. 26, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2014, pp. 107–128. MR 3281415
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.
Guillaume Brunerie, The James construction and $\pi _4(\mathbb {S}^3)$ in homotopy type theory, 2017, preprint available at http://arxiv.org/abs/1710.10307; Journal of Automated Reasoning (to appear).
Ulrik Buchholtz and Kuen-Bang (Favonia) Hou, Cellular cohomology in homotopy type theory, February, 2018, preprint available at http://arxiv.org/abs/1802.02191.
Evan Cavallo and Robert Harper, Computational higher type theory IV: Inductive types, 2018, preprint available at http://arxiv.org/abs/1801.01568.
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, Experimental implementation of cubical type theory, the proof assistant cubical, written in Haskell, available at https://github.com/mortberg/cubicaltt.
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, 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.
Thierry Coquand, Théorie des types dépendants et axiome d’univalence, Astérisque 367-368 (2015), Exp. No. 1085, x, 367–386 (French, with French summary). MR 3363596
N. G. de Bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions, Symposium on Automatic Demonstration (Versailles, 1968) Lecture Notes in Mathematics, Vol. 125, Springer, Berlin, 1970, pp. 29–61. MR 0274219
Georges Gonthier, Formal proof—the four-color theorem, Notices Amer. Math. Soc. 55 (2008), no. 11, 1382–1393. MR 2463991
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry, 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.
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller, A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), e2, 29. MR 3659768, DOI 10.1017/fmp.2017.1
Kuen-Bang Hou and Michael Shulman, The Seifert–van Kampen theorem in homotopy type theory, Computer science logic 2016, LIPIcs. Leibniz Int. Proc. Inform., vol. 62, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2016, pp. Art. No. 22, 16. MR 3566711
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.
Chris Kapulkin and Peter LeFanu Lumsdaine, The simplicial model of univalent foundations (after Voevodsky), 2012, preprint available at http://arxiv.org/abs/1211.2851.
Chris Kapulkin and Peter LeFanu Lumsdaine, The homotopy theory of type theories, 2016, preprint available at http://arxiv.org/abs/1610.00037.
Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky, Univalence in simplicial sets, 2012, preprint available at http://arxiv.org/abs/1203.2553.
Chris Kapulkin and Karol Szumiło, Internal language of finitely complete $(\infty ,1)$-categories, 2017, preprint available at http://arxiv.org/abs/1709.09519.
Daniel R. Licata and Michael Shulman, Calculating the fundamental group of the circle in homotopy type theory, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), IEEE Computer Soc., Los Alamitos, CA, 2013, pp. 223–232. MR 3323808, DOI 10.1109/LICS.2013.28
Peter LeFanu Lumsdaine and Mike Shulman, Semantics of higher inductive types, 2017, preprint available at http://arxiv.org/abs/1705.07088.
M. Makkai, Towards a categorical foundation of mathematics, Logic Colloquium ’95 (Haifa), Lecture Notes Logic, vol. 11, Springer, Berlin, 1998, pp. 153–190. MR 1678360, DOI 10.1007/978-3-662-22108-2_{1}1
Per Martin-Löf, 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, Vol. 63, North-Holland, Amsterdam, 1971, pp. 179–216. MR 0387023
Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium ’73 (Bristol, 1973) Studies in Logic and the Foundations of Mathematics, Vol. 80, North-Holland, Amsterdam, 1975, pp. 73–118. MR 0387009
Per Martin-Löf, Constructive mathematics and computer programming, Logic, methodology and philosophy of science, VI (Hannover, 1979) Stud. Logic Found. Math., vol. 104, North-Holland, Amsterdam, 1982, pp. 153–175. MR 682410, DOI 10.1016/S0049-237X(09)70189-2
David McAllester, Morphoid type theory, a typed platonic foundation for mathematics, preprint available at http://arxiv.org/abs/1407.7274.
Ioseph Peano, Arithmetices principia, Fratres Bocca, 1889.
Charles Rezk, Proof of the Blakers-Massey theorem, available at https://faculty.math.illinois.edu/~rezk/freudenthal-and-blakers-massey.pdf.
Bertrand Russell, Mathematical Logic as Based on the Theory of Types, Amer. J. Math. 30 (1908), no. 3, 222–262. MR 1506041, DOI 10.2307/2369948
Michael Shulman, Minicourse on homotopy type theory, slides from a talk, available at http://home.sandiego.edu/~shulman/hottminicourse2012/, 2012.
Michael Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, 2015, preprint available at http://arxiv.org/abs/1509.07584.
Michael Shulman, Homotopy type theory: the logic of space, 2017, preprint available at http://arxiv.org/abs/1703.03007.
The Coq Development Team, The Coq proof assistant, Available at https://coq.inria.fr/.
Coquand Thierry, Simon Huber, and Anders Mörtberg, On higher inductive types in cubical type theory, 2018, preprint available at http://arxiv.org/abs/1802.01170.
D. Tsementzis, A meaning explanation for HoTT, (2016), Available at http://philsci-archive.pitt.edu/12824/.
Dimitris Tsementzis, Univalent foundations as structuralist foundations, Synthese 194 (2017), no. 9, 3583–3617. MR 3704905, DOI 10.1007/s11229-016-1109-x
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.
D. Tsementzis and H. Halvorson, Foundations and philosophy, Philosopher’s Imprint (forthcoming) (2017), Available at http://philsci-archive.pitt.edu/13504/.
The Univalent Foundations Program, Homotopy type theory—univalent foundations of mathematics, The Univalent Foundations Program, Princeton, NJ; Institute for Advanced Study (IAS), Princeton, NJ, 2013. MR 3204653
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.
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.
Vladimir Voevodsky, B-systems, 2014, preprint available at http://arxiv.org/abs/1410.5389.
Vladimir Voevodsky, C-system of a module over a monad on sets, 2014, preprint available at http://arxiv.org/abs/1407.3394.
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.
Vladimir Voevodsky, A C-system defined by a universe category, Theory Appl. Categ. 30 (2015), Paper No. 37, 1181–1215. MR 3402489
Vladimir Voevodsky, An experimental library of formalized mathematics based on the univalent foundations, Math. Structures Comput. Sci. 25 (2015), no. 5, 1278–1294. MR 3340542, DOI 10.1017/S0960129514000577
Vladimir Voevodsky, Martin-Löf identity types in the C-systems defined by a universe category, 2015, preprint available at http://arxiv.org/abs/1505.06446, pp. 1–51.
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.
Vladimir Voevodsky, Lawvere theories and Jf-relative monads, (2016), 1–21, preprint available at http://arxiv.org/abs/1601.02158.
Vladimir Voevodsky, Products of families of types and $(\Pi ,\lambda )$-structures on C-systems, Theory Appl. Categ. 31 (2016), Paper No. 36, 1044–1094. MR 3584698
Vladimir Voevodsky, Subsystems and regular quotients of C-systems, A panorama of mathematics: pure and applied, Contemp. Math., vol. 658, Amer. Math. Soc., Providence, RI, 2016, pp. 127–137. MR 3475277, DOI 10.1090/conm/658/13124
Vladimir Voevodsky, C-systems defined by universe categories: presheaves, Theory Appl. Categ. 32 (2017), Paper No. 3, 53–112. MR 3607209, DOI 10.1007/s11766-017-3338-2
Vladimir Voevodsky, The $(\Pi , \lambda )$-structures on the C-systems defined by universe categories, Theory Appl. Categ. 32 (2017), Paper No. 4, 113–121. MR 3607210
Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al., UniMath—a computer-checked library of univalent mathematics, available at http://UniMath.org.