Chapter 6: Higher inductive types

michael commented

2024-05-20 21:51:14 +00:00

Owner

Definitions, Lemmas, and Theorems

Definition 6.2.2
Lemma 6.2.5
Lemma 6.2.8
Lemma 6.2.9
HIT 6.3 (Interval)
Lemma 6.3.1
Lemma 6.3.2
HIT 6.4 (Circle)
HIT 6.4 (Sphere)
HIT 6.4 (n-Sphere)
Lemma 6.4.1
Lemma 6.4.2
Corollary 6.4.3
Lemma 6.4.4
Lemma 6.4.5
Lemma 6.4.6
HIT 6.5 (Suspension)
Lemma 6.5.1
Definition 6.5.2
Lemma 6.5.3
Lemma 6.5.4
HIT 6.6 (Torus)
HIT 6.8 (Pushout)
Definition 6.8.1
Lemma 6.8.2
HIT 6.9 (Truncation)
Lemma 6.9.1
Lemma 6.9.2
Lemma 6.9.3
HIT 6.10 (Quotient)
Lemma 6.10.3
Definition 6.10.4
Definition 6.10.5
Theorem 6.10.6
Lemma 6.10.8
Corollary 6.10.10
Lemma 6.10.12
Corollary 6.10.13
Definition 6.11.1 (monoid)
Lemma 6.11.5
Theorem 6.11.6
Theorem 6.11.7
Lemma 6.12.1
Lemma 6.12.2 (flattening)
Lemma 6.12.3
Lemma 6.12.5
Lemma 6.12.7
Lemma 6.12.8
Example 6.13.1

Exercises

Exercise 6.1
Exercise 6.2
Exercise 6.3
Exercise 6.4
Exercise 6.5
Exercise 6.6
Exercise 6.7
Exercise 6.8
Exercise 6.9
Exercise 6.10
Exercise 6.11
Exercise 6.12
Exercise 6.13

## [Definitions, Lemmas, and Theorems](https://git.mzhang.io/school/type-theory/src/branch/master/src/HottBook/Chapter6.lagda.md) - [x] Definition 6.2.2 - [ ] Lemma 6.2.5 - [ ] Lemma 6.2.8 - [ ] Lemma 6.2.9 - [x] HIT 6.3 (Interval) - [x] Lemma 6.3.1 - [x] Lemma 6.3.2 - [x] HIT 6.4 (Circle) - [ ] HIT 6.4 (Sphere) - [ ] HIT 6.4 (n-Sphere) - [x] Lemma 6.4.1 - [x] Lemma 6.4.2 - [ ] Corollary 6.4.3 - [x] Lemma 6.4.4 - [x] Lemma 6.4.5 - [x] Lemma 6.4.6 - [x] HIT 6.5 (Suspension) - [ ] Lemma 6.5.1 - [x] Definition 6.5.2 - [ ] Lemma 6.5.3 - [ ] Lemma 6.5.4 - [ ] HIT 6.6 (Torus) - [ ] HIT 6.8 (Pushout) - [ ] Definition 6.8.1 - [ ] Lemma 6.8.2 - [ ] HIT 6.9 (Truncation) - [ ] Lemma 6.9.1 - [ ] Lemma 6.9.2 - [ ] Lemma 6.9.3 - [ ] HIT 6.10 (Quotient) - [ ] Lemma 6.10.3 - [ ] Definition 6.10.4 - [ ] Definition 6.10.5 - [ ] Theorem 6.10.6 - [ ] Lemma 6.10.8 - [ ] Corollary 6.10.10 - [ ] Lemma 6.10.12 - [ ] Corollary 6.10.13 - [ ] Definition 6.11.1 (monoid) - [ ] Lemma 6.11.5 - [ ] Theorem 6.11.6 - [ ] Theorem 6.11.7 - [ ] Lemma 6.12.1 - [ ] Lemma 6.12.2 (flattening) - [ ] Lemma 6.12.3 - [ ] Lemma 6.12.5 - [ ] Lemma 6.12.7 - [ ] Lemma 6.12.8 - [ ] Example 6.13.1 ## [Exercises](https://git.mzhang.io/school/type-theory/src/branch/master/src/HottBook/Chapter6Exercises.lagda.md) - [ ] Exercise 6.1 - [ ] Exercise 6.2 - [ ] Exercise 6.3 - [ ] Exercise 6.4 - [ ] Exercise 6.5 - [ ] Exercise 6.6 - [ ] Exercise 6.7 - [ ] Exercise 6.8 - [ ] Exercise 6.9 - [ ] Exercise 6.10 - [ ] Exercise 6.11 - [ ] Exercise 6.12 - [ ] Exercise 6.13

michael added this to the (deleted) project 2024-05-20 22:21:39 +00:00

michael modified the project from (deleted) to thesis

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

michael added the due date 2024-09-01

2024-07-25 02:16:31 +00:00

Chapter 6: Higher inductive types #15

Definitions, Lemmas, and Theorems

Exercises