diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index da3c098..01af651 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -14,6 +14,13 @@ isSet : (A : Set) → Set
 isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ```
 
+### Example 3.1.1
+
+```
+𝟙-is-Set : isSet 𝟙
+𝟙-is-Set tt tt p q = {!    !}
+```
+
 ## 3.2 Propositions as types?
 
 ## 3.4 Classical vs. intuitionistic logic