Homotopy Type Theory
Homotopy Type Theory
Type theory is important for construct good programming language in Computer Science.
1 Type theory
1.1 Type theory versus set theory
1.2 Function types
1.3 Universes and families
1.4 Dependent function types ($\Pi$-types)
1.5 Product types
1.6 Dependent pair types ($\Sigma$-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. Exercies
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 $\Sigma$-types
2.8 The unit type
2.9 $\Pi$-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 structuers
2.15 Universal properties
2. Exercises
3 Sets and logic
3.1 Sets and $n$-types
3.2 Propositions as types?
3.3 Mere propositions
3.4 Clssical 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 Contracribility
3. 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
4. Exercises
5 Induction
5.1 Introduction to indutive 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
5. Exercises
6 Higher inductive types
6.1 Introduction
6.2 Induction principles and dependent paths
6.3 The interval
6.4 Cricles 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
6. 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
7. Exercises
8 Homotopy theory
8.1 $\pi_1(S^1)$
8.2 Connectedness of suspensions
8.3 $\pi_{k\le n}$ of an $n$-connected space and $\pi_{k<n}(S^n)$
8.4 Fiber sequences and the long exact sequence
8.5 The Hopf fibration
8.6 The Freudenthal suspension theorem
8.7 The van Kampen theorem
8.8 Whitehead's theorem and Whitehead's principle
8.9 A general statesment of the encode-decode method
8.10 Additional Results
8. 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 categroies
9.7 $\dagger$-categories
9.8 The structure identity principle
9.9 The Rezk completion
9. Exercises
10 Set Theory
10.1 The category of sets
10.2 Cardinal numbers
10.3 Ordinal numbers
10.4 Classical well-orderings
10.5 The cumulative hierachy
10. Exercises
11 Real numbers
11.1 The field of rational numbers
11.2 Dedekind reals
11.3 Cauchy reals
11.4 Comparison of Cauchy and Dedekind reals
11.5 Compactness of the interval
11.6 The surreal numbers
11. Exercises
A Formal type theory
A.1 The first presentation
A.2 The second presentation
A.3 Homotopy type theory
A.4 Basic metatheory
Use
This is one part of ULA.
HoTT is general system of classify and check unknown system of language.