diff --git a/src/2024-05-09-perry-meeting.agda b/src/2024-05-09-perry-meeting.agda
new file mode 100644
index 0000000..03d74e9
--- /dev/null
+++ b/src/2024-05-09-perry-meeting.agda
@@ -0,0 +1,29 @@
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Util
+
+test : {A B : Set}
+  → (equiv @ (f , fIsEquiv) : A ≃ B)
+  → (x y : A)
+  → (x ≡ y) ≃ (f x ≡ f y)
+test (equiv @ (f , mkIsEquiv g g-id h h-id)) x y = f2 , f2IsEquiv
+  where
+    f2 : x ≡ y → f x ≡ f y
+    f2 p = ap f p
+
+    g2 : f x ≡ f y → x ≡ y
+    g2 p = 
+      let p1 = ap h p in
+      let p2 = trans p1 (h-id y) in
+      let p3 = trans (sym (h-id x)) p2 in
+      p3
+
+    forwards : f2 ∘ g2 ∼ id
+    forwards b = {!   !}
+      where
+        q = let y = f2 ∘ g2 in {!   !}
+
+    backwards : g2 ∘ f2 ∼ id
+    backwards b = {!   !}
+
+    f2IsEquiv = mkIsEquiv g2 forwards g2 backwards
\ No newline at end of file
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 2a0a633..16f3fca 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -1,10 +1,15 @@
-```
-module HottBook.Chapter2 where
+<details>
+  <summary>Imports</summary>
 
-open import Agda.Primitive
-open import HottBook.Chapter1
-open import HottBook.Util
-```
+  ```
+  module HottBook.Chapter2 where
+
+  open import Agda.Primitive
+  open import HottBook.Chapter1
+  open import HottBook.Util
+  ```
+
+</details>
 
 ## 2.1 Types are higher groupoids
 
@@ -256,7 +261,7 @@ _≃_ : {l : Level} → (A B : Set l) → Set l
 A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
 ```
 
-## 2.8 Σ-types
+## 2.7 Σ-types
 
 ### Theorem 2.7.2
 
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index c82ed63..cba8dc2 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -53,20 +53,20 @@ isProp P = (x y : P) → x ≡ y
 ### Lemma 3.3.2
 
 ```
-lemma3∙2∙2 : {P : Set}
-  → isProp P
-  → (x₀ : P)
-  → P ≃ 𝟙
-lemma3∙2∙2 {P} PisProp x₀ = f , mkIsEquiv g {!  forwards !} g {!   !}
-  where
-    f : P → 𝟙
-    f x = tt
+-- lemma3∙2∙2 : {P : Set}
+--   → isProp P
+--   → (x₀ : P)
+--   → P ≃ 𝟙
+-- lemma3∙2∙2 {P} PisProp x₀ = f , mkIsEquiv g {!  forwards !} g {!   !}
+--   where
+--     f : P → 𝟙
+--     f x = tt
 
-    g : 𝟙 → P
-    g u = x₀
+--     g : 𝟙 → P
+--     g u = x₀
 
-    forwards : f ∘ g ∼ id
-    forwards x = {! refl  !}
+--     forwards : f ∘ g ∼ id
+--     forwards x = {! refl  !}
 ```
 
 ## 3.4 Classical vs. intuitionistic logic
diff --git a/src/HottBook/Chapter4.lagda.md b/src/HottBook/Chapter4.lagda.md
index 2aa85d8..e1e6d35 100644
--- a/src/HottBook/Chapter4.lagda.md
+++ b/src/HottBook/Chapter4.lagda.md
@@ -1,5 +1,9 @@
 ```
 module HottBook.Chapter4 where
+
+open import HottBook.Chapter1
+open import HottBook.Chapter2
+open import HottBook.Chapter3
 ```
 
 ## 4.1 Quasi-inverses
@@ -7,3 +11,14 @@ module HottBook.Chapter4 where
 ```
 -- qinv : {A B : Type} (f : A → B) → 
 ```
+
+### Theorem 4.1.3
+
+There exist types A and B and a function f : A → B such that qinv( f ) is not a mere proposition.
+
+```
+theorem4∙1∙3 : {A B : Set}
+  → (f : A → B)
+  → isProp (qinv f) → ⊥
+theorem4∙1∙3 f p = {!   !}
+```
\ No newline at end of file