Homotopy Type Theory: Univalent Foundations of Mathematics
Free
Description
Contents
Reviews
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.