lol

.vscode/settings.json

@@ -3,5 +3,8 @@
 	"gitdoc.enabled": false,
 	"gitdoc.autoCommitDelay": 300000,
 	"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
-	"agdaMode.connection.commandLineOptions": ""
+	"agdaMode.connection.commandLineOptions": "",
+	"search.exclude": {
+		"src/HottBook/**": true
+	}
 }

src/CubicalHott/Chapter1.lagda.md

@@ -1,5 +1,5 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Chapter1 where
 
 open import CubicalHott.Primitives public

src/CubicalHott/Chapter2.lagda.md

@@ -1,5 +1,5 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Chapter2 where
 
 open import CubicalHott.Chapter1

src/CubicalHott/Chapter2Lemma221.lagda.md

@@ -1,5 +1,5 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Chapter2Lemma221 where
 
 open import CubicalHott.Chapter1

src/CubicalHott/Chapter3.lagda.md

@@ -1,5 +1,5 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Chapter3 where
 
 open import CubicalHott.Chapter1

src/CubicalHott/Chapter6.lagda.md

@@ -1,5 +1,5 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Chapter6 where
 
 open import CubicalHott.Chapter1

src/CubicalHott/Primitives.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Primitives where
 
 open import CubicalHott.Primitives.Interval public

src/CubicalHott/Primitives/Interval.lagda.md

@@ -1,5 +1,5 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Primitives.Interval where
 
 open import CubicalHott.Primitives.Type

src/CubicalHott/Primitives/Kan.lagda.md

@@ -1,5 +1,5 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Primitives.Kan where
 
 open import CubicalHott.Primitives.Type

src/CubicalHott/Primitives/Type.lagda.md

@@ -1,5 +1,5 @@
 ```
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --no-load-primitives --cubical #-}
 module CubicalHott.Primitives.Type where
 ```