Homotopy type theory and Voevodsky’s univalent foundations
HTML articles powered by AMS MathViewer
- by Álvaro Pelayo and Michael A. Warren PDF
- Bull. Amer. Math. Soc. 51 (2014), 597-648 Request permission
Abstract:
Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has been christened homotopy type theory. In this direction, Vladimir Voevodsky observed that it is possible to model type theory using simplicial sets and that this model satisfies an additional property, called the Univalence Axiom, which has a number of striking consequences. He has subsequently advocated a program, which he calls univalent foundations, of developing mathematics in the setting of type theory with the Univalence Axiom and possibly other additional axioms motivated by the simplicial set model. Because type theory possesses good computational properties, this program can be carried out in a computer proof assistant. In this paper we give an introduction to homotopy type theory in Voevodsky’s setting, paying attention to both theoretical and practical issues. In particular, the paper serves as an introduction to both the general ideas of homotopy type theory as well as to some of the concrete details of Voevodsky’s work using the well-known proof assistant Coq. The paper is written for a general audience of mathematicians with basic knowledge of algebraic topology; the paper does not assume any preliminary knowledge of type theory, logic, or computer science. Because a defining characteristic of Voevodsky’s program is that the Coq code has fundamental mathematical content, and many of the mathematical concepts which are efficiently captured in the code cannot be explained in standard mathematical English without a lengthy detour through type theory, the later sections of this paper (beginning with Section \ref{sec2}) make use of code; however, all notions are introduced from the beginning and in a self-contained fashion.References
- Assorted authors, Univalent foundations of mathematics wiki, 2013, https://uf-ias-2012.wikispaces.com.
- Steve Awodey, Type theory and homotopy, Epistemology versus ontology, Log. Epistemol. Unity Sci., vol. 27, Springer, Dordrecht, 2012, pp. 183–201. MR 2962717, DOI 10.1007/978-94-007-4435-6_{9}
- Steve Awodey, Pieter Hofstra, and Michael A. Warren, Martin-Löf complexes, Ann. Pure Appl. Logic 164 (2013), no. 10, 928–956. MR 3069018, DOI 10.1016/j.apal.2013.05.001
- Steve Awodey, Álvaro Pelayo, and Michael A. Warren, Voevodsky’s univalence axiom in homotopy type theory, Notices Amer. Math. Soc. 60 (2013), no. 9, 1164–1167. MR 3113277, DOI 10.1090/noti1043
- 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
- M. A. Batanin, Monoidal globular categories as a natural environment for the theory of weak $n$-categories, Adv. Math. 136 (1998), no. 1, 39–103. MR 1623672, DOI 10.1006/aima.1998.1724
- Hans Joachim Baues, Homotopy types, Handbook of algebraic topology, North-Holland, Amsterdam, 1995, pp. 1–72. MR 1361886, DOI 10.1016/B978-044481779-2/50002-X
- Benno van den Berg and Richard Garner, Types are weak $\omega$-groupoids, Proc. Lond. Math. Soc. (3) 102 (2011), no. 2, 370–394. MR 2769118, DOI 10.1112/plms/pdq026
- Yves Bertot and Pierre Castéran, Interactive theorem proving and program development, Texts in Theoretical Computer Science. An EATCS Series, Springer-Verlag, Berlin, 2004. Coq’Art: the calculus of inductive constructions; With a foreword by Gérard Huet and Christine Paulin-Mohring. MR 2229784, DOI 10.1007/978-3-662-07964-5
- Ronald Brown, Topology and groupoids, BookSurge, LLC, Charleston, SC, 2006. Third edition of Elements of modern topology [McGraw-Hill, New York, 1968; MR0227979]; With 1 CD-ROM (Windows, Macintosh and UNIX). MR 2273730
- M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberger (eds.), Symposium on Automatic Demonstration (held at Versailles, France, December 1968), Lecture Notes in Mathematics, Vol. 125, Springer-Verlag, Berlin-New York, 1970. MR 0267814
- Eugenia Cheng, An $\omega$-category with all duals is an $\omega$-groupoid, Appl. Categ. Structures 15 (2007), no. 4, 439–453. MR 2350215, DOI 10.1007/s10485-007-9081-8
- A. Chlipala, Certified programming with dependent types, to appear. MIT Press. Currently available online at http://adam.chlipala.net/cpdt/, 2012.
- Alonzo Church, A set of postulates for the foundation of logic, Ann. of Math. (2) 34 (1933), no. 4, 839–864. MR 1503136, DOI 10.2307/1968702
- Alonzo Church, A formulation of the simple theory of types, J. Symbolic Logic 5 (1940), 56–68. MR 1931, DOI 10.2307/2266170
- Alonzo Church, The Calculi of Lambda-Conversion, Annals of Mathematics Studies, No. 6, Princeton University Press, Princeton, N. J., 1941. MR 0005274
- Denis-Charles Cisinski, Batanin higher groupoids and homotopy types, Categories in algebra, geometry and mathematical physics, Contemp. Math., vol. 431, Amer. Math. Soc., Providence, RI, 2007, pp. 171–186. MR 2342828, DOI 10.1090/conm/431/08272
- C. Coquand and T. Coquand, Structured type theory, Proceedings of the Workshop on Logical Frameworks and Meta-Languages (LFM’99) (Paris), 1999.
- Thierry Coquand and Gérard Huet, The calculus of constructions, Inform. and Comput. 76 (1988), no. 2-3, 95–120. MR 935892, DOI 10.1016/0890-5401(88)90005-3
- H. B. Curry, Functionality in combinatory logic, Proceedings of the National Academy of Sciences 20 (1934), no. 11, 584–590.
- Jean Dieudonné, A history of algebraic and differential topology 1900–1960, Modern Birkhäuser Classics, Birkhäuser Boston, Ltd., Boston, MA, 2009. Reprint of the 1989 edition [MR0995842]. MR 2509981, DOI 10.1007/978-0-8176-4907-4
- B. Eckmann and P. J. Hilton, Group-like structures in general categories. I. Multiplications and comultiplications, Math. Ann. 145 (1961/62), 227–255. MR 136642, DOI 10.1007/BF01451367
- N. Gambino, The Univalence Axiom and Function Extensionality, Oberwolfach Reports 8 (2011), no. 1, p. 625, Abstracts from the mini-workshop held February 27–March 5, 2011, organized by Steve Awodey, Richard Garner, Per Martin-Löf and Vladimir Voevodsky.
- Nicola Gambino and Richard Garner, The identity type weak factorisation system, Theoret. Comput. Sci. 409 (2008), no. 1, 94–109. MR 2469279, DOI 10.1016/j.tcs.2008.08.030
- R. Gordon, A. J. Power, and Ross Street, Coherence for tricategories, Mem. Amer. Math. Soc. 117 (1995), no. 558, vi+81. MR 1261589, DOI 10.1090/memo/0558
- A. Grothendieck, Pursuing Stacks, 1983.
- Thomas C. Hales, Formal proof, Notices Amer. Math. Soc. 55 (2008), no. 11, 1370–1380. MR 2463990
- Martin Hofmann, On the interpretation of type theory in locally Cartesian closed categories, Computer science logic (Kazimierz, 1994) Lecture Notes in Comput. Sci., vol. 933, Springer, Berlin, 1995, pp. 427–441. MR 1471244, DOI 10.1007/BFb0022273
- Martin Hofmann and Thomas Streicher, The groupoid interpretation of type theory, Twenty-five years of constructive type theory (Venice, 1995) Oxford Logic Guides, vol. 36, Oxford Univ. Press, New York, 1998, pp. 83–111. MR 1686862
- Pieter Hofstra and Michael A. Warren, Combinatorial realizability models of type theory, Ann. Pure Appl. Logic 164 (2013), no. 10, 957–988. MR 3069019, DOI 10.1016/j.apal.2013.05.002
- W. A. Howard, The formulae-as-types notion of construction, To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, Academic Press, London-New York, 1980, pp. 480–490. MR 592816
- The Univalent Foundations Program Institute for Advanced Study 2013, Homotopy type theory: Univalent foundations of mathematics, 2013, http://homotopytypetheory.org/book.
- A. Joyal, I. Moerdijk, and B. Toën, Advanced Course on Simplicial Methods in Higher Categories, Quaderns 45 (2008), no. 2.
- Daniel M. Kan, On c. s. s. complexes, Amer. J. Math. 79 (1957), 449–476. MR 90047, DOI 10.2307/2372558
- M. M. Kapranov and V. A. Voevodsky, $\infty$-groupoids and homotopy types, Cahiers Topologie Géom. Différentielle Catég. 32 (1991), no. 1, 29–46 (English, with French summary). International Category Theory Meeting (Bangor, 1989 and Cambridge, 1990). MR 1130401
- C. Kapulkin, P. L. Lumsdaine, and V. Voevodsky, Univalence in simplicial sets, in preparation, on the arXiv as arXiv:1203.2553, 2012.
- U. Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008. MR 2445721
- A. Kolmogoroff, Zur Deutung der intuitionistischen Logik, Math. Z. 35 (1932), no. 1, 58–65 (German). MR 1545289, DOI 10.1007/BF01186549
- F. William Lawvere, Adjointness in foundations, Repr. Theory Appl. Categ. 16 (2006), 1–16. Reprinted from Dialectica 23 (1969). MR 2223032
- Tom Leinster, Higher operads, higher categories, London Mathematical Society Lecture Note Series, vol. 298, Cambridge University Press, Cambridge, 2004. MR 2094071, DOI 10.1017/CBO9780511525896
- D. Licata, A formal proof that the higher fundamental groups are abelian, blog post available at http://homotopytypetheory.org/2011/03/26/higher-fundamental-groups-are- abelian/, 2011.
- Jean-Louis Loday, Spaces with finitely many nontrivial homotopy groups, J. Pure Appl. Algebra 24 (1982), no. 2, 179–202. MR 651845, DOI 10.1016/0022-4049(82)90014-7
- Jean-Louis Loday and Bruno Vallette, Algebraic operads, Grundlehren der mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 346, Springer, Heidelberg, 2012. MR 2954392, DOI 10.1007/978-3-642-30362-3
- Peter Lefanu Lumsdaine, Weak $\omega$-categories from intensional type theory, Log. Methods Comput. Sci. 6 (2010), no. 3, 3:24, 19. MR 2720193, DOI 10.2168/LMCS-6(3:24)2010
- P. L. Lumsdaine, Higher inductive types: a tour of the menagerie, blog post available at http://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the- menagerie/, 2011.
- P. L. Lumsdaine, Model structures from higher inductive types, preprint, 2011.
- Jacob Lurie, Higher topos theory, Annals of Mathematics Studies, vol. 170, Princeton University Press, Princeton, NJ, 2009. MR 2522659, DOI 10.1515/9781400830558
- Saunders MacLane, Categories for the working mathematician, Graduate Texts in Mathematics, Vol. 5, Springer-Verlag, New York-Berlin, 1971. MR 0354798
- G. Maltsiniotis, Infini groupoïdes non stricts, d’apreès Grothendieck, preprint, 2007.
- P. Martin-Löf, An intuitionistic theory of types: predicative part, Proceedings of the Logic Colloquium (Bristol, July, 1973) (H. E. Rose and J. C. Shepherdson, eds.), Studies in Logic and the Foundations of Mathematics, vol. 80, North-Holland, Amsterdam, 1975, pp. 73–118.
- 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
- Per Martin-Löf, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, vol. 1, Bibliopolis, Naples, 1984. Notes by Giovanni Sambin. MR 769301
- Per Martin-Löf, An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice, 1995) Oxford Logic Guides, vol. 36, Oxford Univ. Press, New York, 1998, pp. 127–172. MR 1686864
- I. Moerdijk, Fiber bundles and univalence, preprint, available at www.pitt.edu/~krk56/fiber_bundles_univalence.pdf, 2012.
- Ieke Moerdijk and Jan-Alve Svensson, Algebraic classification of equivariant homotopy $2$-types. I, J. Pure Appl. Algebra 89 (1993), no. 1-2, 187–216. MR 1239560, DOI 10.1016/0022-4049(93)90094-A
- Álvaro Pelayo and San Vũ Ngọc, Symplectic theory of completely integrable Hamiltonian systems, Bull. Amer. Math. Soc. (N.S.) 48 (2011), no. 3, 409–455. MR 2801777, DOI 10.1090/S0273-0979-2011-01338-6
- Á. Pelayo, V. Voevodsky, and M. A. Warren, A univalent formalization of the $p$-adic numbers, to appear in Math. Struct. in Comp. Science, preprint, on the arXiv as arXiv:1302.1207, 2013.
- Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002. MR 1887075
- H. Poincaré, Analysis situs, Journal de l’École Polytechnique (ser 2) 1 (1895), 1–123.
- Daniel G. Quillen, Homotopical algebra, Lecture Notes in Mathematics, No. 43, Springer-Verlag, Berlin-New York, 1967. MR 0223432, DOI 10.1007/BFb0097438
- B. Russell, The Principles of Mathematics, 1 ed., Cambridge University Press, Cambridge, 1903.
- Dana Scott, Constructive validity, Symposium on Automatic Demonstration (Versailles, 1968) Lecture Notes in Mathematics, Vol. 125, Springer, Berlin, 1970, pp. 237–275. MR 0278905
- R. A. G. Seely, Locally Cartesian closed categories and type theory, Math. Proc. Cambridge Philos. Soc. 95 (1984), no. 1, 33–48. MR 727078, DOI 10.1017/S0305004100061284
- Jean-Pierre Serre, Homologie singulière des espaces fibrés. Applications, Ann. of Math. (2) 54 (1951), 425–505 (French). MR 45386, DOI 10.2307/1969485
- M. Shulman, A formal proof that $\pi _{1}(s^{1})=z$, blog post available at http://homotopytypetheory.org/2011/04/29/a-formal-proof-that-pi1s1-is-z/, 2011.
- M. Shulman, Homotopy type theory, VI, blog post available at http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html, 2011.
- M. Shulman, The univalence axiom for inverse diagrams, preprint, on the arXiv as arXiv:1203.3253, 2012.
- C. Simpson, Homotopy types of strict 3-groupoids, preprint, on the arXiv as arXiv:math/9810059, 1998.
- Carlos Simpson, Computer theorem proving in mathematics, Lett. Math. Phys. 69 (2004), 287–315. MR 2104448, DOI 10.1007/s11005-004-0607-9
- Ross Street, Cosmoi of internal categories, Trans. Amer. Math. Soc. 258 (1980), no. 2, 271–318. MR 558176, DOI 10.1090/S0002-9947-1980-0558176-3
- T. Streicher, Investigations into intensional type theory, Ph.D. thesis, Habilitation thesis, Ludwig-Maximilians-University Munich, Munich.
- W. W. Tait, Constructive reasoning, Logic, Methodology and Philos. Sci. III (Proc. Third Internat. Congr., Amsterdam, 1967) North-Holland, Amsterdam, 1968, pp. 185–199. MR 0256877
- Zouhair Tamsamani, Sur des notions de $n$-catégorie et $n$-groupoïde non strictes via des ensembles multi-simpliciaux, $K$-Theory 16 (1999), no. 1, 51–99 (French, with English summary). MR 1673923, DOI 10.1023/A:1007747915317
- The Coq Development Team, The coq proof assistant reference manual, 2012, Version 8.4.
- V. Voevodsky, A very short note on the homotopy $\lambda$-calculus, Unpublished note, 2006.
- V. Voevodsky, Notes on type systems, Unpublished notes, 2009.
- V. Voevodsky, Univalent foundations project, Modified version of an NSF grant application, 2010.
- V. Voevodsky, Coq library, available at www.math.ias.edu/~vladimir, 2011.
- V. Voevodsky, Experimental library of univalent formalization of mathematics, to appear in Math. Struct. Comp. Sci., preprint available on the arXiv as 1401.0053, 2014.
- M. A. Warren, Homotopy Models of Intensional Type Theory, Ph.D. thesis prospectus, Carnegie Mellon University, 2006.
- M. A. Warren, Homotopy Theoretic Aspects of Constructive Type Theory, Ph.D. thesis, Carnegie Mellon University, 2008.
- Michael A. Warren, The strict $\omega$-groupoid interpretation of type theory, Models, logics, and higher-dimensional categories, CRM Proc. Lecture Notes, vol. 53, Amer. Math. Soc., Providence, RI, 2011, pp. 291–340. MR 2867977, DOI 10.1090/crmp/053/16
Additional Information
- Álvaro Pelayo
- Affiliation: Department of Mathematics, University of California San Diego, 9500 Gilman Drive 0112, La Jolla, California 92093-0112
- MR Author ID: 731609
- Email: pelayo.alv@gmail.com
- Michael A. Warren
- Affiliation: Los Angeles, California
- Email: mwarren@alumni.cmu.edu
- Received by editor(s): October 20, 2012
- Published electronically: May 9, 2014
- Additional Notes: The first author was partly supported by NSF CAREER Award DMS-1055897, Spain Ministry of Science Grant MTM 2010-21186-C02-01, and Spain Ministry of Science Sev-2011-0087. He also received support from NSF Grant DMS-0635607 during the preparation of this paper.
The second author received support from the Oswald Veblen Fund and NSF Grant DMS-0635607 during the preparation of this paper. - © Copyright 2014 American Mathematical Society
- Journal: Bull. Amer. Math. Soc. 51 (2014), 597-648
- MSC (2010): Primary 03-02; Secondary 03-B15, 68N18, 55P99
- DOI: https://doi.org/10.1090/S0273-0979-2014-01456-9
- MathSciNet review: 3237761