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 research

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

michael added the due date 2024-09-01

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

michael added the

hott-book-chapter

label 2024-10-15 05:09:02 +00:00

Chapter 6: Higher inductive types #15

Definitions, Lemmas, and Theorems

Exercises