From d2d19f42bda1417752bc95e90ee9527557b730c5 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 16 Oct 2024 17:50:43 -0500
Subject: [PATCH] progress

---
 src/ThesisWork/Pi3S2/Lemma4-1-5.agda | 66 +++++++++++++++++++++++++---
 src/ThesisWork/Pi3S2/SuccStr.agda    |  4 +-
 2 files changed, 63 insertions(+), 7 deletions(-)

diff --git a/src/ThesisWork/Pi3S2/Lemma4-1-5.agda b/src/ThesisWork/Pi3S2/Lemma4-1-5.agda
index c8ce4e7..28058a3 100644
--- a/src/ThesisWork/Pi3S2/Lemma4-1-5.agda
+++ b/src/ThesisWork/Pi3S2/Lemma4-1-5.agda
@@ -4,6 +4,7 @@ module ThesisWork.Pi3S2.Lemma4-1-5 where
 
 open import Cubical.Data.Sigma
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Pointed
@@ -23,14 +24,69 @@ lemma {A∙ = A∙ @ (A , a0)} {B∙ = B∙ @ (B , b0)} f∙ @ (f , f-eq) = eqv
   eqv : fst (fiberF ((λ r → fst r) , refl)) ≃ fst (Ω B∙)
   eqv =
       fst (fiberF ((λ r → fst r) , refl))
-    ≃⟨ {!   !} ⟩
+    ≃⟨ idEquiv (fst (fiberF (fst , refl))) ⟩
       Σ (fst (fiberF f∙)) (λ fibf @ (a , p) → a ≡ a0)
-    ≃⟨ {!   !} ⟩
+    ≃⟨ helper1 ⟩
       Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
-    ≃⟨ {!   !} ⟩
+    ≃⟨ helper2 ⟩
       f a0 ≡ b0
-    ≃⟨ {!   !} ⟩
+    ≃⟨ helper3 ⟩
       b0 ≡ b0
     ≃⟨ idEquiv (b0 ≡ b0) ⟩
       fst (Ω B∙)
-    ■
+    ■ where
+      helper1 : Σ (fst (fiberF (f , f-eq))) (λ fibf → fibf .fst ≡ a0) ≃ Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
+      helper1 = isoToEquiv (iso f' g' (λ _ → refl) λ _ → refl) where
+        f' : Σ (fst (fiberF (f , f-eq))) (λ fibf → fibf .fst ≡ a0) → Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
+        f' x @ ((x1 , x2) , x3) = x1 , x3 , x2 
+
+        g' : Σ A (λ a → (a ≡ a0) × (f a ≡ b0)) → Σ (fst (fiberF (f , f-eq))) (λ fibf → fibf .fst ≡ a0)
+        g' x @ (x1 , x2 , x3) = (x1 , x3) , x2
+
+      helper2 : Σ A (λ a → (a ≡ a0) × (f a ≡ b0)) ≃ (f a0 ≡ b0)
+      helper2 = isoToEquiv (iso f' g' fg {!   !}) where
+        f' : Σ A (λ a → (a ≡ a0) × (f a ≡ b0)) → f a0 ≡ b0
+        f' (x1 , x2 , x3) = cong f (sym x2) ∙ x3 
+
+        g' : f a0 ≡ b0 → Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
+        g' x = a0 , refl , x
+
+        fg : section f' g'
+        fg b =
+          f' (g' b) ≡⟨ refl ⟩
+          f' (a0 , refl , b) ≡⟨ refl ⟩
+          cong f (sym refl) ∙ b ≡⟨ refl ⟩
+          refl ∙ b ≡⟨ sym (lUnit b) ⟩
+          b ∎
+
+        gf : retract f' g'
+        gf a @ (x1 , x2 , x3) =
+          g' (cong f (sym x2) ∙ x3) ≡⟨ refl ⟩
+          a0 , refl , (cong f (sym x2) ∙ x3) ≡⟨ cong (λ b → {!   !}) {!   !} ⟩
+          a ∎
+
+      helper3 : (f a0 ≡ b0) ≃ (b0 ≡ b0)
+      helper3 = isoToEquiv (iso f' g' fg gf) where
+        f' : f a0 ≡ b0 → b0 ≡ b0
+        f' x = sym f-eq ∙ x
+
+        g' : b0 ≡ b0 → f a0 ≡ b0
+        g' x = f-eq ∙ x
+
+        fg : section f' g'
+        fg b =
+          f' (g' b) ≡⟨ refl ⟩
+          f' (f-eq ∙ b) ≡⟨ refl ⟩
+          sym f-eq ∙ (f-eq ∙ b) ≡⟨ assoc (sym f-eq) f-eq b ⟩
+          (sym f-eq ∙ f-eq) ∙ b ≡⟨ cong (_∙ b) (lCancel f-eq) ⟩
+          refl ∙ b ≡⟨ sym (lUnit b) ⟩
+          b ∎ 
+
+        gf : retract f' g'
+        gf a =
+          g' (f' a) ≡⟨ refl ⟩
+          g' (sym f-eq ∙ a) ≡⟨ refl ⟩
+          f-eq ∙ (sym f-eq ∙ a) ≡⟨ assoc f-eq (sym f-eq) a ⟩
+          (f-eq ∙ sym f-eq) ∙ a ≡⟨ cong (_∙ a) (rCancel f-eq) ⟩
+          refl ∙ a ≡⟨ sym (lUnit a) ⟩
+          a ∎
\ No newline at end of file
diff --git a/src/ThesisWork/Pi3S2/SuccStr.agda b/src/ThesisWork/Pi3S2/SuccStr.agda
index 2cf9998..ba3ee18 100644
--- a/src/ThesisWork/Pi3S2/SuccStr.agda
+++ b/src/ThesisWork/Pi3S2/SuccStr.agda
@@ -3,7 +3,7 @@
 module ThesisWork.Pi3S2.SuccStr where
 
 open import Cubical.Foundations.Prelude
-open import Data.Nat
+open import Data.Nat using (ℕ ; zero ; suc)
 
 SuccStr : (I : Type) (S : I → I) → (i : I) → (n : ℕ) → I
 SuccStr I S i zero = i 
@@ -17,7 +17,7 @@ module _ where
   ℕ-SuccStr = SuccStr ℕ suc
 
 module _ where
-  open import Data.Integer renaming (suc to zsuc)
+  open import Data.Integer using (ℤ) renaming (suc to zsuc)
 
   -- (ℤ , λ n . n + 1)
   ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