Define spectra

Cubical/Data/Unit/Pointed.agda

@@ -0,0 +1,14 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Unit.Pointed where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed.Base
+
+open import Cubical.Data.Unit
+
+private
+  variable
+    ℓ : Level
+
+Unit∙ : Pointed ℓ
+Unit∙ = Unit* , tt*

Cubical/HITs/Susp/Base.agda

@@ -16,16 +16,20 @@ open import Cubical.HITs.S3
 
 open Iso
 
-data Susp {ℓ} (A : Type ℓ) : Type ℓ where
+private
+  variable
+    ℓ ℓ′ : Level
+
+data Susp (A : Type ℓ) : Type ℓ where
   north : Susp A
   south : Susp A
   merid : (a : A) → north ≡ south
 
-∙Susp : ∀ {ℓ} (A : Type ℓ) → Pointed ℓ
-∙Susp A = Susp A , north
+Susp∙ : (A : Type ℓ) → Pointed ℓ
+Susp∙ A = Susp A , north
 
 -- induced function
-suspFun : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B)
+suspFun : {A : Type ℓ} {B : Type ℓ′} (f : A → B)
        → Susp A → Susp B
 suspFun f north = north
 suspFun f south = south

Cubical/Homotopy/Freudenthal.agda

@@ -26,7 +26,7 @@ open import Cubical.Foundations.Equiv.HalfAdjoint
 
 module _ {ℓ} (n : HLevel) {A : Pointed ℓ} (connA : isConnected (suc (suc n)) (typ A)) where
 
-  σ : typ A → typ (Ω (∙Susp (typ A)))
+  σ : typ A → typ (Ω (Susp∙ (typ A)))
   σ a = merid a ∙ merid (pt A) ⁻¹
 
   private

Cubical/Homotopy/Prespectrum.agda

@@ -0,0 +1,54 @@
+{-# OPTIONS --safe #-}
+{-
+  This uses ideas from Floris van Doorn's phd thesis and the code in
+  https://github.com/cmu-phil/Spectral/blob/master/spectrum/basic.hlean
+-}
+module Cubical.Homotopy.Prespectrum where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Pointed
+open import Cubical.Data.Unit.Pointed
+
+open import Cubical.Structures.Successor
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Int
+
+open import Cubical.HITs.Susp
+
+open import Cubical.Homotopy.Loopspace
+
+private
+  variable
+    ℓ ℓ′ : Level
+
+record GenericPrespectrum (S : SuccStr ℓ) (ℓ′ : Level) : Type (ℓ-max (ℓ-suc ℓ′) ℓ) where
+  open SuccStr S
+  field
+    space : Index → Pointed ℓ′
+    map : (i : Index) → (space i →∙ Ω (space (succ i)))
+
+Prespectrum = GenericPrespectrum ℤ+
+
+Unit∙→ΩUnit∙ : {ℓ : Level} → (Unit∙ {ℓ = ℓ}) →∙ Ω (Unit∙ {ℓ = ℓ})
+Unit∙→ΩUnit∙ = (λ {tt* → refl}) , refl
+
+makeℤPrespectrum : (space : ℕ → Pointed ℓ)
+                  (map : (i : ℕ) → (space i) →∙ Ω (space (suc i)))
+                → Prespectrum ℓ
+GenericPrespectrum.space (makeℤPrespectrum space map) (pos n) = space n
+GenericPrespectrum.space (makeℤPrespectrum space map) (negsuc n) = Unit∙
+GenericPrespectrum.map (makeℤPrespectrum space map) (pos n) = map n
+GenericPrespectrum.map (makeℤPrespectrum space map) (negsuc zero) = (λ {tt* → refl}) , refl
+GenericPrespectrum.map (makeℤPrespectrum space map) (negsuc (suc n)) = Unit∙→ΩUnit∙
+
+SuspensionPrespectrum : Pointed ℓ → Prespectrum ℓ
+SuspensionPrespectrum A = makeℤPrespectrum space map
+          where
+            space : ℕ → Pointed _
+            space zero = A
+            space (suc n) = Susp∙ (typ (space n))
+
+            map : (n : ℕ) → _
+            map n = (λ a → merid a ∙ merid (pt (space n)) ⁻¹) , rCancel (merid (pt (space n)))

Cubical/Homotopy/Spectrum.agda

@@ -0,0 +1,22 @@
+{-# OPTIONS --safe #-}
+{-
+  This uses ideas from Floris van Doorn's phd thesis and the code in
+  https://github.com/cmu-phil/Spectral/blob/master/spectrum/basic.hlean
+-}
+module Cubical.Homotopy.Spectrum where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Unit.Pointed
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Int
+
+open import Cubical.Homotopy.Prespectrum
+
+private
+  variable
+    ℓ : Level
+
+Spectrum : (ℓ : Level) → Type (ℓ-suc ℓ)
+Spectrum ℓ = let open GenericPrespectrum
+             in Σ[ P ∈ Prespectrum ℓ ] ((k : ℤ) → isEquiv (fst (map P k)))

Cubical/Structures/Successor.agda

@@ -0,0 +1,29 @@
+{-# OPTIONS --safe #-}
+{-
+  Successor structures for spectra, chain complexes and fiber sequences.
+  This is an idea from Floris van Doorn's phd thesis.
+-}
+module Cubical.Structures.Successor where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Int
+open import Cubical.Data.Nat
+
+private
+  variable
+    ℓ : Level
+
+record SuccStr (ℓ : Level) : Type (ℓ-suc ℓ) where
+  field
+    Index : Type ℓ
+    succ : Index → Index
+
+open SuccStr
+
+ℤ+ : SuccStr ℓ-zero
+ℤ+ .Index = ℤ
+ℤ+ .succ = sucℤ
+
+ℕ+ : SuccStr ℓ-zero
+ℕ+ .Index = ℕ
+ℕ+ .succ = suc