From the Introduction:
Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids.
Homotopy type theory brings new ideas into the very foundation of mathematics. On the one hand, there is Voevodsky’s subtle and beautiful univalence axiom. The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on work- days, despite its incompatibility with the “official” doctrines of conventional foundations. On the other hand, we have higher inductive types, which provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory: spheres, cylinders, truncations, localizations, etc. Both ideas are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of “logic of homotopy types”.
This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics — and convenient machine implementations, which can serve as a practical aid to the working mathematician. This is the Univalent Foundations program.
The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning — but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant. We believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.
Author(s): The Univalent Foundations Program
Edition: first-edition-0-ge0aa8e9
Year: 2013
Language: English
Pages: 599
Preface......Page 4
Table of Contents......Page 8
Introduction......Page 14
I Foundations......Page 33
1.1 Type theory versus set theory......Page 36
1.2 Function types......Page 41
1.3 Universes and families......Page 45
1.4 Dependent function types (Π-types)......Page 46
1.5 Product types......Page 47
1.6 Dependent pair types (Σ-types)......Page 52
1.7 Coproduct types......Page 56
1.8 The type of booleans......Page 58
1.9 The natural numbers......Page 60
1.10 Pattern matching and recursion......Page 63
1.11 Propositions as types......Page 65
1.12 Identity types......Page 73
1.12.1 Path induction......Page 75
1.12.2 Equivalence of path induction and based path induction......Page 78
Notes......Page 81
Exercises......Page 84
2 Homotopy type theory......Page 86
2.1 Types are higher groupoids......Page 90
2.2 Functions are functors......Page 99
2.3 Type families are fibrations......Page 100
2.4 Homotopies and equivalences......Page 104
2.5 The higher groupoid structure of type formers......Page 109
2.6 Cartesian product types......Page 110
2.7 Σ-types......Page 113
2.8 The unit type......Page 116
2.9 Π-types and the function extensionality axiom......Page 117
2.10 Universes and the univalence axiom......Page 120
2.11 Identity type......Page 122
2.12 Coproducts......Page 124
2.13 Natural numbers......Page 127
2.14.1 Lifting equivalences......Page 130
2.14.2 Equality of semigroups......Page 132
2.15 Universal properties......Page 133
Notes......Page 136
Exercises......Page 138
3.1 Sets and n-types......Page 142
3.2 Propositions as types?......Page 145
3.3 Mere propositions......Page 147
3.4 Classical vs. intuitionistic logic......Page 150
3.5 Subsets and propositional resizing......Page 152
3.6 The logic of mere propositions......Page 154
3.7 Propositional truncation......Page 155
3.8 The axiom of choice......Page 157
3.9 The principle of unique choice......Page 160
3.10 When are propositions truncated?......Page 161
3.11 Contractibility......Page 164
Notes......Page 167
Exercises......Page 168
4 Equivalences......Page 172
4.1 Quasi-inverses......Page 173
4.2 Half adjoint equivalences......Page 175
4.4 Contractible fibers......Page 181
4.5 On the definition of equivalences......Page 183
4.6 Surjections and embeddings......Page 184
4.7 Closure properties of equivalences......Page 185
4.8 The object classifier......Page 188
4.9 Univalence implies function extensionality......Page 190
Notes......Page 193
Exercises......Page 194
5.1 Introduction to inductive types......Page 196
5.2 Uniqueness of inductive types......Page 199
5.3 W-types......Page 203
5.4 Inductive types are initial algebras......Page 206
5.5 Homotopy-inductive types......Page 210
5.6 The general syntax of inductive definitions......Page 215
5.7 Generalizations of inductive types......Page 220
5.8 Identity types and identity systems......Page 223
Exercises......Page 229
6.1 Introduction......Page 232
6.2 Induction principles and dependent paths......Page 234
6.3 The interval......Page 240
6.4 Circles and spheres......Page 241
6.5 Suspensions......Page 244
6.6 Cell complexes......Page 249
6.7 Hubs and spokes......Page 251
6.8 Pushouts......Page 252
6.9 Truncations......Page 257
6.10 Quotients......Page 260
6.11 Algebra......Page 265
6.12 The flattening lemma......Page 272
6.13 The general syntax of higher inductive definitions......Page 278
Notes......Page 281
Exercises......Page 282
7.1 Definition of n-types......Page 284
7.2 Uniqueness of identity proofs and Hedberg's theorem......Page 289
7.3 Truncations......Page 293
7.4 Colimits of n-types......Page 300
7.5 Connectedness......Page 305
7.6 Orthogonal factorization......Page 311
7.7 Modalities......Page 317
Notes......Page 322
Exercises......Page 323
II Mathematics......Page 326
8 Homotopy theory......Page 328
8.1.1 Getting started......Page 333
8.1.2 The classical proof......Page 334
8.1.3 The universal cover in type theory......Page 335
8.1.4 The encode-decode proof......Page 337
8.1.5 The homotopy-theoretic proof......Page 340
8.1.6 The universal cover as an identity system......Page 342
8.2 Connectedness of suspensions......Page 343
8.3 π_(k≤n) of an n-connected space and π_(k8.4 Fiber sequences and the long exact sequence......Page 346
8.5 The Hopf fibration......Page 352
8.5.1 Fibrations over pushouts......Page 353
8.5.2 The Hopf construction......Page 355
8.5.3 The Hopf fibration......Page 356
8.6 The Freudenthal suspension theorem......Page 359
8.7 The van Kampen theorem......Page 367
8.7.1 Naive van Kampen......Page 368
8.7.2 The van Kampen theorem with a set of basepoints......Page 374
8.8 Whitehead's theorem and Whitehead's principle......Page 378
8.9 A general statement of the encode-decode method......Page 383
8.10 Additional Results......Page 385
Notes......Page 386
Exercises......Page 388
9 Category theory......Page 390
9.1 Categories and precategories......Page 391
9.2 Functors and transformations......Page 395
9.3 Adjunctions......Page 400
9.4 Equivalences......Page 401
9.5 The Yoneda lemma......Page 408
9.6 Strict categories......Page 412
9.7 †-categories......Page 413
9.8 The structure identity principle......Page 414
9.9 The Rezk completion......Page 418
Notes......Page 427
Exercises......Page 428
10 Set theory......Page 432
10.1.2 Images......Page 433
10.1.3 Quotients......Page 438
10.1.4 Set is a ΠW-pretopos......Page 440
10.1.5 The axiom of choice implies excluded middle......Page 442
10.2 Cardinal numbers......Page 444
10.3 Ordinal numbers......Page 447
10.4 Classical well-orderings......Page 455
10.5 The cumulative hierarchy......Page 459
Notes......Page 466
Exercises......Page 467
11 Real numbers......Page 470
11.1 The field of rational numbers......Page 471
11.2 Dedekind reals......Page 472
11.2.1 The algebraic structure of Dedekind reals......Page 474
11.2.2 Dedekind reals are Cauchy complete......Page 477
11.2.3 Dedekind reals are Dedekind complete......Page 479
11.3 Cauchy reals......Page 480
11.3.1 Construction of Cauchy reals......Page 482
11.3.2 Induction and recursion on Cauchy reals......Page 484
11.3.3 The algebraic structure of Cauchy reals......Page 499
11.3.4 Cauchy reals are Cauchy complete......Page 504
11.4 Comparison of Cauchy and Dedekind reals......Page 505
11.5 Compactness of the interval......Page 507
11.6 The surreal numbers......Page 515
Notes......Page 529
Exercises......Page 531
Appendix......Page 534
A Formal type theory......Page 536
A.1 The first presentation......Page 538
A.1.2 Dependent function types (Π-types)......Page 540
A.1.3 Dependent pair types (Σ-types)......Page 541
A.1.6 Natural numbers......Page 542
A.2 The second presentation......Page 543
A.2.1 Contexts......Page 544
A.2.2 Structural rules......Page 545
A.2.4 Dependent function types (Π-types)......Page 546
A.2.5 Dependent pair types (Σ-types)......Page 547
A.2.6 Coproduct types......Page 548
A.2.8 The unit type 1......Page 549
A.2.10 Identity types......Page 550
A.3 Homotopy type theory......Page 551
A.3.2 The circle......Page 552
A.4 Basic metatheory......Page 553
Notes......Page 555
Bibliography......Page 557
Index of symbols......Page 570
Index......Page 578
