sequence

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.Univalence
 open import Cubical.HITs.TypeQuotients
 open import Cubical.Foundations.Structure
 open import Cubical.Data.Sigma
@@ -51,16 +52,23 @@ Fiber {A = A , a} {B = B , b} (f , feq) = (fiber f b) , a , feq
 
 -- Lemma 4.1.5 in FVD thesis
 -- Suppose given a pointed map f : A →∗ B
-module _ {A B : Pointed ℓ} (f : A →∙ B) where
+module _ {A∙ @ (A , a) B∙ @ (B , b) : Pointed ℓ} (f∙ @ (f , f-eq) : A∙ →∙ B∙) where
   private
     -- Let p1 : fib_f →∗ A be the first projection. 
-    p₁ : Fiber f →∙ A
+    p₁ : Fiber f∙ →∙ A∙
     p₁ = fst , refl
 
+    lol : (f∙ .fst a ≡ b) , f-eq ≃∙ (b ≡ b) , (λ i → b)
+    lol .fst = pathToEquiv (cong (λ z → z ≡ b) f-eq)
+    lol .snd i j = {!   !}
+
   -- Then there is a pointed natural equivalence e_f
-  lemmaEqv : Fiber p₁ ≃∙ Ω B
-  lemmaEqv .fst = {!   !}
-  lemmaEqv .snd = {!   !}
+  lemmaEqv∙ : Fiber p₁ ≃∙ Ω B∙
+  lemmaEqv∙ =
+    Fiber p₁ ≃∙⟨ {!   !} ⟩
+    (f a ≡ b) , f-eq ≃∙⟨ {!   !} ⟩
+    Ω B∙ ∎≃∙
+  -- lemmaEqv∙ .snd = {!   !}
 
 module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
   private
@@ -81,20 +89,31 @@ module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
   module Step1 where
     arrow* = Σ (Pointed ℓ) λ X → Σ (Pointed ℓ) λ Y → X →∙ Y
 
-    private
-      F' : arrow* → arrow*
-      F' (X , Y , f) = Fiber f , X , fst , refl
+    F' : arrow* → arrow*
+    F' (X , Y , f) = Fiber f , X , fst , refl
 
-      F'^ : (n : ℕ) → arrow* → arrow*
-      F'^ zero a = a
-      F'^ (suc n) a = F' (F'^ n a)
+    F'^ : (n : ℕ) → arrow* → arrow*
+    F'^ zero a = a
+    F'^ (suc n) a = F' (F'^ n a)
 
-      -- Given a pointed map f : X →∗ Y, we define its fiber sequence
-      ASeq : ℕ → Pointed ℓ
-      ASeq n = (F'^ n (X , Y , f)) .snd .fst
+    -- Given a pointed map f : X →∗ Y, we define its fiber sequence
+    ASeq : ℕ → Pointed ℓ
+    ASeq n = (F'^ n (X , Y , f)) .snd .fst
 
-      fSeq : (n : ℕ) → (ASeq (suc n) →∙ ASeq n)
-      fSeq n = (F'^ n (X , Y , f)) .snd .snd
+    _ : ASeq 0 ≡ Y
+    _ = refl
+
+    _ : ASeq 1 ≡ X
+    _ = refl
+
+    _ : ASeq 2 ≡ F
+    _ = refl
+
+    _ : ASeq 3 ≡ Fiber (fst , {!  refl !})
+    _ = refl
+
+    fSeq : (n : ℕ) → (ASeq (suc n) →∙ ASeq n)
+    fSeq n = (F'^ n (X , Y , f)) .snd .snd
 
     module _ where
       open ExactSequence∙
@@ -136,13 +155,38 @@ module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
           cong (fSeq n .fst) (sym (p .snd)) ∙ p .fst .snd
 
     -- δ : ΩY → F
+    -- This is the diagonal arrow
     δ : Ω Y →∙ F
-    δ = {!   !} ∘∙ {! e⁻¹ .fst  !} where
-      e = lemmaEqv f
-      e⁻¹ = invEquiv∙ e
+    δ = p₁′ ∘∙ ≃∙map (invEquiv∙ e) where
+      e : ASeq 3 ≃∙ Ω Y
+      e = lemmaEqv∙ f
+
+      p₁′ : ASeq 3 →∙ F
+      p₁′ = fst , refl
+
+  open Step1 using (δ)
+
+  module Step2 where
+    BSeq : ℕ → Pointed ℓ
+    BSeq 0 = Y
+    BSeq 1 = X
+    BSeq 2 = Fiber f
+    BSeq (suc (suc (suc n))) = Ω (BSeq (suc (suc n)))
+
+    _ : Step1.ASeq 3 ≡ BSeq 3
+    _ = {!  refl !}
+
+    gSeq : (n : ℕ) → BSeq (suc n) →∙ BSeq n
+    gSeq 0 = f
+    gSeq 1 = p₁
+    gSeq 2 = {! δ !}
+    gSeq (suc (suc (suc n))) = {!   !}
+
+  diagHom : (n : ℕ) → GroupHom (πGr (suc n) Y) (πGr n F)
+  diagHom n = {!  δ .fst !} , {!   !}
 
   π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) = {! πHom  !}  
-  πSeqHom (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)   
+  πSeqHom (n , 2 , p) = diagHom n  
+  πSeqHom (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)

src/ThesisWork/Sequence.agda

@@ -0,0 +1,29 @@
+{-# OPTIONS --cubical #-}
+
+-- Trying to do a generic sequence structure?
+
+module ThesisWork.Sequence where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Structures.Successor
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ {ℓN : Level} (N : SuccStr ℓN) where
+  open SuccStr N
+
+  Sequence : ∀ {ℓ : Level} → (A : Index → Type ℓ) → Type (ℓ-max ℓ ℓN)
+  Sequence A = (n : Index) → A n
+
+  record IsChainComplex {ℓS N : Level}
+      (S : Sequence (λ _ → Pointed ℓS))
+      (F : Sequence (λ n → S (succ n) →∙ S n))
+    : Type (ℓ-max ℓN ℓS) where
+    field
+      property : (n : Index) → 
+        let Tₙ₊₂ = S (succ (succ n)) in let Tₙ₊₁ = S (succ n) in let Tₙ = S n in
+        let dₙ₊₁ = F (succ n) in let dₙ = F n in
+        (dₙ ∘∙ dₙ₊₁) ≡ const∙ Tₙ₊₂ Tₙ