From 56394e55aad2dad1d33e7c71c3e51df8b54080cb Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 11 Jul 2024 02:07:11 -0500
Subject: [PATCH] updates

---
 src/CubicalHott/Chapter3.lagda.md |  7 +++++--
 src/HottBook/Chapter3.lagda.md    | 31 +++++++++++++++++++------------
 2 files changed, 24 insertions(+), 14 deletions(-)

diff --git a/src/CubicalHott/Chapter3.lagda.md b/src/CubicalHott/Chapter3.lagda.md
index 5a0e344..e60375e 100644
--- a/src/CubicalHott/Chapter3.lagda.md
+++ b/src/CubicalHott/Chapter3.lagda.md
@@ -72,8 +72,11 @@ postulate
 
 ```
 lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥
-lemma3∙9∙1 {P} prop = ∣_∣ , qinv-to-isequiv (mkQinv inv {!   !} {!   !})
+lemma3∙9∙1 {P} Pprop = ∣_∣ , qinv-to-isequiv (mkQinv inv {!   !} {!   !})
   where
     inv : ∥ P ∥ → P
-    inv = {! rec-∥ P ∥  !}
+    inv ∣ a ∣ = a
+    inv (witness p q i) =
+      let what = ap ∥_∥ {!   !}
+      in {!   !}
 ```
\ No newline at end of file
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index a2011a1..6033a30 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -319,7 +319,9 @@ module section3∙7 where
     ∣_∣ : {A : Set l} → (a : A) → ∥ A ∥
     witness : {A : Set l} → (x y : ∥ A ∥) → x ≡ y → Set l
 
-    rec-∥_∥ : (A : Set l) → {B : Set l} → isProp B → (f : A → B)
+    rec-∥_∥ : (A : Set l) → {B : Set l}
+      → isProp B
+      → (f : A → B)
       → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
 open section3∙7 public
 ```
@@ -365,9 +367,9 @@ open definition3∙8∙1 public
 ### Lemma 3.8.2
 
 ```
-module lemma3∙8∙2 where
-  definition3∙8∙3 : {X : Set} → (Y : X → Set) → ((x : X) → isSet (Y x)) → ((x : X) → ∥ (Y x) ∥) → ∥ ((x : X) → Y x) ∥
-  definition3∙8∙3 {X} Y allYSet = {!   !}
+-- module lemma3∙8∙2 where
+--   definition3∙8∙3 : {X : Set} → (Y : X → Set) → ((x : X) → isSet (Y x)) → ((x : X) → ∥ (Y x) ∥) → ∥ ((x : X) → Y x) ∥
+--   definition3∙8∙3 {X} Y allYSet = {!   !}
 ```
 
 ## 3.9 The principle of unique choice
@@ -376,11 +378,14 @@ module lemma3∙8∙2 where
 
 ```
 lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
-lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
+lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop prop2 ∣_∣ g
   where
-    thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ a)
-    thing = rec-∥ P ∥ prop id
+    open Σ
 
+    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
@@ -390,12 +395,14 @@ lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
     -- x y : ∥ P ∥
     prop2 x y = 
       let
-        gx = g x
-        gy = g y
-        eqP = prop gx gy
-        gpx = g-prop gx
+        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