From 4e65fc2a32bb73ad3f6ccadbd79181d4786fb05b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 24 Jan 2025 05:46:08 -0600
Subject: [PATCH] wip

---
 src/ThesisWork/HomotopyGroupLES2/Step2.agda | 46 ++++++++++++++++-----
 src/ThesisWork/HomotopyGroupLES2/Step3.agda |  4 ++
 2 files changed, 39 insertions(+), 11 deletions(-)

diff --git a/src/ThesisWork/HomotopyGroupLES2/Step2.agda b/src/ThesisWork/HomotopyGroupLES2/Step2.agda
index a928907..f67269f 100644
--- a/src/ThesisWork/HomotopyGroupLES2/Step2.agda
+++ b/src/ThesisWork/HomotopyGroupLES2/Step2.agda
@@ -13,7 +13,7 @@ open import Cubical.Structures.Successor
 
 open import ThesisWork.Exactness
 open import ThesisWork.HomotopyGroupLES2.Util
-open import ThesisWork.HomotopyGroupLES2.Step1
+open import ThesisWork.HomotopyGroupLES2.Step1 renaming (A to A' ; f^ to f^')
 open import ThesisWork.HomotopyGroupLES2.Lemma415
 
 private
@@ -23,6 +23,8 @@ private
 pattern 3+ n = suc (suc (suc n))
 
 module _ {X∙ @ (X , x) : Pointed ℓ} {Y∙ @ (Y , y) : Pointed ℓ} (f∙ @ (f , f₀) : X∙ →∙ Y∙) where
+  A = A' f∙
+  f^ = f^' f∙
   F∙ = Fiber f∙
 
   B : (n : ℕ) → Pointed ℓ
@@ -37,28 +39,50 @@ module _ {X∙ @ (X , x) : Pointed ℓ} {Y∙ @ (Y , y) : Pointed ℓ} (f∙ @ (
   g^ 2 = δ f∙
   g^ (3+ n) = -Ω (g^ n)
 
-  _ : A f∙ 3 ≡ B 3
+  _ : A 3 ≡ B 3
   _ = ua∙ (eqv∙ f∙ .fst) (eqv∙ f∙ .snd)
 
   module Lemma416 where
-    η : (n : ℕ) → A f∙ n ≃∙ B n
+    η : (n : ℕ) → A n ≃∙ B n
     η 0 = idEquiv∙ Y∙
     η 1 = idEquiv∙ X∙
     η 2 = idEquiv∙ F∙
     η (3+ n) =
-      A f∙ (3+ n) ≃∙⟨ eqv∙ (f^ f∙ n) ⟩
-      Ω (A f∙ n) ≃∙⟨ cong-≃∙ Ω (η n) ⟩
+      A (3+ n) ≃∙⟨ eqv∙ (f^ n) ⟩
+      Ω (A n) ≃∙⟨ cong-≃∙ Ω (η n) ⟩
       Ω (B n) ∎≃∙
 
-    eqvfg : (n : ℕ) → (≃∙map (η n) ∘∙ f^ f∙ n) ∙∼ (g^ n ∘∙ ≃∙map (η (suc n)))
-    eqvfg 0 = {!   !}
-    eqvfg 1 = {!   !}
-    eqvfg 2 = {!   !}
-    eqvfg (3+ n) = {!   !}
+    A≡B : A ≡ B
+    A≡B = funExt (λ n → ua∙ (η n .fst) (η n .snd))
 
+    postulate
+      -- TODO: Finish
+      f∙∼g : (n : ℕ) → (≃∙map (η n) ∘∙ f^ n) ∙∼P (g^ n ∘∙ ≃∙map (η (suc n)))
+    -- eqvfg 0 = {!   !}
+    -- eqvfg 1 = {!   !}
+    -- eqvfg 2 = {!   !}
+    -- eqvfg (3+ n) = {!   !}
+
+    -- TODO: Is this actually easier?
+    -- Potential point of deviation from FVD thesis
+    f≡g' : (n : ℕ) → PathP (λ i → A≡B i (suc n) →∙ A≡B i n) (f^ n) (g^ n)
+    f≡g' 0 i = {!   !}
+      -- at i = i0, A^ 1 →∙ A^ 0
+      -- at i = i1, B^ 1 →∙ B^ 0
+    f≡g' 1 i = {!   !}
+    f≡g' 2 i = {!   !}
+    f≡g' (3+ n) = {!   !}
+
+    f≡g : PathP (λ i → (n : ℕ) → A≡B i (suc n) →∙ A≡B i n) f^ g^
+    f≡g = funExt f≡g'
+
+  open Lemma416 using (f≡g)
+
+  BⁿisExact : (n : ℕ) → isExactAt∙ (g^ (suc n)) (g^ n)
+  BⁿisExact n = transp (λ i → isExactAt∙ ((f≡g i) (suc n)) ((f≡g i) n)) i0 (AⁿisExact f∙ n)
 
   open ExactSequence∙
   BSeq : ExactSequence∙ ℕ+
   BSeq .seq = B
   BSeq .fun = g^
-  BSeq .exactness = {!   !}
\ No newline at end of file
+  BSeq .exactness = BⁿisExact
\ No newline at end of file
diff --git a/src/ThesisWork/HomotopyGroupLES2/Step3.agda b/src/ThesisWork/HomotopyGroupLES2/Step3.agda
index 8009ac6..6e2f433 100644
--- a/src/ThesisWork/HomotopyGroupLES2/Step3.agda
+++ b/src/ThesisWork/HomotopyGroupLES2/Step3.agda
@@ -1,3 +1,7 @@
 {-# OPTIONS --cubical #-}
 
 module ThesisWork.HomotopyGroupLES2.Step3 where
+
+open import ThesisWork.HomotopyGroupLES2.Step2 renaming (B to B' ; g^ to g^')
+
+module _ {X∙ @ (X , x) : Pointed ℓ} {Y∙ @ (Y , y) : Pointed ℓ} (f∙ @ (f , f₀) : X∙ →∙ Y∙) where