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

2.1
2.2
2.3
2.4 (#6)
2.5
2.6
2.7
2.8
2.9
2.10
2.11
2.12
2.13 (#8)
2.14
2.15
2.16
2.17
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 - [ ] 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 - [ ] 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) - [ ] Definition 2.14.1 (semigroup structure) - [x] Definition 2.15.1 - [x] Theorem 2.15.2 - [x] Definition 2.15.4 - [ ] Theorem 2.15.5 - [ ] Definition 2.15.6 - [ ] Theorem 2.15.7 ## [Exercises](https://git.mzhang.io/school/type-theory/src/branch/master/src/HottBook/Chapter2Exercises.lagda.md) - [x] 2.1 - [ ] 2.2 - [ ] 2.3 - [ ] 2.4 (#6) - [ ] 2.5 - [x] 2.6 - [ ] 2.7 - [ ] 2.8 - [x] 2.9 - [ ] 2.10 - [ ] 2.11 - [ ] 2.12 - [x] 2.13 (#8) - [ ] 2.14 - [ ] 2.15 - [ ] 2.16 - [ ] 2.17 - [ ] 2.18

michael added a new dependency 2023-05-16 14:05:24 +00:00

#6 Exercise 2.4: n-dimensional path

michael added this to the (deleted) project 2023-05-16 14:05:39 +00:00

michael added a new dependency 2023-05-17 09:53:39 +00:00

#8 Exercise 2.13: (2 ≃ 2) ≃ 2

michael changed title from ~~Chapter 2~~ to Chapter 2: Homotopy type theory

2023-05-18 05:40:59 +00:00

michael added the due date 2024-06-01

2024-05-16 14:29:24 +00:00

michael started working 2024-05-16 14:30:42 +00:00

michael stopped working 2024-05-17 06:02:10 +00:00

15 hours 31 minutes

michael started working 2024-05-17 08:11:32 +00:00

michael stopped working 2024-05-18 00:36:20 +00:00

16 hours 24 minutes

michael started working 2024-05-18 06:09:50 +00:00

michael stopped working 2024-05-18 07:06:08 +00:00

56 minutes 18 seconds

michael modified the project from (deleted) to thesis

2024-05-24 01:34:36 +00:00

Chapter 2: Homotopy type theory #7

Definitions, Lemmas, and Theorems

Exercises