wip lemma 4.1.5

src/ThesisWork/Pi3S2/ChainComplex.agda

@@ -2,10 +2,9 @@
 
 {-# OPTIONS --cubical #-}
 
-module ThesisWork.ChainComplex where
+module ThesisWork.Pi3S2.ChainComplex where
 
 open import Cubical.Foundations.Prelude
 open import Agda.Primitive
 
-SuccStr : ∀ {l} → Type (lsuc l)
-SuccStr {l} = Σ (Type l) (λ carrier → carrier → carrier)
+data ChainComplex : Type where

src/ThesisWork/Pi3S2/LES.agda

@@ -1,6 +1,6 @@
 {-# OPTIONS --cubical #-}
 
-module ThesisWork.LES where
+module ThesisWork.Pi3S2.LES where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Pointed

src/ThesisWork/Pi3S2/Lemma4-1-5.agda

@@ -0,0 +1,36 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Pi3S2.Lemma4-1-5 where
+
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Homotopy.Loopspace
+
+fiberF : {l : Level} {A∙ B∙ : Pointed l} → (f : A∙ →∙ B∙) → Pointed l
+fiberF {A∙ = A∙ @ (A , a)} {B∙ = B∙ @ (B , b)} f = fiber (fst f) b , a , (snd f)
+
+lemma : ∀ {l : Level} {A∙ @ (A , a) B∙ @ (B , b) : Pointed l}
+  → (f : A∙ →∙ B∙)
+  → let
+      p₁ : fiberF f →∙ A∙
+      p₁ = fst , refl
+    in fiberF p₁ ≃∙ (Ω B∙)
+lemma {A∙ = A∙ @ (A , a0)} {B∙ = B∙ @ (B , b0)} f∙ @ (f , f-eq) = eqv , {!   !} where
+  eqv : fst (fiberF ((λ r → fst r) , refl)) ≃ fst (Ω B∙)
+  eqv =
+      fst (fiberF ((λ r → fst r) , refl))
+    ≃⟨ {!   !} ⟩
+      Σ (fst (fiberF f∙)) (λ fibf @ (a , p) → a ≡ a0)
+    ≃⟨ {!   !} ⟩
+      Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
+    ≃⟨ {!   !} ⟩
+      f a0 ≡ b0
+    ≃⟨ {!   !} ⟩
+      b0 ≡ b0
+    ≃⟨ idEquiv (b0 ≡ b0) ⟩
+      fst (Ω B∙)
+    ■

src/ThesisWork/Pi3S2/SuccStr.agda

@@ -0,0 +1,24 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Pi3S2.SuccStr where
+
+open import Cubical.Foundations.Prelude
+open import Data.Nat
+
+SuccStr : (I : Type) (S : I → I) → (i : I) → (n : ℕ) → I
+SuccStr I S i zero = i 
+SuccStr I S i (suc n) = S (SuccStr I S i n)
+
+-- Examples of successor structures:
+
+module _ where
+  -- (ℕ , λ n . n + 1)
+  ℕ-SuccStr : (i : ℕ) → (n : ℕ) → ℕ
+  ℕ-SuccStr = SuccStr ℕ suc
+
+module _ where
+  open import Data.Integer renaming (suc to zsuc)
+
+  -- (ℤ , λ n . n + 1)
+  ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ
+  ℤ-SuccStr = SuccStr ℤ zsuc

src/ThesisWork/README.md

@@ -0,0 +1,3 @@
+# Notes
+
+- Already some existing work by Felix Cherubini (@felixwellen) about spectra here: https://github.com/agda/cubical/pull/723