diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 5daed49..263c259 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -18,7 +18,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 
 ```
 𝟙-is-Set : isSet 𝟙
-𝟙-is-Set tt tt p q = {!    !}
+𝟙-is-Set tt tt p q = J (λ x y p' → p' ≡ q) (λ x → {!   !}) tt tt p
 ```
 
 ### Example 3.1.3