Remote Access Bulletin of the American Mathematical Society

Bulletin of the American Mathematical Society

ISSN 1088-9485(online) ISSN 0273-0979(print)

 
 

 

Homotopy type theory and Voevodsky's univalent foundations


Authors: Álvaro Pelayo and Michael A. Warren
Journal: Bull. Amer. Math. Soc. 51 (2014), 597-648
MSC (2010): Primary 03-02; Secondary 68N18, 55P99
DOI: https://doi.org/10.1090/S0273-0979-2014-01456-9
Published electronically: May 9, 2014
MathSciNet review: 3237761
Full-text PDF Free Access

Abstract | References | Similar Articles | Additional Information

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 [*]) make use of code; however, all notions are introduced from the beginning and in a self-contained fashion.


References [Enhancements On Off] (What's this?)

  • [1] Assorted authors, Univalent foundations of mathematics wiki, 2013, https://uf-ias-2012.wikispaces.com.
  • [2] Steve Awodey, Type theory and homotopy, Epistemology versus ontology, Log. Epistemol. Unity Sci., vol. 27, Springer, Dordrecht, 2012, pp. 183-201. MR 2962717, https://doi.org/10.1007/978-94-007-4435-6_9
  • [3] Steve Awodey, Pieter Hofstra, and Michael A. Warren, Martin-Löf complexes, Ann. Pure Appl. Logic 164 (2013), no. 10, 928-956. MR 3069018, https://doi.org/10.1016/j.apal.2013.05.001
  • [4] 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, https://doi.org/10.1090/noti1043
  • [5] 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 (2010g:03020), https://doi.org/10.1017/S0305004108001783
  • [6] 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 (99f:18010), https://doi.org/10.1006/aima.1998.1724
  • [7] Hans Joachim Baues, Homotopy types, Handbook of algebraic topology, North-Holland, Amsterdam, 1995, pp. 1-72. MR 1361886 (97e:55005), https://doi.org/10.1016/B978-044481779-2/50002-X
  • [8] 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 (2011m:18010), https://doi.org/10.1112/plms/pdq026
  • [9] 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 (2007i:68001)
  • [10] 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
  • [11] N. G. de Bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions. 1970 Symposium on Automatic Demonstration (Versailles, 1968) pp. 29-61. Lecture Notes in Mathematics, Vol. 125. Springer, Berlin, 1970. MR 0267814 (42 #2716)
  • [12] Eugenia Cheng, An $ \omega $-category with all duals is an $ \omega $-groupoid, Appl. Categ. Structures 15 (2007), no. 4, 439-453. MR 2350215 (2008g:18001), https://doi.org/10.1007/s10485-007-9081-8
  • [13] A. Chlipala, Certified programming with dependent types, to appear. MIT Press. Currently available online at http://adam.chlipala.net/cpdt/, 2012.
  • [14] Alonzo Church, A set of postulates for the foundation of logic, Ann. of Math. (2) 34 (1933), no. 4, 839-864. MR 1503136, https://doi.org/10.2307/1968702
  • [15] Alonzo Church, A formulation of the simple theory of types, J. Symbolic Logic 5 (1940), 56-68. MR 0001931 (1,321d)
  • [16] Alonzo Church, The Calculi of Lambda-Conversion, Annals of Mathematics Studies, no. 6, Princeton University Press, Princeton, N. J., 1941. MR 0005274 (3,129b)
  • [17] 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 (2008g:55032), https://doi.org/10.1090/conm/431/08272
  • [18] C. Coquand and T. Coquand, Structured type theory, Proceedings of the Workshop on Logical Frameworks and Meta-Languages (LFM'99) (Paris), 1999.
  • [19] Thierry Coquand and Gérard Huet, The calculus of constructions, Inform. and Comput. 76 (1988), no. 2-3, 95-120. MR 935892 (89j:68096), https://doi.org/10.1016/0890-5401(88)90005-3
  • [20] H. B. Curry, Functionality in combinatory logic, Proceedings of the National Academy of Sciences 20 (1934), no. 11, 584-590.
  • [21] Jean Dieudonné, A history of algebraic and differential topology 1900-1960, Modern Birkhäuser Classics, Birkhäuser Boston, Inc., Boston, MA, 2009. Reprint of the 1989 edition [MR0995842]. MR 2509981
  • [22] B. Eckmann and P. J. Hilton, Group-like structures in general categories. I. Multiplications and comultiplications, Math. Ann. 145 (1961/1962), 227-255. MR 0136642 (25 #108)
  • [23] 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.
  • [24] Nicola Gambino and Richard Garner, The identity type weak factorisation system, Theoret. Comput. Sci. 409 (2008), no. 1, 94-109. MR 2469279 (2011d:03011), https://doi.org/10.1016/j.tcs.2008.08.030
  • [25] R. Gordon, A. J. Power, and Ross Street, Coherence for tricategories, Mem. Amer. Math. Soc. 117 (1995), no. 558, vi+81. MR 1261589 (96j:18002), https://doi.org/10.1090/memo/0558
  • [26] A. Grothendieck, Pursuing Stacks, 1983.
  • [27] Thomas C. Hales, Formal proof, Notices Amer. Math. Soc. 55 (2008), no. 11, 1370-1380. MR 2463990 (2010h:03012)
  • [28] 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, https://doi.org/10.1007/BFb0022273
  • [29] 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
  • [30] Pieter Hofstra and Michael A. Warren, Combinatorial realizability models of type theory, Ann. Pure Appl. Logic 164 (2013), no. 10, 957-988. MR 3069019, https://doi.org/10.1016/j.apal.2013.05.002
  • [31] 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 (82g:03094)
  • [32] The Univalent Foundations Program Institute for Advanced Study 2013, Homotopy type theory: Univalent foundations of mathematics, 2013, http://homotopytypetheory.org/book.
  • [33] A. Joyal, I. Moerdijk, and B. Toën, Advanced Course on Simplicial Methods in Higher Categories, Quaderns 45 (2008), no. 2.
  • [34] Daniel M. Kan, On c. s. s. complexes, Amer. J. Math. 79 (1957), 449-476. MR 0090047 (19,759e)
  • [35] 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 (93c:55006)
  • [36] C. Kapulkin, P. L. Lumsdaine, and V. Voevodsky, Univalence in simplicial sets, in preparation, on the arXiv as arXiv:1203.2553, 2012.
  • [37] U. Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008. MR 2445721 (2009k:03003)
  • [38] A. Kolmogoroff, Zur Deutung der intuitionistischen Logik, Math. Z. 35 (1932), no. 1, 58-65 (German). MR 1545289, https://doi.org/10.1007/BF01186549
  • [39] F. William Lawvere, Adjointness in foundations, Repr. Theory Appl. Categ. 16 (2006), 1-16. Reprinted from Dialectica 23 (1969). MR 2223032 (2007h:18004)
  • [40] Tom Leinster, Higher operads, higher categories, London Mathematical Society Lecture Note Series, vol. 298, Cambridge University Press, Cambridge, 2004. MR 2094071 (2005h:18030)
  • [41] 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.
  • [42] Jean-Louis Loday, Spaces with finitely many nontrivial homotopy groups, J. Pure Appl. Algebra 24 (1982), no. 2, 179-202. MR 651845 (83i:55009), https://doi.org/10.1016/0022-4049(82)90014-7
  • [43] Jean-Louis Loday and Bruno Vallette, Algebraic operads, Grundlehren der Mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 346, Springer, Heidelberg, 2012. MR 2954392
  • [44] Peter Lefanu Lumsdaine, Weak $ \omega $-categories from intensional type theory, Log. Methods Comput. Sci. 6 (2010), no. 3, 3:24, 19. MR 2720193 (2011k:03022), https://doi.org/10.2168/LMCS-6(3:24)2010
  • [45] 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.
  • [46] P. L. Lumsdaine, Model structures from higher inductive types, preprint, 2011.
  • [47] Jacob Lurie, Higher topos theory, Annals of Mathematics Studies, vol. 170, Princeton University Press, Princeton, NJ, 2009. MR 2522659 (2010j:18001)
  • [48] Saunders MacLane, Categories for the working mathematician, Springer-Verlag, New York-Berlin, 1971. Graduate Texts in Mathematics, Vol. 5. MR 0354798 (50 #7275)
  • [49] G. Maltsiniotis, Infini groupoïdes non stricts, d'apreès Grothendieck, preprint, 2007.
  • [50] 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.
  • [51] 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 (85d:03112), https://doi.org/10.1016/S0049-237X(09)70189-2
  • [52] Per Martin-Löf, Intuitionistic type theory, Studies in Proof Theory. Lecture Notes, vol. 1, Bibliopolis, Naples, 1984. Notes by Giovanni Sambin. MR 769301 (86j:03005)
  • [53] Per Martin-Löf, An intuitionistic theory of types, Twenty-five years of constructive type theory (Venice, 1995), 127-172, Oxford Logic Guides, 36, Oxford University Press, New York, 1998. MR 1686864
  • [54] I. Moerdijk, Fiber bundles and univalence, preprint, available at www.pitt.edu/~krk56/fiber_bundles_univalence.pdf, 2012.
  • [55] 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 (94j:55013), https://doi.org/10.1016/0022-4049(93)90094-A
  • [56] Álvaro Pelayo and San Vũ Ngoc, Symplectic theory of completely integrable Hamiltonian systems, Bull. Amer. Math. Soc. (N.S.) 48 (2011), no. 3, 409-455. MR 2801777 (2012i:37097), https://doi.org/10.1090/S0273-0979-2011-01338-6
  • [57] Á. 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.
  • [58] Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002. MR 1887075 (2003h:68015)
  • [59] H. Poincaré, Analysis situs, Journal de l'École Polytechnique (ser 2) 1 (1895), 1-123.
  • [60] Daniel G. Quillen, Homotopical algebra, Lecture Notes in Mathematics, No. 43, Springer-Verlag, Berlin-New York, 1967. MR 0223432 (36 #6480)
  • [61] B. Russell, The Principles of Mathematics, 1 ed., Cambridge University Press, Cambridge, 1903.
  • [62] Dana Scott, Constructive validity, Symposium on Automatic Demonstration (Versailles, 1968) Lecture Notes in Mathematics, Vol. 125, Springer, Berlin, 1970, pp. 237-275. MR 0278905 (43 #4631)
  • [63] R. A. G. Seely, Locally Cartesian closed categories and type theory, Math. Proc. Cambridge Philos. Soc. 95 (1984), no. 1, 33-48. MR 727078 (86b:18008), https://doi.org/10.1017/S0305004100061284
  • [64] Jean-Pierre Serre, Homologie singulière des espaces fibrés. Applications, Ann. of Math. (2) 54 (1951), 425-505 (French). MR 0045386 (13,574g)
  • [65] 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.
  • [66] M. Shulman, Homotopy type theory, VI, blog post available at http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html, 2011.
  • [67] M. Shulman, The univalence axiom for inverse diagrams, preprint, on the arXiv as arXiv:1203.3253, 2012.
  • [68] C. Simpson, Homotopy types of strict 3-groupoids, preprint, on the arXiv as arXiv:math/9810059, 1998.
  • [69] Carlos Simpson, Computer theorem proving in mathematics, Lett. Math. Phys. 69 (2004), 287-315. MR 2104448 (2005f:03020), https://doi.org/10.1007/s11005-004-0607-9
  • [70] Ross Street, Cosmoi of internal categories, Trans. Amer. Math. Soc. 258 (1980), no. 2, 271-318. MR 558176 (82a:18007), https://doi.org/10.2307/1998059
  • [71] T. Streicher, Investigations into intensional type theory, Ph.D. thesis, Habilitation thesis, Ludwig-Maximilians-University Munich, Munich.
  • [72] 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 (41 #1533)
  • [73] 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 (99m:18007), https://doi.org/10.1023/A:1007747915317
  • [74] The Coq Development Team, The coq proof assistant reference manual, 2012, Version 8.4.
  • [75] V. Voevodsky, A very short note on the homotopy $ \lambda $-calculus, Unpublished note, 2006.
  • [76] V. Voevodsky, Notes on type systems, Unpublished notes, 2009.
  • [77] V. Voevodsky, Univalent foundations project, Modified version of an NSF grant application, 2010.
  • [78] V. Voevodsky, Coq library, available at www.math.ias.edu/~vladimir, 2011.
  • [79] 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.
  • [80] M. A. Warren, Homotopy Models of Intensional Type Theory, Ph.D. thesis prospectus, Carnegie Mellon University, 2006.
  • [81] M. A. Warren, Homotopy Theoretic Aspects of Constructive Type Theory, Ph.D. thesis, Carnegie Mellon University, 2008.
  • [82] 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

Similar Articles

Retrieve articles in Bulletin of the American Mathematical Society with MSC (2010): 03-02, 68N18, 55P99

Retrieve articles in all journals with MSC (2010): 03-02, 68N18, 55P99


Additional Information

Álvaro Pelayo
Affiliation: Department of Mathematics, University of California San Diego, 9500 Gilman Drive 0112, La Jolla, California 92093-0112
Email: pelayo.alv@gmail.com

Michael A. Warren
Affiliation: Los Angeles, California
Email: mwarren@alumni.cmu.edu

DOI: https://doi.org/10.1090/S0273-0979-2014-01456-9
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.
Article copyright: © Copyright 2014 American Mathematical Society

American Mathematical Society