eilenberg maclane spaces forms a spectrum

src/ThesisWork/Cohomology.agda

@@ -4,7 +4,55 @@ module ThesisWork.Cohomology where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Homotopy.Loopspace
 open import Cubical.Algebra.AbGroup
+open import Cubical.Algebra.Group
+open import Cubical.HITs.SetTruncation as ST
+open import Cubical.HITs.Sn
+open import Cubical.HITs.Susp
+open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Data.Nat
+open import Cubical.Foundations.Equiv
 
-Cohomology : ∀ {l} → (X : Pointed l) → AbGroup l
-Cohomology = {!   !}
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+-- nth Unreduced cohomology
+UnreducedCohomology : (n : ℕ) → (X : Type ℓ) → (G : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
+UnreducedCohomology n X G = ∥ (X → EM G n) ∥₂
+
+-- nth Reduced cohomology
+ReducedCohomology : (n : ℕ) → (X : Pointed ℓ) → (G : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
+ReducedCohomology n X G = ∥ X →∙ EM∙ G n ∥₂
+
+-- Examples
+module Examples where
+  -- Theorem 4.1.7 in JHY thesis
+  module UnitCohomology (k : ℕ) where
+    open import Cubical.Data.Unit
+    open import Cubical.Data.Int
+    open import Cubical.Algebra.AbGroup.Instances.Int
+
+    Unit∙ : Pointed₀
+    Unit∙ = Unit , tt
+
+    Lift∙ : ∀ {ℓ} → Pointed₀ → Pointed ℓ
+    Lift∙ (T , t) = (Lift T) , lift t
+
+    module _ {B : Pointed₀} {n : ℕ} where
+      lemma1 : ∀ {n : ℕ} →
+            (S₊∙ (suc n) →∙ (Ω^ n) B ∙)
+        ≃∙  (S₊∙ n →∙ (Ω^ (suc n)) B ∙)
+      lemma1 {n} =
+        (S₊∙ (suc n) →∙ (Ω^ n) B ∙) ≃∙⟨ {!   !} ⟩
+        (Susp∙ (S₊ n) →∙ (Ω^ n) B ∙) ≃∙⟨ invEquiv (isoToEquiv ΩSuspAdjointIso) , {!   !} ⟩
+        (S₊∙ n →∙ Ω ((Ω^ n) B) ∙) ≃∙⟨ {! idEquiv∙  !} ⟩
+        (S₊∙ n →∙ (Ω^ (suc n)) B ∙) ∎≃∙
+
+      lemma : (Lift∙ {ℓ} (S₊∙ n) →∙ B ∙) ≃∙ (Ω^ n) B
+      lemma = {!   !}
+
+    UnitCohomology : ReducedCohomology k Unit∙ ℤAbGroup ≡ Unit
+    UnitCohomology = isContr→≡Unit ({!   !} , {!   !}) 

src/ThesisWork/EMSpace.agda

@@ -2,167 +2,24 @@
 
 module ThesisWork.EMSpace where
 
-open import Cubical.Algebra.Group
-open import Cubical.Algebra.Group.Base
-open import Cubical.Algebra.Monoid
-open import Cubical.Algebra.Semigroup
-open import Cubical.Algebra.Group.Morphisms
-open import Cubical.Data.Nat using (ℕ) 
-open import Cubical.Foundations.Function
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.GroupoidLaws
-open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Univalence
-open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
-open import Cubical.Homotopy.Loopspace
-open import Cubical.Homotopy.Group.Base
-open import Cubical.HITs.SetTruncation as ST hiding (rec)
-open import Cubical.HITs.GroupoidTruncation as GT hiding (rec)
+open import Cubical.Algebra.Group
 
-variable
-  ℓ ℓ' : Level
-
-data K[_,1] {ℓ : Level} (G : Group ℓ) : Type ℓ where
-  base : K[ G ,1]
-  loop : ⟨ G ⟩ → base ≡ base
-  loop-1g : loop (str G .GroupStr.1g) ≡ refl
-  loop-∙ : (x y : ⟨ G ⟩) → loop (G .snd .GroupStr._·_ x y) ≡ loop y ∙ loop x
-  squash : (x y : K[ G ,1]) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+  
+module _ {ℓ : Level} (GG : Group ℓ) where
+  G = GG .fst
+  open GroupStr (GG .snd)
+  data EM0 : Type ℓ where
+    base : EM0
+    loop : G → base ≡ base
+    loop-1g : loop 1g ≡ refl
+    loop-∙ : (x y : G) → loop (x · y) ≡ loop y ∙ loop x
+    squash : (x y : EM0) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s
 
 module _ where
-  open import Cubical.HITs.S1 renaming (base to S¹-base; loop to S¹-loop)
-  open import Cubical.Data.Int
-  open import Cubical.Algebra.Group.Instances.Int
-  
-  test : S¹ ≃ K[ ℤGroup ,1]
-  test = isoToEquiv (iso {!   !} {!   !} {!   !} {!   !}) where
-    loop^_ : ℤ → S¹-base ≡ S¹-base
-    -- loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop
-    -- loop^ pos zero = refl
-    -- loop^ negsuc zero = sym S¹-loop
-    -- loop^ negsuc (suc n) = (loop^ (negsuc n)) ∙ sym S¹-loop
-
-    Code1 : S¹ → Type
-    Code1 S¹-base = ℤ
-    Code1 (S¹-loop i) = sucPathℤ i
-
-    -- f : S¹ → K[ ℤGroup ,1]
-    -- f S¹-base = base
-    -- f (S¹-loop i) = loop (subst Code1 {!   !} {!   !}) i
-
-    -- f : S¹ → K[ ℤGroup ,1]
-    -- f S¹-base = base
-    -- f (S¹-loop i) = loop (subst Code1 {!   !} {!   !}) i
-
-    -- g : K[ ℤGroup ,1] → S¹
-    -- g base = S¹-base
-    -- g (loop x i) = {!   !}
-    -- g (loop-1g i i₁) = {!   !}
-    -- g (loop-∙ x y i i₁) = {!   !}
-    -- g (squash x y p q r s i j k) = {!   !}
-
-
-
--------------------------------------------------------------------------------
--- Properties
-
--- ΩK(G,1) ≃ G
-
-module _ (G : Group ℓ) where
-  open GroupStr (G .snd)
-
-  _⊙_ = _·_
-
-  K[G,1] = K[ G ,1]
-
-  K[G,1]∙ : Pointed ℓ
-  K[G,1]∙ = K[G,1] , base
-
-  ΩK[G,1] = Ω K[G,1]∙
-  π1K[G,1] = π 1 K[G,1]∙
-
-  lemma1 : isOfHLevel 3 K[G,1] 
-  lemma1 = squash
-
-  lemma2 : isOfHLevel 2 ⟨ ΩK[G,1] ⟩
-  lemma2 = squash base base
-
-  ΩSetG : Pointed (ℓ-suc ℓ)
-  ΩSetG = (hSet ℓ) , (fst G) , is-set
-
-  module Codes-aux where
-    f : (g : ⟨ G ⟩) → ⟨ G ⟩ ≃ ⟨ G ⟩
-    f x = isoToEquiv (iso (λ y → y ⊙ x) (λ y → y ⊙ inv x) fg gf) where
-      fg : section (λ y → y ⊙ x) (λ y → y ⊙ inv x)
-      fg b = sym (·Assoc b (inv x) x) ∙ cong (b ⊙_) (·InvL x) ∙ ·IdR b
-      gf : retract (λ y → y ⊙ x) (λ y → y ⊙ inv x)
-      gf a = sym (·Assoc a x (inv x)) ∙ cong (a ⊙_) (·InvR x) ∙ ·IdR a
-
-    feq : (g : ⟨ G ⟩) → ⟨ G ⟩ ≡ ⟨ G ⟩
-    feq g = ua (f g)
-
-    f1≡id : f 1g ≡ idEquiv ⟨ G ⟩
-    f1≡id = equivEq (funExt (λ x → ·IdR x))
-
-    feq1≡refl : feq 1g ≡ refl
-    feq1≡refl = cong ua f1≡id ∙ uaIdEquiv
-
-    flemma2 : (x y : ⟨ G ⟩) → f (x · y) ≡ compEquiv (f x) (f y)
-    flemma2 x y = equivEq (funExt (λ z → ·Assoc z x y))
-
-  S = Square
-  transpose : {A : Type ℓ} {a00 a01 a10 a11 : A}
-    {a0- : a00 ≡ a01} {a1- : a10 ≡ a11} {a-0 : a00 ≡ a10} {a-1 : a01 ≡ a11}
-    → Square a0- a1- a-0 a-1 → Square a-0 a-1 a0- a1-
-  transpose s i j = s j i
-
-  Codes : K[G,1] → hSet ℓ
-  Codes base = ⟨ G ⟩ , is-set
-  Codes (loop x i) = (Codes-aux.feq x i) , z i where
-    z : PathP (λ i → isSet (Codes-aux.feq x i)) is-set is-set
-    z = toPathP (isPropIsSet (transport (λ i₁ → isSet (Codes-aux.feq x i₁)) is-set) is-set)
-  Codes (loop-1g i j) = {!   !}
-  Codes (loop-∙ x y i j) = {!   !} , {!   !}
-  Codes (squash x y p q r s i j k) = CodesGpd (Codes x) (Codes y) (cong Codes p) (cong Codes q) (cong (cong Codes) r) (cong (cong Codes) s) i j k where
-    CodesGpd = isOfHLevelTypeOfHLevel 2
-
-  -- For point-free transports
-  Codes2 : K[G,1] → Type ℓ
-  Codes2 x = Codes x .fst
-
-  fact : (x y : ⟨ G ⟩) → subst Codes2 (loop x) y ≡ y ⊙ x
-  fact x y = let z = sym (subst-filler {!   !} {!   !} {!   !}) in {!   !}
-
-  encode : (z : K[G,1]) → base ≡ z → ⟨ Codes z ⟩
-  encode z p = subst Codes2 p 1g
-
-  decode : ⟨ G ⟩ → base ≡ base
-  decode x = loop x
-
-  encode-decode : (x : ⟨ G ⟩) → encode base (decode x) ≡ x
-  encode-decode x =
-    encode base (decode x) ≡⟨ refl ⟩
-    encode base (loop x) ≡⟨ refl ⟩
-    subst Codes2 (loop x) 1g ≡⟨ fact x 1g ⟩
-    1g ⊙ x ≡⟨ ·IdL x ⟩
-    x ∎
-
-  ΩKG1≃G' : GroupIso {! ΩK[G,1]  !} G
-
-  ΩKG1≃G : ⟨ ΩK[G,1] ⟩ ≃ ⟨ G ⟩
-  ΩKG1≃G = isoToEquiv (iso f {!   !} {!   !} {!   !}) where
-    f : ⟨ ΩK[G,1] ⟩ → ⟨ G ⟩
-    f p = {!   !}
-
-  ΩKG1-idem-trunc : π 1 (K[G,1]∙) ≃ ⟨ ΩK[G,1] ⟩
-  ΩKG1-idem-trunc = isoToEquiv (setTruncIdempotentIso lemma2)
-
-  π₁KG1≃G : ⟨ πGr 0 (K[G,1]∙) ⟩ ≃ ⟨ G ⟩
-  π₁KG1≃G = compEquiv ΩKG1-idem-trunc ΩKG1≃G
-   
--- Uniqueness
-     
-module _ (n : ℕ) (X Y : Pointed ℓ) where
+  open import Cubical.HITs.EilenbergMacLane1
+  open import Cubical.Homotopy.EilenbergMacLane.Base

src/ThesisWork/EMSpaceOld0.agda

@@ -0,0 +1,168 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.EMSpaceOld0 where
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Semigroup
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Data.Nat using (ℕ) 
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Homotopy.Group.Base
+open import Cubical.HITs.SetTruncation as ST hiding (rec)
+open import Cubical.HITs.GroupoidTruncation as GT hiding (rec)
+
+variable
+  ℓ ℓ' : Level
+
+data K[_,1] {ℓ : Level} (G : Group ℓ) : Type ℓ where
+  base : K[ G ,1]
+  loop : ⟨ G ⟩ → base ≡ base
+  loop-1g : loop (str G .GroupStr.1g) ≡ refl
+  loop-∙ : (x y : ⟨ G ⟩) → loop (G .snd .GroupStr._·_ x y) ≡ loop y ∙ loop x
+  squash : (x y : K[ G ,1]) (p q : x ≡ y) (r s : p ≡ q) → r ≡ s
+
+module _ where
+  open import Cubical.HITs.S1 renaming (base to S¹-base; loop to S¹-loop)
+  open import Cubical.Data.Int
+  open import Cubical.Algebra.Group.Instances.Int
+  
+  test : S¹ ≃ K[ ℤGroup ,1]
+  test = isoToEquiv (iso {!   !} {!   !} {!   !} {!   !}) where
+    loop^_ : ℤ → S¹-base ≡ S¹-base
+    -- loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop
+    -- loop^ pos zero = refl
+    -- loop^ negsuc zero = sym S¹-loop
+    -- loop^ negsuc (suc n) = (loop^ (negsuc n)) ∙ sym S¹-loop
+
+    Code1 : S¹ → Type
+    Code1 S¹-base = ℤ
+    Code1 (S¹-loop i) = sucPathℤ i
+
+    -- f : S¹ → K[ ℤGroup ,1]
+    -- f S¹-base = base
+    -- f (S¹-loop i) = loop (subst Code1 {!   !} {!   !}) i
+
+    -- f : S¹ → K[ ℤGroup ,1]
+    -- f S¹-base = base
+    -- f (S¹-loop i) = loop (subst Code1 {!   !} {!   !}) i
+
+    -- g : K[ ℤGroup ,1] → S¹
+    -- g base = S¹-base
+    -- g (loop x i) = {!   !}
+    -- g (loop-1g i i₁) = {!   !}
+    -- g (loop-∙ x y i i₁) = {!   !}
+    -- g (squash x y p q r s i j k) = {!   !}
+
+
+
+-------------------------------------------------------------------------------
+-- Properties
+
+-- ΩK(G,1) ≃ G
+
+module _ (G : Group ℓ) where
+  open GroupStr (G .snd)
+
+  _⊙_ = _·_
+
+  K[G,1] = K[ G ,1]
+
+  K[G,1]∙ : Pointed ℓ
+  K[G,1]∙ = K[G,1] , base
+
+  ΩK[G,1] = Ω K[G,1]∙
+  π1K[G,1] = π 1 K[G,1]∙
+
+  lemma1 : isOfHLevel 3 K[G,1] 
+  lemma1 = squash
+
+  lemma2 : isOfHLevel 2 ⟨ ΩK[G,1] ⟩
+  lemma2 = squash base base
+
+  ΩSetG : Pointed (ℓ-suc ℓ)
+  ΩSetG = (hSet ℓ) , (fst G) , is-set
+
+  module Codes-aux where
+    f : (g : ⟨ G ⟩) → ⟨ G ⟩ ≃ ⟨ G ⟩
+    f x = isoToEquiv (iso (λ y → y ⊙ x) (λ y → y ⊙ inv x) fg gf) where
+      fg : section (λ y → y ⊙ x) (λ y → y ⊙ inv x)
+      fg b = sym (·Assoc b (inv x) x) ∙ cong (b ⊙_) (·InvL x) ∙ ·IdR b
+      gf : retract (λ y → y ⊙ x) (λ y → y ⊙ inv x)
+      gf a = sym (·Assoc a x (inv x)) ∙ cong (a ⊙_) (·InvR x) ∙ ·IdR a
+
+    feq : (g : ⟨ G ⟩) → ⟨ G ⟩ ≡ ⟨ G ⟩
+    feq g = ua (f g)
+
+    f1≡id : f 1g ≡ idEquiv ⟨ G ⟩
+    f1≡id = equivEq (funExt (λ x → ·IdR x))
+
+    feq1≡refl : feq 1g ≡ refl
+    feq1≡refl = cong ua f1≡id ∙ uaIdEquiv
+
+    flemma2 : (x y : ⟨ G ⟩) → f (x · y) ≡ compEquiv (f x) (f y)
+    flemma2 x y = equivEq (funExt (λ z → ·Assoc z x y))
+
+  S = Square
+  transpose : {A : Type ℓ} {a00 a01 a10 a11 : A}
+    {a0- : a00 ≡ a01} {a1- : a10 ≡ a11} {a-0 : a00 ≡ a10} {a-1 : a01 ≡ a11}
+    → Square a0- a1- a-0 a-1 → Square a-0 a-1 a0- a1-
+  transpose s i j = s j i
+
+  Codes : K[G,1] → hSet ℓ
+  Codes base = ⟨ G ⟩ , is-set
+  Codes (loop x i) = (Codes-aux.feq x i) , z i where
+    z : PathP (λ i → isSet (Codes-aux.feq x i)) is-set is-set
+    z = toPathP (isPropIsSet (transport (λ i₁ → isSet (Codes-aux.feq x i₁)) is-set) is-set)
+  Codes (loop-1g i j) = {!   !}
+  Codes (loop-∙ x y i j) = {!   !} , {!   !}
+  Codes (squash x y p q r s i j k) = CodesGpd (Codes x) (Codes y) (cong Codes p) (cong Codes q) (cong (cong Codes) r) (cong (cong Codes) s) i j k where
+    CodesGpd = isOfHLevelTypeOfHLevel 2
+
+  -- For point-free transports
+  Codes2 : K[G,1] → Type ℓ
+  Codes2 x = Codes x .fst
+
+  fact : (x y : ⟨ G ⟩) → subst Codes2 (loop x) y ≡ y ⊙ x
+  fact x y = let z = sym (subst-filler {!   !} {!   !} {!   !}) in {!   !}
+
+  encode : (z : K[G,1]) → base ≡ z → ⟨ Codes z ⟩
+  encode z p = subst Codes2 p 1g
+
+  decode : ⟨ G ⟩ → base ≡ base
+  decode x = loop x
+
+  encode-decode : (x : ⟨ G ⟩) → encode base (decode x) ≡ x
+  encode-decode x =
+    encode base (decode x) ≡⟨ refl ⟩
+    encode base (loop x) ≡⟨ refl ⟩
+    subst Codes2 (loop x) 1g ≡⟨ fact x 1g ⟩
+    1g ⊙ x ≡⟨ ·IdL x ⟩
+    x ∎
+
+  ΩKG1≃G' : GroupIso {! ΩK[G,1]  !} G
+
+  ΩKG1≃G : ⟨ ΩK[G,1] ⟩ ≃ ⟨ G ⟩
+  ΩKG1≃G = isoToEquiv (iso f {!   !} {!   !} {!   !}) where
+    f : ⟨ ΩK[G,1] ⟩ → ⟨ G ⟩
+    f p = {!   !}
+
+  ΩKG1-idem-trunc : π 1 (K[G,1]∙) ≃ ⟨ ΩK[G,1] ⟩
+  ΩKG1-idem-trunc = isoToEquiv (setTruncIdempotentIso lemma2)
+
+  π₁KG1≃G : ⟨ πGr 0 (K[G,1]∙) ⟩ ≃ ⟨ G ⟩
+  π₁KG1≃G = compEquiv ΩKG1-idem-trunc ΩKG1≃G
+   
+-- Uniqueness
+     
+module _ (n : ℕ) (X Y : Pointed ℓ) where

src/ThesisWork/Ext.agda

@@ -5,6 +5,7 @@
 module ThesisWork.Ext where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.Function
 open import Cubical.Algebra.Module

src/ThesisWork/HomotopyGroupLES.agda

@@ -50,14 +50,15 @@ module _ where
 Fiber : {A B : Pointed ℓ} (f : A →∙ B) → Pointed ℓ
 Fiber {A = A , a} {B = B , b} (f , feq) = (fiber f b) , a , feq
 
+-- General definition of p₁ as the first projection
+p₁ : ∀ {ℓ} {A∙ B∙ : Pointed ℓ} {f∙ : A∙ →∙ B∙} → Fiber f∙ →∙ A∙
+p₁ = fst , refl
+
 -- Lemma 4.1.5 in FVD thesis
 -- Suppose given a pointed map f : A →∗ B
 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₁ = 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 = {!   !}
@@ -81,10 +82,6 @@ module πLES {X Y : Pointed ℓ} (f : X →∙ Y) where
   πSeq (n , 2 , p) = πGr n F
   πSeq (n , suc (suc (suc k)) , p) = ⊥-rec (¬m+n<m p)  
 
-  -- First projection pointed function
-  p₁ : F →∙ X
-  p₁ = fst , refl
-
   -- Step 1
   module Step1 where
     arrow* = Σ (Pointed ℓ) λ X → Σ (Pointed ℓ) λ Y → X →∙ Y

src/ThesisWork/README.md

@@ -25,22 +25,24 @@ flowchart TB
     Exactness --> ExactSequence
     ChainComplex --> Homology
     ChainComplex --> CochainComplex
+    ChainComplex --> Homology
     CochainComplex --> Cohomology
     ChainComplex --> ExactSequence
     CochainComplex --> ExactSequence
     Cohomology --> Theorem5410
+    ExactCouple --> DerivedCouple
     ExactSequence --> ExactCouple
-    
+
     ExactSequence --> HomotopyGroupLES
     HomotopyGroupLES --> SpectrumLES
     Spectrum --> SpectrumMap
     SpectrumMap --> SpectrumMapTruncation
     SpectrumMapTruncation --> PostnikovTowerForSpectra
-    
+
     ExactCouple --> BoundedExactCouple
     BoundedExactCouple --> ExactCoupleConvergence
     ExactCoupleConvergence --> Theorem537
-    
+
     Lemma549 --> Theorem5410
     Theorem537 --> Theorem5410
     PostnikovTowerForSpectra --> Theorem5410

src/ThesisWork/Sequence.agda

@@ -18,12 +18,18 @@ module _ {ℓN : Level} (N : SuccStr ℓN) where
   Sequence : ∀ {ℓ : Level} → (A : Index → Type ℓ) → Type (ℓ-max ℓ ℓN)
   Sequence A = (n : Index) → A n
 
-  record IsChainComplex {ℓS N : Level}
+  record IsChainComplex {ℓS : Level}
       (S : Sequence (λ _ → Pointed ℓS))
       (F : Sequence (λ n → S (succ n) →∙ S n))
     : Type (ℓ-max ℓN ℓS) where
     field
-      property : (n : Index) → 
+      CC : (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ₙ
+        (dₙ ∘∙ dₙ₊₁) ≡ const∙ Tₙ₊₂ Tₙ
+
+  record IsExactSequence {ℓS : Level}
+      (S : Sequence (λ _ → Pointed ℓS))
+      (F : Sequence (λ n → S (succ n) →∙ S n))
+    : Type (ℓ-max ℓN ℓS) where
+    field

src/ThesisWork/SpectralSequence.agda

@@ -41,4 +41,4 @@ module _ (R : Ring ℓ) where
       dᵣ∘dᵣ≡0 : (s : ℕ) → compGradedModuleHom (d s) (d s) ≡ idGradedModuleHom (E s)
 
       -- Isomorphisms
-      -- the cohomology of the cochain complex determined by dᵣ.
+      -- the cohomology of the cochain complex determined by dᵣ.

src/ThesisWork/Spectrum.agda

@@ -3,6 +3,7 @@
 module ThesisWork.Spectrum where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.Equiv
@@ -35,6 +36,7 @@ isPtEquivTo≃∙ 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 {ℓ ℓ' : Level} {N : SuccStr ℓ'} (P : Prespectrum {ℓ = ℓ} N) : Type (ℓ-max ℓ ℓ') where
+  constructor mkIsSpectrum
   open Prespectrum P
   open SuccStr N
   field
@@ -70,4 +72,23 @@ SpectrumMap S₁ S₂ = PrespectrumMap (S₁ .fst) (S₂ .fst)
   -- open SuccStr N
   -- field
   --   f : (n : Index) → Y₁ n →∙ Y₂ n
-  --   p : (n : Index) → (e₂ n ∘∙ f n) ∙∼ (Ω→ (f (succ n)) ∘∙ e₁ n)
+  --   p : (n : Index) → (e₂ n ∘∙ f n) ∙∼ (Ω→ (f (succ n)) ∘∙ e₁ n)
+
+module _ where
+  open import Cubical.HITs.EilenbergMacLane1
+  open import Cubical.Homotopy.EilenbergMacLane.Base
+  open import Cubical.Homotopy.EilenbergMacLane.Properties
+  open import Cubical.Structures.Successor
+  open import Cubical.Data.Nat
+  open import Cubical.Algebra.AbGroup
+
+  -- EilenbergMacLane spaces form a spectrum
+
+  open Prespectrum
+
+  EMPrespectrum : (G : AbGroup ℓ) → Prespectrum {ℓ = ℓ} ℕ+
+  EMPrespectrum G .Y n = EM∙ G n 
+  EMPrespectrum G .e n = EM→ΩEM+1∙ n
+
+  EMSpectrum : (G : AbGroup ℓ) → Spectrum {ℓ = ℓ} ℕ+
+  EMSpectrum G = EMPrespectrum G , mkIsSpectrum (λ n → isoToIsEquiv (Iso-EM-ΩEM+1 n) , EM→ΩEM+1-0ₖ n)