diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md
index 3ff1b1a..6216cdb 100644
--- a/html/src/SUMMARY.md
+++ b/html/src/SUMMARY.md
@@ -12,6 +12,9 @@
 - [Chapter 4](./generated/HottBook.Chapter4.md)
 - [Chapter 5](./generated/HottBook.Chapter5.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
 
diff --git a/html/src/front.md b/html/src/front.md
index 24f68fb..885e6bb 100644
--- a/html/src/front.md
+++ b/html/src/front.md
@@ -4,7 +4,7 @@ This book tracks my current research goals and progress.
 
 - [Source](https://git.mzhang.io/school/type-theory)
 
-```dot process
+<!-- ```dot process
 digraph {
   rankdir="BT"
 
@@ -21,4 +21,4 @@ digraph {
     }
   }
 }
-```
\ No newline at end of file
+``` -->
\ No newline at end of file
diff --git a/resources/HoTT.pdf b/resources/HoTT.pdf
new file mode 100644
index 0000000..920fbad
Binary files /dev/null and b/resources/HoTT.pdf differ
diff --git a/resources/MayConcise/exercises.pdf b/resources/MayConcise/exercises.pdf
new file mode 100644
index 0000000..71ac041
Binary files /dev/null and b/resources/MayConcise/exercises.pdf differ
diff --git a/resources/MayConcise/exercises.typ b/resources/MayConcise/exercises.typ
new file mode 100644
index 0000000..c14a750
--- /dev/null
+++ b/resources/MayConcise/exercises.typ
@@ -0,0 +1,5 @@
+= Chapter 1
+
+1. #[
+
+]
\ No newline at end of file
diff --git a/src/HottBook/Chapter7.lagda.md b/src/HottBook/Chapter7.lagda.md
new file mode 100644
index 0000000..ab8b050
--- /dev/null
+++ b/src/HottBook/Chapter7.lagda.md
@@ -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
+```
\ No newline at end of file
diff --git a/src/HottBook/Chapter8.lagda.md b/src/HottBook/Chapter8.lagda.md
index 0e7f22c..3855299 100644
--- a/src/HottBook/Chapter8.lagda.md
+++ b/src/HottBook/Chapter8.lagda.md
@@ -25,4 +25,8 @@ data ℤ : Set where
 ```
 -- code : {l : Level} → S¹ → Set (lsuc l)
 -- code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)
-```
\ No newline at end of file
+```
+
+## 8.7  The van Kampen theorem
+
+### 8.7.1 Naive van Kampen