From fea38f46f5162354d495299fc6ce6700f285800d Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 23 Jan 2025 23:10:11 -0600
Subject: [PATCH] more work on homotopy group LES

---
 src/ThesisWork/HomotopyGroupLES.agda          |  84 +++++++++++--
 src/ThesisWork/HomotopyGroupLES2.agda         |  68 +++++++++++
 .../HomotopyGroupLES2/Lemma415.agda           | 110 ++++++++++++++++++
 src/ThesisWork/HomotopyGroupLES2/Step1.agda   |  93 +++++++++++++++
 src/ThesisWork/HomotopyGroupLES2/Step2.agda   |  64 ++++++++++
 src/ThesisWork/HomotopyGroupLES2/Step3.agda   |   3 +
 src/ThesisWork/HomotopyGroupLES2/Util.agda    |  29 +++++
 type-theory.agda-lib                          |   2 +-
 8 files changed, 441 insertions(+), 12 deletions(-)
 create mode 100644 src/ThesisWork/HomotopyGroupLES2.agda
 create mode 100644 src/ThesisWork/HomotopyGroupLES2/Lemma415.agda
 create mode 100644 src/ThesisWork/HomotopyGroupLES2/Step1.agda
 create mode 100644 src/ThesisWork/HomotopyGroupLES2/Step2.agda
 create mode 100644 src/ThesisWork/HomotopyGroupLES2/Step3.agda
 create mode 100644 src/ThesisWork/HomotopyGroupLES2/Util.agda

diff --git a/src/ThesisWork/HomotopyGroupLES.agda b/src/ThesisWork/HomotopyGroupLES.agda
index 70b099f..cc4a438 100644
--- a/src/ThesisWork/HomotopyGroupLES.agda
+++ b/src/ThesisWork/HomotopyGroupLES.agda
@@ -6,6 +6,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
 open import Cubical.HITs.TypeQuotients
 open import Cubical.Foundations.Structure
@@ -21,6 +22,8 @@ open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Homotopy.Group.Base
 open import Cubical.Homotopy.Loopspace
 
+import Cubical.Homotopy.Group.LES
+
 open import ThesisWork.Exactness
 
 -- The long exact sequence of homotopy groups
@@ -47,7 +50,7 @@ module _ where
   NFin3+ .Index = NFin3
   NFin3+ .succ = sucNFin3
 
-Fiber : {A B : Pointed ℓ} (f : A →∙ B) → Pointed ℓ
+Fiber : {A B : Pointed ℓ} (f∙ : A →∙ B) → Pointed ℓ
 Fiber {A = A , a} {B = B , b} (f , feq) = (fiber f b) , a , feq
 
 -- General definition of p₁ as the first projection
@@ -57,18 +60,77 @@ p₁ = fst , refl
 -- Lemma 4.1.5 in FVD thesis
 -- Suppose given a pointed map f : A →∗ B
 module _ {A∙ @ (A , a) B∙ @ (B , b) : Pointed ℓ} (f∙ @ (f , f-eq) : A∙ →∙ B∙) where
+  -- Fix this instance of p1
+  p1 = p₁ {A∙ = A∙} {B∙ = B∙} {f∙ = f∙}
+
   private
