Homotopy Type Theory: Univalent Foundations of Mathematics
The Univalent Foundations Program, Institute for Advanced Study
Homotopy Type Theory: Univalent Foundations of Mathematics
Free
Description
Contents
Reviews

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 offers a new “univalent” foundation of
mathematics, in which a central role is played by Voevodsky’s
univalence axiom and higher inductive types. 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.


This is the first (and to date, only) edition of the book. For the benefit of all readers, the available PDF and printed copies are being updated on a rolling basis with minor corrections and clarifications as we receive them. Every copy has a version marker that can be found on the title page and is of the form “first-edition-XX-gYYYYYYY”, where XX is a natural number and YYYYYYY is the git commit hash that uniquely identifies the exact version. Higher values of XX indicate more recent copies. This update was on August 30, 2015 and its version marker is "first-edition-967-g0b0914e". The most recent builds, as well as PDFs with other form factors are available on GitHub. Printed copies may be purchased via the books homepage.

Language
English
ISBN
Unknown
Preface
Table of Contents
Introduction
I Foundations
1 Type theory
1.1 Type theory versus set theory
1.2 Function types
1.3 Universes and families
1.4 Dependent function types (Π-types)
1.5 Product types
1.6 Dependent pair types (Σ-types)
1.7 Coproduct types
1.8 The type of booleans
1.9 The natural numbers
1.10 Pattern matching and recursion
1.11 Propositions as types
1.12 Identity types
1.12.1 Path induction
1.12.2 Equivalence of path induction and based path induction
1.12.3 Disequality
Notes
Exercises
2 Homotopy type theory
2.1 Types are higher groupoids
2.2 Functions are functors
2.3 Type families are fibrations
2.4 Homotopies and equivalences
2.5 The higher groupoid structure of type formers
2.6 Cartesian product types
2.7 Σ-types
2.8 The unit type
2.9 Π-types and the function extensionality axiom
2.10 Universes and the univalence axiom
2.11 Identity type
2.12 Coproducts
2.13 Natural numbers
2.14 Example: equality of structures
2.14.1 Lifting equivalences
2.14.2 Equality of semigroups
2.15 Universal properties
Notes
Exercises
3 Sets and logic
3.1 Sets and n-types
3.2 Propositions as types?
3.3 Mere propositions
3.4 Classical vs. intuitionistic logic
3.5 Subsets and propositional resizing
3.6 The logic of mere propositions
3.7 Propositional truncation
3.8 The axiom of choice
3.9 The principle of unique choice
3.10 When are propositions truncated?
3.11 Contractibility
Notes
Exercises
4 Equivalences
4.1 Quasi-inverses
4.2 Half adjoint equivalences
4.3 Bi-invertible maps
4.4 Contractible fibers
4.5 On the definition of equivalences
4.6 Surjections and embeddings
4.7 Closure properties of equivalences
4.8 The object classifier
4.9 Univalence implies function extensionality
Notes
Exercises
5 Induction
5.1 Introduction to inductive types
5.2 Uniqueness of inductive types
5.3 W-types
5.4 Inductive types are initial algebras
5.5 Homotopy-inductive types
5.6 The general syntax of inductive definitions
5.7 Generalizations of inductive types
5.8 Identity types and identity systems
Notes
Exercises
6 Higher inductive types
6.1 Introduction
6.2 Induction principles and dependent paths
6.3 The interval
6.4 Circles and spheres
6.5 Suspensions
6.6 Cell complexes
6.7 Hubs and spokes
6.8 Pushouts
6.9 Truncations
6.10 Quotients
6.11 Algebra
6.12 The flattening lemma
6.13 The general syntax of higher inductive definitions
Notes
Exercises
7 Homotopy n-types
7.1 Definition of n-types
7.2 Uniqueness of identity proofs and Hedberg's theorem
7.3 Truncations
7.4 Colimits of n-types
7.5 Connectedness
7.6 Orthogonal factorization
7.7 Modalities
Notes
Exercises
II Mathematics
8 Homotopy theory
8.1 π₁(S¹)
8.1.1 Getting started
8.1.2 The classical proof
8.1.3 The universal cover in type theory
8.1.4 The encode-decode proof
8.1.5 The homotopy-theoretic proof
8.1.6 The universal cover as an identity system
8.2 Connectedness of suspensions
8.3 π_(k≤n) of an n-connected space and π_(k<n)(Sⁿ)
8.4 Fiber sequences and the long exact sequence
8.5 The Hopf fibration
8.5.1 Fibrations over pushouts
8.5.2 The Hopf construction
8.5.3 The Hopf fibration
8.6 The Freudenthal suspension theorem
8.7 The van Kampen theorem
8.7.1 Naive van Kampen
8.7.2 The van Kampen theorem with a set of basepoints
8.8 Whitehead's theorem and Whitehead's principle
8.9 A general statement of the encode-decode method
8.10 Additional Results
Notes
Exercises
9 Category theory
9.1 Categories and precategories
9.2 Functors and transformations
9.3 Adjunctions
9.4 Equivalences
9.5 The Yoneda lemma
9.6 Strict categories
9.7 †-categories
9.8 The structure identity principle
9.9 The Rezk completion
Notes
Exercises
10 Set theory
10.1 The category of sets
10.1.1 Limits and colimits
10.1.2 Images
10.1.3 Quotients
10.1.4 Set is a ΠW-pretopos
10.1.5 The axiom of choice implies excluded middle
10.2 Cardinal numbers
10.3 Ordinal numbers
10.4 Classical well-orderings
10.5 The cumulative hierarchy
Notes
Exercises
11 Real numbers
11.1 The field of rational numbers
11.2 Dedekind reals
11.2.1 The algebraic structure of Dedekind reals
11.2.2 Dedekind reals are Cauchy complete
11.2.3 Dedekind reals are Dedekind complete
11.3 Cauchy reals
11.3.1 Construction of Cauchy reals
11.3.2 Induction and recursion on Cauchy reals
11.3.3 The algebraic structure of Cauchy reals
11.3.4 Cauchy reals are Cauchy complete
11.4 Comparison of Cauchy and Dedekind reals
11.5 Compactness of the interval
11.6 The surreal numbers
Notes
Exercises
Appendix
A Formal type theory
A.1 The first presentation
A.1.1 Type universes
A.1.2 Dependent function types (Π-types)
A.1.3 Dependent pair types (Σ-types)
A.1.4 Coproduct types
A.1.5 The finite types
A.1.6 Natural numbers
A.1.7 W-types
A.1.8 Identity types
A.2 The second presentation
A.2.1 Contexts
A.2.2 Structural rules
A.2.3 Type universes
A.2.4 Dependent function types (Π-types)
A.2.5 Dependent pair types (Σ-types)
A.2.6 Coproduct types
A.2.7 The empty type 0
A.2.8 The unit type 1
A.2.9 The natural number type
A.2.10 Identity types
A.2.11 Definitions
A.3 Homotopy type theory
A.3.1 Function extensionality and univalence
A.3.2 The circle
A.4 Basic metatheory
Notes
Bibliography
Index of symbols
Index
The book hasn't received reviews yet.