From 130cda914b04b88d13fb91f4ca702e9b1256d230 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sat, 13 Jul 2024 17:15:34 -0400
Subject: [PATCH] lemma 3.9.1

---
 .vscode/settings.json          |  2 +-
 src/HottBook/Chapter1.lagda.md |  1 +
 src/HottBook/Chapter3.lagda.md | 44 ++++++++++++----------------------
 3 files changed, 17 insertions(+), 30 deletions(-)

diff --git a/.vscode/settings.json b/.vscode/settings.json
index 6dabf9e..0e67ce1 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -3,7 +3,7 @@
 	"gitdoc.enabled": false,
 	"gitdoc.autoCommitDelay": 300000,
 	"gitdoc.commitMessageFormat": "'auto gitdoc commit'",
-	"agdaMode.connection.commandLineOptions": "",
+	"agdaMode.connection.commandLineOptions": "--rewriting",
 	"search.exclude": {
 		"src/CubicalHott/**": true
 	}
diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index e5ab39c..7b87a40 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -145,6 +145,7 @@ infix 3 ¬_
 infix 4 _≡_
 data _≡_ {A : Set l} : (a b : A) → Set l where
   instance refl : {x : A} → x ≡ x
+{-# BUILTIN REWRITE _≡_ #-}
 ```
 
 ### 1.12.3 Disequality
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index c268f5e..1116007 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -393,14 +393,22 @@ example3∙6∙2 {A} {B} allProps = λ f g → funext λ x → allProps x (f x)
 module section3∙7 where
   postulate
     ∥_∥ : Set l → Set l
-    ∣_∣ : {A : Set l} → (a : A) → ∥ A ∥
-    witness : {A : Set l} → (x y : ∥ A ∥) → x ≡ y → Set l
+    ∣_∣ : {A : Set l} → A → ∥ A ∥
+    trunc-witness : {A : Set l} → isProp (∥ A ∥)
 
     rec-∥_∥ : (A : Set l) → {B : Set l}
       → isProp B
       → (f : A → B)
       → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
+    
+    trunc-rec : (A : Set) → {B : Set} → isProp B → (f : A → B)
+      → ∥ A ∥ → B
+
+    trunc-rec-1 : {A : Set} → {B : Set} → (Bprop : isProp B) → (f : A → B)
+      → (a : A) → trunc-rec A Bprop f (∣ a ∣) ≡ f a
+
 open section3∙7 public
+{-# REWRITE trunc-rec-1 #-}
 ```
 
 ### Definition 3.7.1
@@ -455,35 +463,13 @@ open definition3∙8∙1 public
 
 ```
 lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
-lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop prop2 ∣_∣ g
+lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop witness ∣_∣ rec-func
   where
-    open Σ
+    rec-func : ∥ P ∥ → P
+    rec-func = trunc-rec P Pprop id
 
-    thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ a)
-    thing = rec-∥ P ∥ Pprop id
-
-    g : ∥ P ∥ → P
-    g = Σ.fst thing
-
-    g-prop : (a : P) → g ∣ a ∣ ≡ a
-    g-prop = Σ.snd thing
-
-    prop2 : isProp ∥ P ∥
-    -- x y : ∥ P ∥
-    prop2 x y = 
-      let
-        gx = g x -- : g x
-        gy = g y -- : g y
-        eqP = Pprop gx gy -- : gx ≡ gy
-        gpx = g-prop gx   -- : g (∣ gx ∣) ≡ gx
-        what = gpx ∙ eqP
-        prevResult = (lemma3∙9∙1 {P} Pprop) .snd .isequiv.g-id
-      in
-      admit
-      where
-        postulate
-          -- TODO: Finish this 
-          admit : x ≡ y
+    witness : isProp ∥ P ∥
+    witness = trunc-witness
 ```
 
 ### Corollary 3.9.2