update
This commit is contained in:
parent
ab8ba9f8bf
commit
9ea3e91e17
|
@ -12,6 +12,9 @@
|
||||||
- [Chapter 4](./generated/HottBook.Chapter4.md)
|
- [Chapter 4](./generated/HottBook.Chapter4.md)
|
||||||
- [Chapter 5](./generated/HottBook.Chapter5.md)
|
- [Chapter 5](./generated/HottBook.Chapter5.md)
|
||||||
- [Chapter 6](./generated/HottBook.Chapter6.md)
|
- [Chapter 6](./generated/HottBook.Chapter6.md)
|
||||||
|
- [Chapter 7](./generated/HottBook.Chapter7.md)
|
||||||
|
- [Chapter 8](./generated/HottBook.Chapter8.md)
|
||||||
|
- [Chapter 9](./generated/HottBook.Chapter9.md)
|
||||||
|
|
||||||
# Individual lemmas
|
# Individual lemmas
|
||||||
|
|
||||||
|
|
|
@ -4,7 +4,7 @@ This book tracks my current research goals and progress.
|
||||||
|
|
||||||
- [Source](https://git.mzhang.io/school/type-theory)
|
- [Source](https://git.mzhang.io/school/type-theory)
|
||||||
|
|
||||||
```dot process
|
<!-- ```dot process
|
||||||
digraph {
|
digraph {
|
||||||
rankdir="BT"
|
rankdir="BT"
|
||||||
|
|
||||||
|
@ -21,4 +21,4 @@ digraph {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
```
|
``` -->
|
BIN
resources/HoTT.pdf
vendored
Normal file
BIN
resources/HoTT.pdf
vendored
Normal file
Binary file not shown.
BIN
resources/MayConcise/exercises.pdf
vendored
Normal file
BIN
resources/MayConcise/exercises.pdf
vendored
Normal file
Binary file not shown.
5
resources/MayConcise/exercises.typ
vendored
Normal file
5
resources/MayConcise/exercises.typ
vendored
Normal file
|
@ -0,0 +1,5 @@
|
||||||
|
= Chapter 1
|
||||||
|
|
||||||
|
1. #[
|
||||||
|
|
||||||
|
]
|
16
src/HottBook/Chapter7.lagda.md
Normal file
16
src/HottBook/Chapter7.lagda.md
Normal file
|
@ -0,0 +1,16 @@
|
||||||
|
```
|
||||||
|
module HottBook.Chapter7 where
|
||||||
|
|
||||||
|
open import Agda.Primitive
|
||||||
|
open import HottBook.Chapter1
|
||||||
|
open import HottBook.Chapter2
|
||||||
|
open import HottBook.Chapter6
|
||||||
|
```
|
||||||
|
|
||||||
|
## 7.1 Definition of $n$-types
|
||||||
|
|
||||||
|
### Definition 7.1.1
|
||||||
|
|
||||||
|
```
|
||||||
|
is-_-type : ℕ → Set → Set
|
||||||
|
```
|
|
@ -25,4 +25,8 @@ data ℤ : Set where
|
||||||
```
|
```
|
||||||
-- code : {l : Level} → S¹ → Set (lsuc l)
|
-- code : {l : Level} → S¹ → Set (lsuc l)
|
||||||
-- code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)
|
-- code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)
|
||||||
```
|
```
|
||||||
|
|
||||||
|
## 8.7 The van Kampen theorem
|
||||||
|
|
||||||
|
### 8.7.1 Naive van Kampen
|
||||||
|
|
Loading…
Reference in a new issue