diff --git a/src/Dedekind/Bool.agda b/src/Dedekind/Bool.agda
deleted file mode 100644
index eb288fb..0000000
--- a/src/Dedekind/Bool.agda
+++ /dev/null
@@ -1,8 +0,0 @@
-module Dedekind.Bool where
-
--- Booleans
-data Bool : Set where
-  true : Bool
-  false : Bool
-
-
diff --git a/src/Dedekind/Integer.agda b/src/Dedekind/Integer.agda
deleted file mode 100644
index 4c9e181..0000000
--- a/src/Dedekind/Integer.agda
+++ /dev/null
@@ -1,8 +0,0 @@
-module Dedekind.Integer where
-
-open import Dedekind.Natural using (ℕ)
-
--- Integers
-data ℤ : Set where
-  pos : ℕ → ℤ
-  negsuc : ℕ → ℤ
diff --git a/src/Dedekind/Natural.agda b/src/Dedekind/Natural.agda
deleted file mode 100644
index 2399d68..0000000
--- a/src/Dedekind/Natural.agda
+++ /dev/null
@@ -1,15 +0,0 @@
-module Dedekind.Natural where
-
-open import Dedekind.Set using (⊤; ⊥)
-
--- Natural
-data ℕ : Set where
-  zero : ℕ
-  suc : ℕ → ℕ
-
-NonZero : ℕ → Set
-NonZero zero = ⊥
-NonZero (suc n) = ⊤
-
-gcd : (x y : ℕ) .{{ _ : NonZero x }} .{{ _ : NonZero y }} → ℕ
-gcd x y = ?
diff --git a/src/Dedekind/Rational.agda b/src/Dedekind/Rational.agda
deleted file mode 100644
index 2153f33..0000000
--- a/src/Dedekind/Rational.agda
+++ /dev/null
@@ -1,12 +0,0 @@
-module Dedekind.Rational where
-
-open import Dedekind.Bool using (Bool)
-open import Dedekind.Integer using (ℤ)
-open import Dedekind.Natural using (ℕ; NonZero)
-
--- Rational
-data ℚ : Set where
-  rat : ℤ → (d : ℕ) .{{ _ : NonZero d }} → ℚ
-
-_<_ : ℚ → ℚ → Bool
-x < y = ?
diff --git a/src/Dedekind/Real.agda b/src/Dedekind/Real.agda
deleted file mode 100644
index e442b56..0000000
--- a/src/Dedekind/Real.agda
+++ /dev/null
@@ -1,20 +0,0 @@
--- Dedekind cuts using Cubical Agda
-{-# OPTIONS --cubical #-}
-
-module Dedekind.Real where
-
-open import Dedekind.Rational using (ℚ; _<_)
-
--- Dedekind cuts
-record ℝ : Set where
-  constructor real
-  field
-    lower : (ℚ → Bool)
-    closed : ∀ (x y : ℚ) → x < y
-
--- Operations on reals
-_+_ : ℝ → ℝ → ℝ
-a + b = real 
-  (λ q → ℝ.lower a q)
-
--- Properties of reals
diff --git a/src/Dedekind/Set.agda b/src/Dedekind/Set.agda
deleted file mode 100644
index 45fa565..0000000
--- a/src/Dedekind/Set.agda
+++ /dev/null
@@ -1,6 +0,0 @@
-module Dedekind.Set where
-
-record ⊥ : Set where
-
-record ⊤ : Set where
-  instance constructor tt
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 01af651..5daed49 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -14,13 +14,20 @@ isSet : (A : Set) → Set
 isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ```
 
-### Example 3.1.1
+### Example 3.1.2
 
 ```
 𝟙-is-Set : isSet 𝟙
 𝟙-is-Set tt tt p q = {!    !}
 ```
 
+### Example 3.1.3
+
+```
+⊥-is-Set : isSet ⊥
+⊥-is-Set () () p q
+```
+
 ## 3.2 Propositions as types?
 
 ## 3.4 Classical vs. intuitionistic logic