-    -- Let p1 : fib_f →∗ A be the first projection. 
-    lol : (f∙ .fst a ≡ b) , f-eq ≃∙ (b ≡ b) , (λ i → b)
-    lol .fst = pathToEquiv (cong (λ z → z ≡ b) f-eq)
-    lol .snd i j = {!   !}
+    leg1 : (Σ (fiber f b) λ (a' , p) → a' ≡ a) , ((a , f-eq) , refl) ≃∙ (Σ A λ a' → (a' ≡ a) × (f a' ≡ b)) , (a , refl , f-eq)
+    leg1 = isoToEquiv (iso f1 g1 {!   !} {!   !}) , {!   !} where
+      f1 : (Σ (fiber f b) λ (a' , p) → a' ≡ a) → (Σ A λ a' → (a' ≡ a) × (f a' ≡ b))
+      f1 (fib , fib-eq) = (fib .fst) , fib-eq , subst (λ p → f∙ .fst p ≡ b) (sym fib-eq) f-eq
+
+      g1 : (Σ A λ a' → (a' ≡ a) × (f a' ≡ b)) → (Σ (fiber f b) λ (a' , p) → a' ≡ a)
+      g1 (a , a-pf , f-a) = (a , subst (λ p → f∙ .fst p ≡ b) (sym a-pf) f-eq) , a-pf
+
+      fg : section f1 g1
+      fg x = {!   !}
+
+    leg2 : (Σ A λ a' → (a' ≡ a) × (f a' ≡ b)) , (a , refl , f-eq) ≃∙ (f a ≡ b) , f-eq
+    leg2 = isoToEquiv (iso f1 g1 {!   !} {!   !}) , {!   !} where
+      f1 : (Σ A λ a' → (a' ≡ a) × (f a' ≡ b)) → (f a ≡ b)
+      f1 (a' , a-prf , f-prf) = subst (λ p → f p ≡ b) a-prf f-prf
+      
+      g1 : (f a ≡ b) → (Σ A λ a' → (a' ≡ a) × (f a' ≡ b))
+      g1 p = a , refl , p
+
+      fg : section f1 g1
+      fg p = substRefl {B = λ p → f p ≡ b} p
+      
+      gf : retract f1 g1
+      gf (a' , a-prf , f-prf) =
+        {!   !}
+        -- f(a',a-prf,f-prf) = subst (λ p → f p ≡ b) a-prf f-prf
+        -- g(f(...)) = a  , refl  , subst (λ p → f p ≡ b) a-prf f-prf
+        --           ≡ a' , a-prf , f-prf
+        -- this becomes: a , refl , subst (λ p → f p ≡ b) refl f-prf ≡ a , refl , f-prf
+
+    leg3 : (f a ≡ b) , f-eq ≃∙ (b ≡ b) , refl
+    leg3 = (isoToEquiv (iso f1 g1 fg {! λ _ → refl !})) , {!   !} where
+      f1 : f a ≡ b → b ≡ b
+      f1 p = subst (λ x → x ≡ b) p p
+
+      g1 : b ≡ b → f a ≡ b
+      g1 p = f-eq ∙ p
+
+      fg : section f1 g1
+      fg p =
+        -- g1(p) = f-eq ∙ p
+        -- f1(g1(p)) = subst (λ x → x ≡ b) (f-eq ∙ p) (f-eq ∙ p)
+        {!   !}
 
   -- Then there is a pointed natural equivalence e_f
-  lemmaEqv∙ : Fiber p₁ ≃∙ Ω B∙
+  lemmaEqv∙ : Fiber p1 ≃∙ Ω B∙
   lemmaEqv∙ =
-    Fiber p₁ ≃∙⟨ {!   !} ⟩
-    (f a ≡ b) , f-eq ≃∙⟨ {!   !} ⟩
+    Fiber p1 ≃∙⟨ idEquiv∙ (Fiber p1) ⟩
+    (Σ (fiber f b) λ (a' , p) → a' ≡ a) , ((a , f-eq) , refl) ≃∙⟨ leg1 ⟩
+    (Σ A λ a' → (a' ≡ a) × (f a' ≡ b)) , (a , refl , f-eq) ≃∙⟨ {!  leg2 !} ⟩
+    (f a ≡ b) , f-eq ≃∙⟨ leg3 ⟩
+    (b ≡ b) , refl ≃∙⟨ idEquiv∙ (Ω B∙)  ⟩
     Ω B∙ ∎≃∙
+
+  -- wtf : (f a ≡ b) → (b ≡ b)
+  -- wtf p = subst (λ x → x ≡ b) p p
+
+  -- wtf2 : (f a ≡ b) ≃ (b ≡ b)
+  -- wtf2 = isoToEquiv (iso {! wtf  !} {!   !} {!   !} {!   !})
+
+
+
+    -- Fiber p1 ≃∙⟨ idEquiv∙ (Fiber p1) ⟩
+    -- fiber fst a , (a , f-eq) , refl ≃∙⟨ {!   !} ⟩
+    -- (f a ≡ b) , f-eq ≃∙⟨ {!   !} ⟩
+    -- (b ≡ b) , refl ≃∙⟨ idEquiv∙ (Ω B∙) ⟩
+    -- Ω B∙ ∎≃∙
   -- lemmaEqv∙ .snd = {!   !}
 
 module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
@@ -106,7 +168,7 @@ module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
     _ : ASeq 2 ≡ F
     _ = refl
 
-    _ : ASeq 3 ≡ Fiber (fst , {!  refl !})
+    _ : ASeq 3 ≡ Fiber (fst , refl)
     _ = refl
 
     fSeq : (n : ℕ) → (ASeq (suc n) →∙ ASeq n)
@@ -180,10 +242,10 @@ module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
     gSeq (suc (suc (suc n))) = {!   !}
 
   diagHom : (n : ℕ) → GroupHom (πGr (suc n) Y) (πGr n F)
-  diagHom n = {!  δ .fst !} , {!   !}
+  diagHom n = {!  δ .fst !} , record { pres· = {!   !} ; pres1 = {!   !} ; presinv = {!   !} }
 
   πSeqHom : (n : NFin3) → GroupHom (πSeq (sucNFin3 n)) (πSeq n)
   πSeqHom (n , 0 , p) = πHom n f
   πSeqHom (n , 1 , p) = πHom n p₁
   πSeqHom (n , 2 , p) = diagHom n  
-  πSeqHom (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)
\ No newline at end of file
+  πSeqHom (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)        
\ No newline at end of file
diff --git a/src/ThesisWork/HomotopyGroupLES2.agda b/src/ThesisWork/HomotopyGroupLES2.agda
new file mode 100644
index 0000000..14fe5b9
--- /dev/null
+++ b/src/ThesisWork/HomotopyGroupLES2.agda
@@ -0,0 +1,68 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.HomotopyGroupLES2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Structures.Successor
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order hiding (eq)
+open import Cubical.Data.Fin
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty renaming (rec to ⊥-rec)
+open import Cubical.Homotopy.Loopspace
+
+open import ThesisWork.Exactness
+open import ThesisWork.HomotopyGroupLES2.Lemma415
+open import ThesisWork.HomotopyGroupLES2.Util
+open import ThesisWork.HomotopyGroupLES2.Step1 renaming (A to A')
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ where
+  open SuccStr
+
+  NFin3 : Type ℓ-zero
+  NFin3 = ℕ × Fin 3
+
+  sucNFin3 : NFin3 → NFin3
+  sucNFin3 (n , 0 , _) = n , fsuc fzero
+  sucNFin3 (n , 1 , _) = n , fsuc (fsuc fzero)
+  sucNFin3 (n , 2 , _) = (suc n) , fzero
+  sucNFin3 (n , suc (suc (suc _)) , p) = ⊥-rec (¬m+n<m p)
+
+  NFin3+ : SuccStr ℓ-zero
+  NFin3+ .Index = NFin3
+  NFin3+ .succ = sucNFin3
+
+module _ {ℓ} {X∙ @ (X , x₀) : Pointed ℓ} {Y∙ @ (Y , y₀) : Pointed ℓ} where
+
+  module ΩLES (f∙ @ (f , f-eq) : X∙ →∙ Y∙) where
+    -- Fiber of f
+    F∙ : Pointed ℓ
+    F∙ = fiber f y₀ , x₀ , f-eq
+
+    -- Fix this instance of p1
+    p1 = p₁ {f∙ = f∙}
+    
+    Lift∙ : (ℓ ℓ' : Level) → Pointed ℓ → Pointed (ℓ-max ℓ ℓ')
+    Lift∙ ℓ ℓ' P = (Lift {j = ℓ'} (P .fst)) , lift (P .snd)
+
+    seq : (n* : NFin3) → Pointed ℓ
+    seq (n , 0 , _) = (Ω^ n) Y∙
+    seq (n , 1 , _) = (Ω^ n) X∙
+    seq (n , 2 , _) = ((Ω^ n) F∙)
+    seq (n , suc (suc (suc _)) , p) = ⊥-rec (¬m+n<m p)
+
+    fibfst : (n : ℕ) → (Ω^ n) F∙ →∙ (Ω^ n) X∙
+    fibfst n = Ω^→ n p1
+
+    A : (n : ℕ) → Pointed ℓ
+    A = A' f∙
+
diff --git a/src/ThesisWork/HomotopyGroupLES2/Lemma415.agda b/src/ThesisWork/HomotopyGroupLES2/Lemma415.agda
new file mode 100644
index 0000000..3d1304c
--- /dev/null
+++ b/src/ThesisWork/HomotopyGroupLES2/Lemma415.agda
@@ -0,0 +1,110 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.HomotopyGroupLES2.Lemma415 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Data.Sigma
+
+open import ThesisWork.HomotopyGroupLES2.Util
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ {A∙ @ (A , a₀) : Pointed ℓ} {B∙ @ (B , b₀) : Pointed ℓ} (f∙ @ (f , f₀) : A∙ →∙ B∙) where
+  private
+    p1 : Fiber f∙ →∙ A∙
+    p1 = fst , refl
+
+    leg2 : (Σ (fiber f b₀) λ (a , p) → a ≡ a₀) , ((a₀ , f₀) , refl) ≃∙ (Σ A λ a → (a ≡ a₀) × (f a ≡ b₀)) , (a₀ , refl , f₀)
+    leg2 = isoToEquiv (iso fw gw (λ _ → refl) (λ _ → refl)) , refl where
+      fw : (Σ (fiber f b₀) λ (a , p) → a ≡ a₀) → (Σ A λ a → (a ≡ a₀) × (f a ≡ b₀))
+      fw ((a , p) , q) = a , q , p
+      gw : (Σ A λ a → (a ≡ a₀) × (f a ≡ b₀)) → (Σ (fiber f b₀) λ (a , p) → a ≡ a₀)
+      gw (a , q , p) = (a , p) , q
+
+    -- p : f(a) ≡ b₀
+    -- q : a ≡ a₀
+    --
+    -- ap_f(q) : f(a) ≡ f(a₀)
+    -- sym(ap_f(q)) ∙ p : f(a₀) ≡ b₀
+    -- f₀ : f(a₀) ≡ b₀
+    -- sym(f₀) ∙ sym(ap_f(q)) ∙ p : b₀ ≡ b₀
+
+    leg3 : (Σ A λ a → (a ≡ a₀) × (f a ≡ b₀)) , (a₀ , refl , f₀) ≃∙ (f a₀ ≡ b₀) , f₀
+    leg3 = (isoToEquiv (iso fw gw fg gf)) , eq where
+      P : A → Type ℓ
+      P a = f a ≡ b₀
+      fw : Σ A (λ a → (a ≡ a₀) × (f a ≡ b₀)) → f a₀ ≡ b₀
+      fw (a , p , feq) = subst P p feq
+      gw : f a₀ ≡ b₀ → Σ A (λ a → (a ≡ a₀) × (f a ≡ b₀))
+      gw p = a₀ , refl , p
+      fg : section fw gw
+      fg p = substRefl {B = λ a → f a ≡ b₀} p
+      gf : retract fw gw
+        -- p : f a₀ ≡ b₀
+        -- fw (gw p) ≡ p
+        -- fw (a₀ , refl , p) ≡ p
+        -- subst (λ a' → f a' ≡ b₀) refl p ≡ p
+      test : (feq : f a₀ ≡ b₀) → subst P refl feq ≡ feq
+      test feq = substRefl {B = P} feq
+      module _ (a : A) (p : a ≡ a₀) (feq : f a ≡ b₀) where
+        -- bottomFace : Square (subst P p feq) (subst P refl feq) (λ i → f (p (~ i))) refl
+        -- bottomFace i j = subst {!   !} {!   !} {!   !} {!   !}
+
+        postulate
+          -- TODO: FINISH THIS
+          topFace : Square (λ i → f (p (~ i))) (λ i → b₀) (subst P p feq) feq
+        -- topFace = {!   !}
+
+      gf (a , p , feq) i = p (~ i) , (λ j → p (~ i ∨ j)) , λ j → topFace a p feq j i
+        -- gw (fw (a , p , feq)) ≡ (a , p , feq)
+        -- gw (subst (λ a' → f a' ≡ b₀) p feq) ≡ (a , p , feq)
+        -- (a₀ , refl , p) ≡ (a , p , feq)
+      eq : subst P refl f₀ ≡ f₀
+      eq = substRefl {B = P} f₀
+
+    leg4 : (f a₀ ≡ b₀) , f₀ ≃∙ Ω B∙
+    leg4 = isoToEquiv (iso fw gw fg gf) , eq where
+      fw : f a₀ ≡ b₀ → b₀ ≡ b₀
+      fw p = sym f₀ ∙ p
+      gw : b₀ ≡ b₀ → f a₀ ≡ b₀
+      gw p = f₀ ∙ p
+      fg : section fw gw
+      fg p = assoc (sym f₀) f₀ p ∙ cong (_∙ p) (lCancel f₀) ∙ sym (lUnit p)
+      gf : retract fw gw
+      gf p = assoc f₀ (sym f₀) p ∙ cong (_∙ p) (rCancel f₀) ∙ sym (lUnit p)
+      eq : sym f₀ ∙ f₀ ≡ refl
+      eq = lCancel f₀
+
+  eqv∙ : Fiber p1 ≃∙ Ω B∙
+  eqv∙ =
+    Fiber p1 ≃∙⟨ idEquiv∙ (Fiber p1) ⟩
+    (Σ (fiber f b₀) λ (a , p) → a ≡ a₀) , ((a₀ , f₀) , refl) ≃∙⟨ leg2 ⟩
+    (Σ A λ a → (a ≡ a₀) × (f a ≡ b₀)) , (a₀ , refl , f₀) ≃∙⟨ leg3 ⟩
+    (f a₀ ≡ b₀) , f₀ ≃∙⟨ leg4 ⟩
+    Ω B∙ ∎≃∙
+
+  -Ω : Ω A∙ →∙ Ω B∙ 
+  -Ω = Ω→ f∙ ∘∙ sym∙
+  
+module _ {A∙ @ (A , a₀) : Pointed ℓ} {B∙ @ (B , b₀) : Pointed ℓ} (f∙ @ (f , f₀) : A∙ →∙ B∙) where
+  private
+    p1 : Fiber f∙ →∙ A∙
+    p1 = fst , refl
+
+    q1 : Fiber p1 →∙ Fiber f∙
+    q1 = fst , refl
+
+    r1 : Fiber q1 →∙ Fiber p1
+    r1 = fst , refl
+
+  postulate
+    -- TODO: Finish
+    comm : ≃∙map (eqv∙ f∙) ∘∙ r1 ≡ -Ω f∙ ∘∙ ≃∙map (eqv∙ p1)
+
diff --git a/src/ThesisWork/HomotopyGroupLES2/Step1.agda b/src/ThesisWork/HomotopyGroupLES2/Step1.agda
new file mode 100644
index 0000000..2e9563d
--- /dev/null
+++ b/src/ThesisWork/HomotopyGroupLES2/Step1.agda
@@ -0,0 +1,93 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.HomotopyGroupLES2.Step1 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Equiv
+open import Cubical.Data.Sigma
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Structures.Successor
+open import Cubical.Data.Nat
+
+open import ThesisWork.Exactness
+open import ThesisWork.HomotopyGroupLES2.Util
+open import ThesisWork.HomotopyGroupLES2.Lemma415
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+arrow : (ℓ : Level) → Type (ℓ-suc ℓ)
+arrow ℓ = Σ (Pointed ℓ) (λ X → Σ (Pointed ℓ) (λ Y → X →∙ Y))
+
+F : arrow ℓ → arrow ℓ
+F (X , Y , f) = ((fiber (f .fst) (Y .snd)) , (X .snd , f .snd)) , X , (fst , refl)
+
+F^ : (n : ℕ) → arrow ℓ → arrow ℓ
+F^ zero x = x
+F^ (suc n) x = F (F^ n x)
+
+module _ {X∙ @ (X , x) : Pointed ℓ} {Y∙ @ (Y , y) : Pointed ℓ} (f∙ @ (f , f₀) : X∙ →∙ Y∙) where
+  private
+    p1 : arrow ℓ → Pointed ℓ
+    p1 (X , Y , f) = X
+
+    p2 : arrow ℓ → Pointed ℓ
+    p2 (X , Y , f) = Y
+
+    p3 : (a : arrow ℓ) → (p1 a →∙ p2 a)
+    p3 (X , Y , f) = f
+
+  A : (n : ℕ) → Pointed ℓ
+  A n = p2 (F^ n (X∙ , Y∙ , f∙))
+
+  f^ : (n : ℕ) → A (suc n) →∙ A n
+  f^ n = p3 (F^ n (X∙ , Y∙ , f∙))
+
+  Aⁿ⁺²≡fibfⁿ : (n : ℕ) → A (suc (suc n)) ≡ Fiber (f^ n)
+  Aⁿ⁺²≡fibfⁿ n = refl
+
+  ker→im : (n : ℕ) → (b : fst (A (suc n))) → isInKer∙ (f^ n) b → isInIm∙ (f^ (suc n)) b
+  ker→im n b isInKer = (b , isInKer) , refl
+    -- b is in the kernel of fⁿ means that fⁿ(b) ≡ 0_(Aⁿ)
+    -- we need to prove that there is some (a : Aⁿ⁺²) s.t fⁿ⁺¹(a) ≡ b
+    -- but since Aⁿ⁺² ≡ fiber(fⁿ), then fst(a) : Aⁿ⁺¹ and snd(a) : fⁿ(fst(a)) ≡ 0_(Aⁿ)
+
+  im→ker : (n : ℕ) → (b : fst (A (suc n))) → isInIm∙ (f^ (suc n)) b → isInKer∙ (f^ n) b
+  im→ker n b (a , aIsInIm) = goal where
+    a' : fiber (f^ n .fst) (A n .snd)
+    a' = a
+
+    a'1 : A (suc n) .fst
+    a'1 = fst a'
+
+    a'2 : (f^ n .fst) a'1 ≡ A n .snd
+    a'2 = snd a'
+
+    a'IsInIm : (f^ (suc n) .fst) a' ≡ b
+    a'IsInIm = aIsInIm
+
+    goal : (f^ n .fst) b ≡ A n .snd
+    goal = subst (λ p → (f^ n .fst) p ≡ A n .snd) a'IsInIm a'2
+
+    -- b isInIm means that there exists some (a : Aⁿ⁺²) s.t fⁿ⁺¹(a) ≡ b
+    -- we need to prove that fⁿ(b) ≡ 0_(Aⁿ)
+    -- but since Aⁿ⁺² ≡ fiber(fⁿ), fst(a) : Aⁿ⁺¹ and snd(a) : fⁿ(fst(a)) ≡ 0_(Aⁿ)
+    -- so we just need to substitute some fst(a) ≡ b into snd(a)
+
+  AⁿisExact : (n : ℕ) → isExactAt∙ (f^ (suc n)) (f^ n)
+  AⁿisExact n b = (ker→im n b) , (im→ker n b)
+
+  open ExactSequence∙
+  ASeq : ExactSequence∙ ℕ+
+  ASeq .seq = A
+  ASeq .fun = f^
+  ASeq .exactness = AⁿisExact
+
+  eqvf : (A 3) ≃∙ (Ω Y∙)
+  eqvf = eqv∙ f∙
+
+  -- Diagonal map 
+  δ : Ω Y∙ →∙ Fiber f∙
+  δ = p₁ ∘∙ ≃∙map (invEquiv∙ eqvf)
\ No newline at end of file
diff --git a/src/ThesisWork/HomotopyGroupLES2/Step2.agda b/src/ThesisWork/HomotopyGroupLES2/Step2.agda
new file mode 100644
index 0000000..a928907
--- /dev/null
+++ b/src/ThesisWork/HomotopyGroupLES2/Step2.agda
@@ -0,0 +1,64 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.HomotopyGroupLES2.Step2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Data.Sigma
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Data.Nat
+open import Cubical.Structures.Successor
+
+open import ThesisWork.Exactness
+open import ThesisWork.HomotopyGroupLES2.Util
+open import ThesisWork.HomotopyGroupLES2.Step1
+open import ThesisWork.HomotopyGroupLES2.Lemma415
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+pattern 3+ n = suc (suc (suc n))
+
+module _ {X∙ @ (X , x) : Pointed ℓ} {Y∙ @ (Y , y) : Pointed ℓ} (f∙ @ (f , f₀) : X∙ →∙ Y∙) where
+  F∙ = Fiber f∙
+
+  B : (n : ℕ) → Pointed ℓ
+  B 0 = Y∙
+  B 1 = X∙
+  B 2 = F∙
+  B (3+ n) = Ω (B n)
+
+  g^ : (n : ℕ) → B (suc n) →∙ B n
+  g^ 0 = f∙
+  g^ 1 = p₁
+  g^ 2 = δ f∙
+  g^ (3+ n) = -Ω (g^ n)
+
+  _ : A f∙ 3 ≡ B 3
+  _ = ua∙ (eqv∙ f∙ .fst) (eqv∙ f∙ .snd)
+
+  module Lemma416 where
+    η : (n : ℕ) → A f∙ 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) ⟩
+      Ω (B n) ∎≃∙
+
+    eqvfg : (n : ℕ) → (≃∙map (η n) ∘∙ f^ f∙ n) ∙∼ (g^ n ∘∙ ≃∙map (η (suc n)))
+    eqvfg 0 = {!   !}
+    eqvfg 1 = {!   !}
+    eqvfg 2 = {!   !}
+    eqvfg (3+ n) = {!   !}
+
+
+  open ExactSequence∙
+  BSeq : ExactSequence∙ ℕ+
+  BSeq .seq = B
+  BSeq .fun = g^
+  BSeq .exactness = {!   !}
\ No newline at end of file
diff --git a/src/ThesisWork/HomotopyGroupLES2/Step3.agda b/src/ThesisWork/HomotopyGroupLES2/Step3.agda
new file mode 100644
index 0000000..8009ac6
--- /dev/null
+++ b/src/ThesisWork/HomotopyGroupLES2/Step3.agda
@@ -0,0 +1,3 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.HomotopyGroupLES2.Step3 where
diff --git a/src/ThesisWork/HomotopyGroupLES2/Util.agda b/src/ThesisWork/HomotopyGroupLES2/Util.agda
new file mode 100644
index 0000000..1f4b418
--- /dev/null
+++ b/src/ThesisWork/HomotopyGroupLES2/Util.agda
@@ -0,0 +1,29 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.HomotopyGroupLES2.Util where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Equiv
+open import Cubical.Homotopy.Loopspace
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+-- Pointed fiber
+Fiber : {X∙ Y∙ : Pointed ℓ} → (f∙ @ (f , f-eq) : X∙ →∙ Y∙) → Pointed ℓ
+Fiber {X∙ = X∙} {Y∙ = Y∙} f∙ @ (f , f-eq) = (fiber f (Y∙ .snd)) , X∙ .snd , f-eq
+
+-- General definition of p₁ as the first projection
+p₁ : {A∙ B∙ : Pointed ℓ} {f∙ : A∙ →∙ B∙} → Fiber f∙ →∙ A∙
+p₁ = fst , refl
+
+sym∙ : {A∙ @ (A , a) : Pointed ℓ} → (Ω A∙) →∙ (Ω A∙)
+sym∙ = sym , refl
+
+Lift∙ : {i j : Level} → Pointed i → Pointed (ℓ-max i j)
+Lift∙ {i = i} {j = j} P = (Lift {j = j} (P .fst)) , lift (P .snd)
+
+cong-≃∙ : ∀ {ℓ ℓ'} → {A∙ B∙ : Pointed ℓ} → (f : Pointed ℓ → Pointed ℓ') → (p : A∙ ≃∙ B∙) → f A∙ ≃∙ f B∙
+cong-≃∙ {ℓ = ℓ} {ℓ' = ℓ'} {B∙ = B∙} f p = Equiv∙J (λ T∙ T≃∙B → f T∙ ≃∙ f B∙) (idEquiv∙ (f B∙)) p
\ No newline at end of file
diff --git a/type-theory.agda-lib b/type-theory.agda-lib
index 9ad3605..205f29b 100644
--- a/type-theory.agda-lib
+++ b/type-theory.agda-lib
@@ -1,2 +1,2 @@
-include: src src/ThesisWork src/AOP talks
+include: src src/AOP talks
 depend: standard-library cubical