diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md
index 3030a01..d48f08f 100644
--- a/html/src/SUMMARY.md
+++ b/html/src/SUMMARY.md
@@ -8,4 +8,11 @@
 - [Chapter 3](./generated/HottBook.Chapter3.md)
 - [Chapter 4](./generated/HottBook.Chapter4.md)
 - [Chapter 5](./generated/HottBook.Chapter5.md)
-- [Chapter 6](./generated/HottBook.Chapter6.md)
\ No newline at end of file
+- [Chapter 6](./generated/HottBook.Chapter6.md)
+
+# Individual lemmas
+
+- [Lemma 2.2.1](./generated/HottBook.Chapter2Lemma221.md)
+- [Definition 3.3.1](./generated/HottBook.Chapter3Definition331.md)
+- [Lemma 3.3.3](./generated/HottBook.Chapter3Lemma333.md)
+
diff --git a/src/HottBook/Chapter2Lemma221.lagda.md b/src/HottBook/Chapter2Lemma221.lagda.md
index cb59032..5949871 100644
--- a/src/HottBook/Chapter2Lemma221.lagda.md
+++ b/src/HottBook/Chapter2Lemma221.lagda.md
@@ -5,7 +5,9 @@ open import Agda.Primitive
 open import HottBook.Chapter1
 ```
 
-[]: ANCHOR: ap
+## Lemma 2.2.1
+
+[//]: <> (ANCHOR: ap)
 
 ```
 ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
@@ -16,4 +18,4 @@ ap {l1} {l2} {A} {B} {x} {y} f p =
   J (λ x y p → f x ≡ f y) (λ x → refl) x y p
 ```
 
-[]: ANCHOR_END: ap
\ No newline at end of file
+[//]: <> (ANCHOR_END: ap)
\ No newline at end of file
diff --git a/src/HottBook/Chapter3Definition331.lagda.md b/src/HottBook/Chapter3Definition331.lagda.md
index 16d0ce0..c97bd0d 100644
--- a/src/HottBook/Chapter3Definition331.lagda.md
+++ b/src/HottBook/Chapter3Definition331.lagda.md
@@ -5,11 +5,13 @@ open import Agda.Primitive
 open import HottBook.Chapter1
 ```
 
-[]: ANCHOR: isProp
+## Definition 3.3.1
+
+[//]: <> (ANCHOR: isProp)
 
 ```
 isProp : (P : Set) → Set
 isProp P = (x y : P) → x ≡ y
 ```
 
-[]: ANCHOR_END: isProp
\ No newline at end of file
+[//]: <> (ANCHOR_END: isProp)
\ No newline at end of file
diff --git a/src/HottBook/Chapter3Lemma333.lagda.md b/src/HottBook/Chapter3Lemma333.lagda.md
index dda68e9..39fe562 100644
--- a/src/HottBook/Chapter3Lemma333.lagda.md
+++ b/src/HottBook/Chapter3Lemma333.lagda.md
@@ -7,7 +7,9 @@ open import HottBook.Chapter2
 open import HottBook.Chapter3Definition331
 ```
 
-[]: ANCHOR: lemma333
+## Lemma 3.3.3
+
+[//]: <> (ANCHOR: lemma333)
 
 ```
 lemma3∙3∙3 : {P Q : Set}
@@ -25,4 +27,4 @@ lemma3∙3∙3 pp qq f g = f , qinv-to-isequiv (mkQinv g backward forward)
     backward x = qq ((f ∘ g) x) (id x)
 ```
 
-[]: ANCHOR_END: lemma333
\ No newline at end of file
+[//]: <> (ANCHOR_END: lemma333)
\ No newline at end of file