Chapter 2: Homotopy type theory

michael commented

2023-05-16 14:05:07 +00:00

Owner

Definitions, Lemmas, and Theorems

Lemma 2.1.1
Lemma 2.1.2
Lemma 2.1.4
Theorem 2.1.6 (Eckmann-Hilton)
Definition 2.1.7 (pointed type)
Definition 2.1.8 (loop space)
Lemma 2.2.1
Lemma 2.2.2
Lemma 2.3.1 (transport)
Lemma 2.3.2 (path lifting property)
Lemma 2.3.4 (dependent map)
Lemma 2.3.5
Equation 2.3.6
Equation 2.3.7
Lemma 2.3.8
Lemma 2.3.9
Lemma 2.3.10
Lemma 2.3.11
Definition 2.4.1 (homotopy)
Lemma 2.4.2
Lemma 2.4.3
Corollary 2.4.4
Definition 2.4.6 (quasi-inverse)
Example 2.4.7
Example 2.4.8
Example 2.4.9
Definition 2.4.10 (is-equiv)
Definition 2.4.11 (equivalence)
Lemma 2.4.12
Equation 2.5.1
Definition 2.6.1
Theorem 2.6.2
Theorem 2.6.4
Theorem 2.6.5
Theorem 2.7.2
Corollary 2.7.3
Theorem 2.7.4
Theorem 2.8.1
Definition 2.9.1
Definition 2.9.2 (happly)
Axiom 2.9.3 (function extensionality)
Equation 2.9.4
Equation 2.9.5
Lemma 2.9.6
Lemma 2.9.7
Lemma 2.10.1
Definition 2.10.2 (idtoeqv)
Axiom 2.10.3 (univalence)
Lemma 2.10.5
Theorem 2.11.1
Lemma 2.11.2
Theorem 2.11.3
Theorem 2.11.4
Theorem 2.11.5
Theorem 2.12.5
Remark 2.12.6
Theorem 2.13.1 (#13)
Definition 2.14.1 (semigroup structure)
Definition 2.15.1
Theorem 2.15.2
Definition 2.15.4
Theorem 2.15.5
Definition 2.15.6
Theorem 2.15.7

Exercises

Exercise 2.1
Exercise 2.2
Exercise 2.3
Exercise 2.4 (#6)
Exercise 2.5
Exercise 2.6
Exercise 2.7
Exercise 2.8
Exercise 2.9
Exercise 2.10
Exercise 2.11
Exercise 2.12
Exercise 2.13 (#8)
Exercise 2.14
Exercise 2.15
Exercise 2.16
Exercise 2.17
Exercise 2.18

## [Definitions, Lemmas, and Theorems](https://git.mzhang.io/school/type-theory/src/branch/master/src/HottBook/Chapter2.lagda.md) - [x] Lemma 2.1.1 - [x] Lemma 2.1.2 - [x] Lemma 2.1.4 - [ ] Theorem 2.1.6 (Eckmann-Hilton) - [x] Definition 2.1.7 (pointed type) - [x] Definition 2.1.8 (loop space) - [x] Lemma 2.2.1 - [x] Lemma 2.2.2 - [x] Lemma 2.3.1 (transport) - [x] Lemma 2.3.2 (path lifting property) - [x] Lemma 2.3.4 (dependent map) - [x] Lemma 2.3.5 - [x] Equation 2.3.6 - [x] Equation 2.3.7 - [x] Lemma 2.3.8 - [x] Lemma 2.3.9 - [x] Lemma 2.3.10 - [x] Lemma 2.3.11 - [x] Definition 2.4.1 (homotopy) - [x] Lemma 2.4.2 - [x] Lemma 2.4.3 - [ ] Corollary 2.4.4 - [x] Definition 2.4.6 (quasi-inverse) - [x] Example 2.4.7 - [x] Example 2.4.8 - [x] Example 2.4.9 - [x] Definition 2.4.10 (is-equiv) - [x] Definition 2.4.11 (equivalence) - [x] Lemma 2.4.12 - [x] Equation 2.5.1 - [x] Definition 2.6.1 - [x] Theorem 2.6.2 - [x] Theorem 2.6.4 - [x] Theorem 2.6.5 - [x] Theorem 2.7.2 - [x] Corollary 2.7.3 - [ ] Theorem 2.7.4 - [x] Theorem 2.8.1 - [x] Definition 2.9.1 - [x] Definition 2.9.2 (happly) - [x] Axiom 2.9.3 (function extensionality) - [x] Equation 2.9.4 - [x] Equation 2.9.5 - [ ] Lemma 2.9.6 - [ ] Lemma 2.9.7 - [x] Lemma 2.10.1 - [x] Definition 2.10.2 (idtoeqv) - [x] Axiom 2.10.3 (univalence) - [ ] Lemma 2.10.5 - [ ] Theorem 2.11.1 - [x] Lemma 2.11.2 - [x] Theorem 2.11.3 - [x] Theorem 2.11.4 - [ ] Theorem 2.11.5 - [x] Theorem 2.12.5 - [x] Remark 2.12.6 - [x] Theorem 2.13.1 (#13) - [x] Definition 2.14.1 (semigroup structure) - [x] Definition 2.15.1 - [x] Theorem 2.15.2 - [x] Definition 2.15.4 - [x] Theorem 2.15.5 - [x] Definition 2.15.6 - [x] Theorem 2.15.7 ## [Exercises](https://git.mzhang.io/school/type-theory/src/branch/master/src/HottBook/Chapter2Exercises.lagda.md) - [x] Exercise 2.1 - [ ] Exercise 2.2 - [ ] Exercise 2.3 - [ ] Exercise 2.4 (#6) - [x] Exercise 2.5 - [x] Exercise 2.6 - [ ] Exercise 2.7 - [ ] Exercise 2.8 - [x] Exercise 2.9 - [x] Exercise 2.10 - [ ] Exercise 2.11 - [ ] Exercise 2.12 - [x] Exercise 2.13 (#8) - [ ] Exercise 2.14 - [ ] Exercise 2.15 - [ ] Exercise 2.16 - [ ] Exercise 2.17 - [x] Exercise 2.18