diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 5e29448..8da10c6 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -354,3 +354,31 @@ postulate
 postulate
   ua : {A B : Set} (eqv : A ≃ B) → (A ≡ B)
 ```
+
+## 2.13 Natural numbers
+
+```
+code : ℕ → ℕ → Set
+code zero zero = 𝟙
+code zero (suc y) = ⊥
+code (suc x) zero = ⊥
+code (suc x) (suc y) = code x y
+```
+
+### Theorem 2.13.1
+
+```
+theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n
+theorem2∙13∙1 m n = {!   !}
+  where
+    r : (n : ℕ) → code n n
+    r zero = tt
+    r (suc n) = r n
+
+    encode : (m n : ℕ) → m ≡ n → code m n
+    encode m n p = transport (λ n → code m n) p (r m)
+
+    decode : (m n : ℕ) → code m n → m ≡ n
+    decode zero zero c = refl
+    decode (suc m) (suc n) c = {!   !}
+```
\ No newline at end of file
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 263c259..785e54e 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 = J (λ x y p' → p' ≡ q) (λ x → {!   !}) tt tt p
+𝟙-is-Set tt tt refl refl = refl
 ```
 
 ### Example 3.1.3
@@ -28,6 +28,13 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ⊥-is-Set () () p q
 ```
 
+### Example 3.1.4
+
+```
+ℕ-is-Set : isSet ℕ
+ℕ-is-Set = {!   !}
+```
+
 ## 3.2 Propositions as types?
 
 ## 3.4 Classical vs. intuitionistic logic