AMS :: Bulletin of the American Mathematical Society

Bulletin of the American Mathematical Society

An introduction to univalent foundations for mathematicians

Author: Daniel R. Grayson

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

MSC (2010): Primary 03B35, 03B15

DOI: https://doi.org/10.1090/bull/1616

Published electronically: March 5, 2018

MathSciNet review: 3854072
Full-text PDF Free Access

Abstract | References | Similar Articles | Additional Information

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 [Enhancements On Off] (What's this?)

[1] Homotopy Type Theory in Agda, an Agda library of formalized proofs, available at https://github.com/HoTT/HoTT-Agda.
[2] Lean theorem prover, a proof assistant together with a library of formalized proofs, available at https://github.com/leanprover/lean.
[3] RedPRL, a proof assistant for Computational Cubical Type Theory together with a library of formalized proofs, available at http://www.redprl.org/.
[4] The HoTT Library, a Coq library of formalized proofs, available at https://github.com/HoTT/HoTT.
[5] 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, https://doi.org/10.1017/S0960129514000486
[6] Mathieu Anel, Georg Biedermann, Eric Finster, and André Joyal, A generalized Blakers-Massey theorem, 2017, preprint available at http://arxiv.org/abs/1703.09050.
[7] 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.
[8] 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] Carlo Angiuli and Robert Harper, Computational higher type theory II: Dependent cubical realizability, 2016, preprint available at http://arxiv.org/abs/1606.09638.
[10] 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.
[11] 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] K. Appel and W. Haken, Every planar map is four colorable. I. Discharging, Illinois J. Math. 21 (1977), no. 3, 429–490. MR 0543792
[13] K. Appel and W. Haken, Every planar map is four colorable. I. Discharging, Illinois J. Math. 21 (1977), no. 3, 429–490. MR 0543792
[14] 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] 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, https://doi.org/10.1017/S0305004108001783
[16] Steven Awodey and Andrej Bauer, Propositions as [types], J. Logic Comput. 14 (2004), no. 4, 447–471. MR 2081047, https://doi.org/10.1093/logcom/14.4.447
[17] 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] A. Beilinson, I. M. Gelfand and his seminar—a presence, Notices Amer. Math. Soc. 63 (2016), no. 3, 295–298. MR 3445168, https://doi.org/10.1090/noti1337
[19] Paul Bernays, A system of axiomatic set theory. Part II, J. Symbolic Logic 6 (1941), 1–17. MR 3382, https://doi.org/10.2307/2267281
[20] 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
[21] 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.
[22] 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).
[23] 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] Evan Cavallo and Robert Harper, Computational higher type theory IV: Inductive types, 2018, preprint available at http://arxiv.org/abs/1801.01568.
[25] 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.
[26] 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.
[27] 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
[28] 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
[29] Georges Gonthier, Formal proof—the four-color theorem, Notices Amer. Math. Soc. 55 (2008), no. 11, 1382–1393. MR 2463991
[30] 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.
[31] 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, https://doi.org/10.1017/fmp.2017.1
[32] 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
[33] 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.
[34] Chris Kapulkin and Peter LeFanu Lumsdaine, The simplicial model of univalent foundations (after Voevodsky), 2012, preprint available at http://arxiv.org/abs/1211.2851.
[35] Chris Kapulkin and Peter LeFanu Lumsdaine, The homotopy theory of type theories, 2016, preprint available at http://arxiv.org/abs/1610.00037.
[36] Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky, Univalence in simplicial sets, 2012, preprint available at http://arxiv.org/abs/1203.2553.
[37] Chris Kapulkin and Karol Szumiło, Internal language of finitely complete $(\infty ,1)$ -categories, 2017, preprint available at http://arxiv.org/abs/1709.09519.
[38] 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
[39] Peter LeFanu Lumsdaine and Mike Shulman, Semantics of higher inductive types, 2017, preprint available at http://arxiv.org/abs/1705.07088.
[40] 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, https://doi.org/10.1007/978-3-662-22108-2_11
[41] Per Martin-Löf, Hauptsatz for the intuitionistic theory of iterated inductive definitions, Proceedings of the Second Scandinavian Logic Symposium (Univ. Oslo, Oslo, 1970) North-Holland, Amsterdam, 1971, pp. 179–216. Studies in Logic and the Foundations of Mathematics, Vol. 63. MR 0387023
[42] Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium ’73 (Bristol, 1973) North-Holland, Amsterdam, 1975, pp. 73–118. Studies in Logic and the Foundations of Mathematics, Vol. 80. MR 0387009
[43] 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, https://doi.org/10.1016/S0049-237X(09)70189-2
[44] David McAllester, Morphoid type theory, a typed platonic foundation for mathematics, preprint available at http://arxiv.org/abs/1407.7274.
[45] Ioseph Peano, Arithmetices principia, Fratres Bocca, 1889.
[46] Charles Rezk, Proof of the Blakers-Massey theorem, available at https://faculty.math.illinois.edu/~rezk/freudenthal-and-blakers-massey.pdf.
[47] Bertrand Russell, Mathematical Logic as Based on the Theory of Types, Amer. J. Math. 30 (1908), no. 3, 222–262. MR 1506041, https://doi.org/10.2307/2369948
[48] Michael Shulman, Minicourse on homotopy type theory, slides from a talk, available at http://home.sandiego.edu/~shulman/hottminicourse2012/, 2012.
[49] Michael Shulman, Brouwer's fixed-point theorem in real-cohesive homotopy type theory, 2015, preprint available at http://arxiv.org/abs/1509.07584.
[50] Michael Shulman, Homotopy type theory: the logic of space, 2017, preprint available at http://arxiv.org/abs/1703.03007.
[51] The Coq Development Team, The Coq proof assistant, Available at https://coq.inria.fr/.
[52] 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.
[53] D. Tsementzis, A meaning explanation for HoTT, (2016), Available at http://philsci-archive.pitt.edu/12824/.
[54] Dimitris Tsementzis, Univalent foundations as structuralist foundations, Synthese 194 (2017), no. 9, 3583–3617. MR 3704905, https://doi.org/10.1007/s11229-016-1109-x
[55] 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] 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—univalent foundations of mathematics, The Univalent Foundations Program, Princeton, NJ; Institute for Advanced Study (IAS), Princeton, NJ, 2013. MR 3204653
[58] 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.
[59] 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] Vladimir Voevodsky, B-systems, 2014, preprint available at http://arxiv.org/abs/1410.5389.
[61] Vladimir Voevodsky, C-system of a module over a monad on sets, 2014, preprint available at http://arxiv.org/abs/1407.3394.
[62] 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] Vladimir Voevodsky, A C-system defined by a universe category, Theory Appl. Categ. 30 (2015), Paper No. 37, 1181–1215. MR 3402489
[64] 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, https://doi.org/10.1017/S0960129514000577
[65] 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.
[66] 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] Vladimir Voevodsky, Lawvere theories and Jf-relative monads, (2016), 1-21, preprint available at http://arxiv.org/abs/1601.02158.
[68] Vladimir Voevodsky, Products of families of types and (Π,𝜆)-structures on C-systems, Theory Appl. Categ. 31 (2016), Paper No. 36, 1044–1094. MR 3584698
[69] 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, https://doi.org/10.1090/conm/658/13124
[70] Vladimir Voevodsky, C-systems defined by universe categories: presheaves, Theory Appl. Categ. 32 (2017), Paper No. 3, 53–112. MR 3607209
[71] Vladimir Voevodsky, The (Π,𝜆)-structures on the C-systems defined by universe categories, Theory Appl. Categ. 32 (2017), Paper No. 4, 113–121. MR 3607210
[72] Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al., UniMath--a computer-checked library of univalent mathematics, available at http://UniMath.org.

Recommend

[1803.02294] A self-contained, brief and complete formulation of Voevodsky's Uni...

Issues · agda/agda · GitHub

Issues · agda/cubical · GitHub

redtt/s1.red at master · RedPRL/redtt · GitHub

[1705.07442] A type theory for synthetic $\infty$-categories

[1611.02108] Cubical Type Theory: a constructive interpretation of the univalenc...

[1802.01170] On Higher Inductive Types in Cubical Type Theory

Writing a Lisp, Part 18: No Define

Writing a Lisp, Part 17: Modules

Writing a Lisp, Part 16: Standard Library

About Joyk