diff --git a/src/2022-10-10-notes.lagda.md b/src/2022-10-10-notes.lagda.md
index 188023f..174b9d8 100644
--- a/src/2022-10-10-notes.lagda.md
+++ b/src/2022-10-10-notes.lagda.md
@@ -1,5 +1,4 @@
-2022 Oct 10
-===
+# 2022 Oct 10
 
 ```agda
 {-# OPTIONS --cubical #-}
diff --git a/src/2023-08-05-scratchpad.agda b/src/2023-08-05-scratchpad.agda
new file mode 100644
index 0000000..e69de29
diff --git a/src/Ch2.agda b/src/Ch2.agda
index 6cae3ef..3733683 100644
--- a/src/Ch2.agda
+++ b/src/Ch2.agda
@@ -11,7 +11,7 @@ path-ind : {A : Set}
   → (C : (x y : A) → x ≡ y → Set)
   → (c : (x : A) → C x x refl)
   → (x y : A) → (p : x ≡ y) → C x y p
-path-ind C c x y p = ?
+path-ind C c x y p = {!   !}
 
 -- Lemma 2.1.1
 
@@ -52,13 +52,13 @@ ap f p i = f (p i)
 
 lemma2111 : {A B : Set} → (f : A → B) → (ie : isEquiv f) → {a a′ : A}
   → isEquiv (ap f)
-lemma2111 f ie .equiv-proof y = ?
+lemma2111 f ie .equiv-proof y = {!   !}
 
 -- Lemma 2.11.2
 
 lemma2112a : {A : Set} → (a : A) → {x₁ x₂ : A} → (p : x₁ ≡ x₂) → (q : a ≡ x₁)
-  → transport ? p ≡ q ∙ p
-lemma2112a a p q = ?
+  → transport {!   !} p ≡ q ∙ p
+lemma2112a a p q = {!   !}
 
 -- Lemma 2.11.3
 
diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index 2833c08..60ecffd 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -1,10 +1,11 @@
 ```
 module HottBook.Chapter1 where
 
+open import Relation.Binary.PropositionalEquality
 open import Data.Empty
 open import Data.Sum
 
-Type = Set
+open import HottBook.Common
 ```
 
 ## 1.7 Coproduct types
@@ -21,3 +22,12 @@ A + B = A ⊎ B
 ¬_ : (A : Type) → Type
 ¬ A = A → ⊥
 ```
+
+## 1.12.1 Path Induction
+
+```
+J : {A : Type} → (C : (x y : A) → x ≡ y → Type)
+  → (c : (x : A) → C x x refl)
+  → (x y : A) → (p : x ≡ y) → C x y p
+J C c x x refl = c x
+```
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index eeecd0d..b194e8b 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -5,12 +5,14 @@ open import Relation.Binary.PropositionalEquality
 open import Function
 open import Data.Product
 open import Data.Product.Properties
-Type = Set
 
-infixr 6 _∙_
-_∙_ = trans
+open import HottBook.Common
+open import HottBook.Chapter1
 ```
 
+> An internal error has occurred. Please report this as a bug.
+> Location of the error: `__IMPOSSIBLE__`, called at src/full/Agda/Interaction/Imports.hs:915:15 in Agd-2.6.3-d4728884:Agda.Interaction.Imports
+
 ## 2.2 Functions are functors
 
 ### Lemma 2.2.1
@@ -222,16 +224,16 @@ data 𝟙 : Set where
 -- open import Function.HalfAdjointEquivalence
 -- _is-⋆ : (x : 𝟙) → x ≡ ⋆
 -- ⋆ is-⋆ = refl
--- 
+--
 -- theorem281-helper2 : {x : 𝟙} → (p : x ≡ x) → p ≡ refl
--- theorem281-helper2 {x} p = 
+-- theorem281-helper2 {x} p =
 --   let a = sym (x is-⋆) ∙ p ∙ (x is-⋆) in
 --   J (λ the what → p ≡ the) ? ?
--- 
+--
 -- theorem281-helper : {x y : 𝟙} → (p : x ≡ y) → (x is-⋆) ∙ sym (y is-⋆) ≡ p
 -- theorem281-helper {x} p =
 --   J (λ the what → (x is-⋆) ∙ sym (the is-⋆) ≡ what) p (theorem281-helper2 _)
--- 
+--
 -- theorem281 : (x y : 𝟙) → (x ≡ y) ≃ 𝟙
 -- theorem281 x y = record
 --   { to = λ _ → ⋆
diff --git a/src/HottBook/Common.agda b/src/HottBook/Common.agda
new file mode 100644
index 0000000..2e0f4db
--- /dev/null
+++ b/src/HottBook/Common.agda
@@ -0,0 +1,6 @@
+open import Relation.Binary.PropositionalEquality
+
+Type = Set
+
+infixr 6 _∙_
+_∙_ = trans
\ No newline at end of file