diff --git a/.vscode/settings.json b/.vscode/settings.json
index 5c606e0..b5429d2 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -3,7 +3,7 @@
 	"gitdoc.enabled": false,
 	"gitdoc.autoCommitDelay": 300000,
 	"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
-	"agdaMode.connection.commandLineOptions": "--rewriting --without-K",
+	"agdaMode.connection.commandLineOptions": "--without-K",
 	"search.exclude": {
 		"src/CubicalHott/**": true
 	},
diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index 1447719..27b6456 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -2,6 +2,8 @@
   <summary>Imports</summary>
 
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter1 where
 
 open import Agda.Primitive public
diff --git a/src/HottBook/Chapter1Exercises.lagda.md b/src/HottBook/Chapter1Exercises.lagda.md
index 043515f..4ff865e 100644
--- a/src/HottBook/Chapter1Exercises.lagda.md
+++ b/src/HottBook/Chapter1Exercises.lagda.md
@@ -1,4 +1,6 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter1Exercises where
 
 open import HottBook.Chapter1
diff --git a/src/HottBook/Chapter1Util.agda b/src/HottBook/Chapter1Util.agda
index 9d24998..1983924 100644
--- a/src/HottBook/Chapter1Util.agda
+++ b/src/HottBook/Chapter1Util.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter1Util where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 27aa8c5..8c8fc20 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -2,6 +2,8 @@
   <summary>Imports</summary>
 
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter2 where
 
 open import Agda.Primitive.Cubical hiding (i1)
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 55242e7..e643115 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -1,4 +1,6 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter2Exercises where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Chapter2Lemma221.lagda.md b/src/HottBook/Chapter2Lemma221.lagda.md
index 5949871..ae587e4 100644
--- a/src/HottBook/Chapter2Lemma221.lagda.md
+++ b/src/HottBook/Chapter2Lemma221.lagda.md
@@ -1,4 +1,6 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter2Lemma221 where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Chapter2Lemma231.lagda.md b/src/HottBook/Chapter2Lemma231.lagda.md
index 3f0e00c..33815f5 100644
--- a/src/HottBook/Chapter2Lemma231.lagda.md
+++ b/src/HottBook/Chapter2Lemma231.lagda.md
@@ -1,4 +1,6 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter2Lemma231 where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Chapter2Util.agda b/src/HottBook/Chapter2Util.agda
index 09e6d04..05f17b4 100644
--- a/src/HottBook/Chapter2Util.agda
+++ b/src/HottBook/Chapter2Util.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter2Util where
 
 open import HottBook.Chapter1
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 6b58b6f..07b44a5 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -2,6 +2,8 @@
   <summary>Imports</summary>
 
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter3 where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Chapter3Definition331.lagda.md b/src/HottBook/Chapter3Definition331.lagda.md
index c915271..c867c60 100644
--- a/src/HottBook/Chapter3Definition331.lagda.md
+++ b/src/HottBook/Chapter3Definition331.lagda.md
@@ -1,4 +1,6 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter3Definition331 where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Chapter3Exercises.lagda.md b/src/HottBook/Chapter3Exercises.lagda.md
index f13512a..4f1cfef 100644
--- a/src/HottBook/Chapter3Exercises.lagda.md
+++ b/src/HottBook/Chapter3Exercises.lagda.md
@@ -1,4 +1,6 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter3Exercises where
 
 open import HottBook.Chapter1
diff --git a/src/HottBook/Chapter3Lemma333.lagda.md b/src/HottBook/Chapter3Lemma333.lagda.md
index 39fe562..a70677e 100644
--- a/src/HottBook/Chapter3Lemma333.lagda.md
+++ b/src/HottBook/Chapter3Lemma333.lagda.md
@@ -1,4 +1,6 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter3Lemma333 where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Chapter4.lagda.md b/src/HottBook/Chapter4.lagda.md
index 5a8f4e6..bc3f816 100644
--- a/src/HottBook/Chapter4.lagda.md
+++ b/src/HottBook/Chapter4.lagda.md
@@ -2,6 +2,8 @@
   <summary>Imports</summary>
 
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter4 where
 
 open import HottBook.Chapter1
diff --git a/src/HottBook/Chapter5.lagda.md b/src/HottBook/Chapter5.lagda.md
index d65a49c..45ecefa 100644
--- a/src/HottBook/Chapter5.lagda.md
+++ b/src/HottBook/Chapter5.lagda.md
@@ -1,4 +1,6 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter5 where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index ae5952f..0a41931 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -2,6 +2,8 @@
   <summary>Imports</summary>
 
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter6 where
 
 open import HottBook.Chapter1
diff --git a/src/HottBook/Chapter6Exercises.lagda.md b/src/HottBook/Chapter6Exercises.lagda.md
index 5fee9e9..f96f462 100644
--- a/src/HottBook/Chapter6Exercises.lagda.md
+++ b/src/HottBook/Chapter6Exercises.lagda.md
@@ -1,3 +1,5 @@
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter6Exercises where
 ```
\ No newline at end of file
diff --git a/src/HottBook/Chapter8.lagda.md b/src/HottBook/Chapter8.lagda.md
index b8e6fdb..89ecf2e 100644
--- a/src/HottBook/Chapter8.lagda.md
+++ b/src/HottBook/Chapter8.lagda.md
@@ -2,6 +2,8 @@
   <summary>Imports</summary>
 
 ```
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Chapter8 where
 
 open import HottBook.Chapter1
diff --git a/src/HottBook/CoreUtil.agda b/src/HottBook/CoreUtil.agda
index eac6abc..8126373 100644
--- a/src/HottBook/CoreUtil.agda
+++ b/src/HottBook/CoreUtil.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module HottBook.CoreUtil where
 
 open import Agda.Primitive
diff --git a/src/HottBook/Util.agda b/src/HottBook/Util.agda
index d24339d..bdca745 100644
--- a/src/HottBook/Util.agda
+++ b/src/HottBook/Util.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --rewriting #-}
+
 module HottBook.Util where
 
 open import Agda.Primitive