Merge pull request #589 from felixwellen/define-spectra

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/Sn/Base.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --safe #-}
 module Cubical.HITs.Sn.Base where
 
-open import Cubical.HITs.Susp
+open import Cubical.HITs.Susp.Base
 open import Cubical.Foundations.Pointed
 open import Cubical.Data.Nat
 open import Cubical.Data.NatMinusOne

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/HITs/Susp/Properties.agda

@@ -6,11 +6,19 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Path
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.GroupoidLaws
+
+open import Cubical.Homotopy.Loopspace
 
 open import Cubical.Data.Bool
 open import Cubical.HITs.Join
 open import Cubical.HITs.Susp.Base
 
+private
+  variable
+    ℓ : Level
+
 open Iso
 
 Susp-iso-joinBool : ∀ {ℓ} {A : Type ℓ} → Iso (Susp A) (join A Bool)
@@ -117,3 +125,9 @@ Iso.rightInv funSpaceSuspIso f = funExt λ {north → refl
                                              ; south → refl
                                              ; (merid a i) → refl}
 Iso.leftInv funSpaceSuspIso _ = refl
+
+toSusp : (A : Pointed ℓ) → typ A → typ (Ω (Susp∙ (typ A)))
+toSusp A a = merid a ∙ merid (pt A) ⁻¹
+
+toSuspPointed : (A : Pointed ℓ) → A →∙ Ω (Susp∙ (typ A))
+toSuspPointed A = (λ a → merid a ∙ merid (pt A) ⁻¹) , rCancel (merid (pt A))

Cubical/HITs/Truncation/FromNegTwo/Properties.agda

@@ -18,7 +18,7 @@ open import Cubical.Data.Nat hiding (elim)
 open import Cubical.Data.NatMinusOne as ℕ₋₁
 open import Cubical.Data.Sigma
 open import Cubical.HITs.Sn.Base
-open import Cubical.HITs.Susp
+open import Cubical.HITs.Susp.Base
 open import Cubical.HITs.Nullification as Null hiding (rec; elim)
 
 open import Cubical.HITs.Truncation.FromNegTwo.Base

Cubical/HITs/Truncation/Properties.agda

@@ -23,7 +23,7 @@ open import Cubical.Data.Bool
 open import Cubical.Data.Unit
 open import Cubical.HITs.Sn.Base
 open import Cubical.HITs.S1
-open import Cubical.HITs.Susp
+open import Cubical.HITs.Susp.Base
 open import Cubical.HITs.Nullification as Null hiding (rec; elim)
 
 open import Cubical.HITs.PropositionalTruncation as PropTrunc

Cubical/Homotopy/Freudenthal.agda

@@ -11,7 +11,7 @@ open import Cubical.Foundations.Everything
 open import Cubical.Data.Nat
 open import Cubical.Data.Sigma
 open import Cubical.HITs.Nullification
-open import Cubical.HITs.Susp
+open import Cubical.HITs.Susp renaming (toSusp to σ)
 open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec ; elim to trElim)
 open import Cubical.Homotopy.Connected
 open import Cubical.Homotopy.WedgeConnectivity
@@ -26,16 +26,13 @@ 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)))
-  σ a = merid a ∙ merid (pt A) ⁻¹
-
   private
     2n+2 = suc n + suc n
 
     module WC (p : north ≡ north) =
       WedgeConnectivity (suc n) (suc n) A connA A connA
         (λ a b →
-          ( (σ b ≡ p → hLevelTrunc 2n+2 (fiber (λ x → merid x ∙ merid a ⁻¹) p))
+          ( (σ A b ≡ p → hLevelTrunc 2n+2 (fiber (λ x → merid x ∙ merid a ⁻¹) p))
           , isOfHLevelΠ 2n+2 λ _ → isOfHLevelTrunc 2n+2
           ))
         (λ a r → ∣ a , (rCancel' (merid a) ∙ rCancel' (merid (pt A)) ⁻¹) ∙ r ∣)
@@ -46,7 +43,7 @@ module _ {ℓ} (n : HLevel) {A : Pointed ℓ} (connA : isConnected (suc (suc n))
               ∙ lUnit r ⁻¹))
 
     fwd : (p : north ≡ north) (a : typ A)
-      → hLevelTrunc 2n+2 (fiber σ p)
+      → hLevelTrunc 2n+2 (fiber (σ A) p)
       → hLevelTrunc 2n+2 (fiber (λ x → merid x ∙ merid a ⁻¹) p)
     fwd p a = Trunc.rec (isOfHLevelTrunc 2n+2) (uncurry (WC.extension p a))
 
@@ -78,7 +75,7 @@ module _ {ℓ} (n : HLevel) {A : Pointed ℓ} (connA : isConnected (suc (suc n))
     interpolate a i x j = compPath-filler (merid x) (merid a ⁻¹) (~ i) j
 
   Code : (y : Susp (typ A)) → north ≡ y → Type ℓ
-  Code north p = hLevelTrunc 2n+2 (fiber σ p)
+  Code north p = hLevelTrunc 2n+2 (fiber (σ A) p)
   Code south q = hLevelTrunc 2n+2 (fiber merid q)
   Code (merid a i) p =
     Glue
@@ -114,7 +111,7 @@ module _ {ℓ} (n : HLevel) {A : Pointed ℓ} (connA : isConnected (suc (suc n))
   isConnectedMerid : isConnectedFun 2n+2 (merid {A = typ A})
   isConnectedMerid p = encode south p , contractCodeSouth p
 
-  isConnectedσ : isConnectedFun 2n+2 σ
+  isConnectedσ : isConnectedFun 2n+2 (σ A)
   isConnectedσ =
     transport (λ i → isConnectedFun 2n+2 (interpolate (pt A) (~ i))) isConnectedMerid
 
@@ -129,10 +126,10 @@ FreudenthalEquiv : ∀ {ℓ} (n : HLevel) (A : Pointed ℓ)
                 → hLevelTrunc ((suc n) + (suc n)) (typ A)
                  ≃ hLevelTrunc ((suc n) + (suc n)) (typ (Ω (Susp (typ A) , north)))
 FreudenthalEquiv n A iscon = connectedTruncEquiv _
-                                                 (σ n {A = A} iscon)
+                                                 (σ A)
                                                  (isConnectedσ _ iscon)
 FreudenthalIso : ∀ {ℓ} (n : HLevel) (A : Pointed ℓ)
                 → isConnected (2 + n) (typ A)
                 → Iso (hLevelTrunc ((suc n) + (suc n)) (typ A))
                       (hLevelTrunc ((suc n) + (suc n)) (typ (Ω (Susp (typ A) , north))))
-FreudenthalIso n A iscon = connectedTruncIso _ (σ n {A = A} iscon) (isConnectedσ _ iscon)
+FreudenthalIso n A iscon = connectedTruncIso _ (σ A) (isConnectedσ _ iscon)

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 = toSuspPointed (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