Homotopy type theory and Voevodsky’s univalent foundations

Pelayo, Álvaro; Warren, Michael

doi:10.1090/S0273-0979-2014-01456-9

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