a

src/HottBook/Chapter2.lagda.md

@@ -358,11 +358,12 @@ postulate
 ## 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
+private
+  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
@@ -430,4 +431,4 @@ theorem2∙13∙1 m n = encode m n , equiv
       ; h = decode m n
       ; h-id = backward m n
       }
-```
+```

src/HottBook/Chapter8.lagda.md

@@ -2,6 +2,8 @@
 module HottBook.Chapter8 where
 
 open import Agda.Primitive
+open import HottBook.Chapter1
+open import HottBook.Chapter2
 open import HottBook.Chapter6
 ```
 
@@ -14,6 +16,6 @@ data ℤ : Set where
 ```
 
 ```
-code : {l : Level} → S¹ → Set l
-code {l} = S¹-elim (λ _ → Set l) ℤ (ua succ)
+code : {l : Level} → S¹ → Set (lsuc l)
+code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)
 ```