spectra

src/ThesisWork/Pi3S2/SuccStr.agda

@@ -3,47 +3,77 @@
 module ThesisWork.Pi3S2.SuccStr where
 
 open import Cubical.Foundations.Prelude
-open import Data.Nat using (ℕ ; zero ; suc)
 
-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)
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
 
--- Examples of successor structures:
+-- An indexing parameter that has only the successor operation
+-- Can be used to index into sequences
+-- Defined in FVD 4.1.2.
+record SuccStr (ℓ : Level) : Type (ℓ-suc ℓ) where
+  field
+    A : Type ℓ
+    suc : A → A
+
+module _ {S : SuccStr ℓ} where
+  open import Cubical.Data.Nat renaming (suc to nsuc)
+  open SuccStr S
+  _+ˢ_ : (i : A) → (n : ℕ) → A
+  i +ˢ zero = i
+  i +ˢ nsuc n = suc (i +ˢ n)
 
 module _ where
-  -- (ℕ , λ n . n + 1)
-  ℕ-SuccStr : (i : ℕ) → (n : ℕ) → ℕ
-  ℕ-SuccStr = SuccStr ℕ suc
+  open import Cubical.Data.Int
+  open SuccStr
+  ℤ-SuccStr : SuccStr ℓ-zero
+  ℤ-SuccStr .A = ℤ
+  ℤ-SuccStr .suc = sucℤ
 
-module _ where
-  open import Data.Integer using (ℤ) renaming (suc to zsuc)
+-- OLD: This doesn't work because we don't want the type of SuccStr to be
+-- parameterized by the base type of the structure; instead, we want it to be
+-- contained within the structure and have the structure expose a uniform
+-- type
 
-  -- (ℤ , λ n . n + 1)
-  ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ
-  ℤ-SuccStr = SuccStr ℤ zsuc
+-- 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)
 
-module _ where
-  open import Data.Fin
-  open import Data.Product
+-- -- Examples of successor structures:
 
-  inc-k-inv : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
-  inc-k-inv {k} (n , zero) = (suc n) , opposite zero
-  inc-k-inv {k} (n , suc k1) = n , inject₁ k1
+-- module _ where
+--   -- (ℕ , λ n . n + 1)
+--   ℕ-SuccStr : (i : ℕ) → (n : ℕ) → ℕ
+--   ℕ-SuccStr = SuccStr ℕ suc
 
-  inc : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
-  inc {k} (n , k1) =
-    let result = inc-k-inv (n , opposite k1) in
-    (fst result) , opposite (snd result)
+-- module _ where
+--   open import Data.Integer using (ℤ) renaming (suc to zsuc)
 
-  _ : inc {k = 3} (5 , fromℕ 2) ≡ (6 , zero)
-  _ = refl
+--   -- (ℤ , λ n . n + 1)
+--   ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ
+--   ℤ-SuccStr = SuccStr ℤ zsuc
 
-  -- _ : inc {k = 3} (5 , inject₁ (fromℕ 1)) ≡ (6 , zero)
-  -- _ = {!  refl !}
+-- module _ where
+--   open import Data.Fin
+--   open import Data.Product
 
-  _ : inc {k = 5} (5 , fromℕ 4) ≡ (6 , zero)
-  _ = refl
+--   inc-k-inv : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
+--   inc-k-inv {k} (n , zero) = (suc n) , opposite zero
+--   inc-k-inv {k} (n , suc k1) = n , inject₁ k1
 
-  ℕ-k-SuccStr : (k : ℕ) → (ℕ × Fin k) → ℕ → (ℕ × Fin k)
-  ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc
+--   inc : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
+--   inc {k} (n , k1) =
+--     let result = inc-k-inv (n , opposite k1) in
+--     (fst result) , opposite (snd result)
+
+--   _ : inc {k = 3} (5 , fromℕ 2) ≡ (6 , zero)
+--   _ = refl
+
+--   -- _ : inc {k = 3} (5 , inject₁ (fromℕ 1)) ≡ (6 , zero)
+--   -- _ = {!  refl !}
+
+--   _ : inc {k = 5} (5 , fromℕ 4) ≡ (6 , zero)
+--   _ = refl
+
+--   ℕ-k-SuccStr : (k : ℕ) → (ℕ × Fin k) → ℕ → (ℕ × Fin k)
+--   ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc

src/ThesisWork/Spectrum.agda

@@ -1,3 +1,47 @@
 {-# OPTIONS --cubical #-}
 
 module ThesisWork.Spectrum where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Equiv
+open import Cubical.Data.Sigma
+open import Cubical.Homotopy.Loopspace
+open import ThesisWork.Pi3S2.SuccStr
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+-- A prespectrum is a pair consisting of a sequence of pointed types
+-- (Y : Z → U∗) and a sequence of pointed maps e: (n : Z) → Yₙ →∗ ΩYₙ₊₁.
+-- We will give a definition in terms of a successor structure tho.
+record Prespectrum (N : SuccStr ℓ) : Type (ℓ-suc ℓ) where
+  open SuccStr N
+  field
+    Y : A → Pointed ℓ
+    e : (n : A) → Y n →∙ Ω (Y (suc n))
+
+ℤ-Prespectrum : Type (ℓ-suc ℓ-zero)
+ℤ-Prespectrum = Prespectrum ℤ-SuccStr
+
+isPointedEquiv : {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) → Type (ℓ-max ℓ ℓ')
+isPointedEquiv {A = A} {B = B} f = isEquiv (f .fst) × (f .fst (A .snd) ≡ B .snd)
+
+isPtEquivToPtEquiv : {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) → isPointedEquiv f → A ≃∙ B
+isPtEquivToPtEquiv f (fEqv , fPt) = (f .fst , fEqv) , fPt
+
+-- An Ω-spectrum or spectrum is a prespectrum (Y, e) where eₙ is a
+-- pointed equivalence for all n.
+record IsSpectrum {N : SuccStr ℓ} (P : Prespectrum N) : Type ℓ where
+  open Prespectrum P
+  open SuccStr N
+  field
+    eIsEquiv : ∀ (n : A) → isPointedEquiv (e n)
+
+Spectrum : SuccStr ℓ → Type (ℓ-suc ℓ)
+Spectrum {ℓ = ℓ} N = Σ (Prespectrum N) IsSpectrum
+
+ℤ-Spectrum : Type (ℓ-suc ℓ-zero)
+ℤ-Spectrum = Spectrum ℤ-SuccStr