diff --git a/src/ThesisWork/ChainComplex.agda b/src/ThesisWork/ChainComplex.agda
new file mode 100644
index 0000000..1ad2fa1
--- /dev/null
+++ b/src/ThesisWork/ChainComplex.agda
@@ -0,0 +1,72 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.ChainComplex where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Function
+open import Cubical.HITs.TypeQuotients
+open import Cubical.Foundations.Structure
+open import Cubical.Structures.Successor
+
+open import ThesisWork.Exactness
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+-- In mathematics, a chain complex is an algebraic structure that consists of a
+-- sequence of abelian groups (or modules) and a sequence of homomorphisms
+-- between consecutive groups such that the image of each homomorphism is
+-- contained in the kernel of the next. 
+--
+-- "Type chain complexes" are chain complexes without the set requirement
+-- a.k.a no set truncation
+-- FVD Definition 4.1.2
+--
+-- Similar to Cubical.Algebra.ChainComplex except it is indexed by a SuccStr
+-- instead of ℕ, and uses Pointed types rather than groups.
+record TypeChainComplex {ℓ ℓ' : Level} (N : SuccStr ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
+  open SuccStr N
+  field
+    seq : (n : Index) → Pointed ℓ'
+    fun : (n : Index) → seq (succ n) →∙ seq n
+
+    -- The primary chain complex property is that the composition of
+    -- consecutive maps is equivalent to the zero morphism, which in groups
+    -- corresponds to the constant map to the zero element.
+    --
+    -- Relevant image: https://upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Illustration_of_an_Exact_Sequence_of_Groups.svg/2880px-Illustration_of_an_Exact_Sequence_of_Groups.svg.png
+    -- ^Explanation: chain complex is only half of the property of an exact
+    -- sequence, so the crucial thing here is that the circle where the left
+    -- half of the cone meets the right is actually potentially smaller for the
+    -- left than the right side. (TODO: Draw this!) But this still means that
+    -- that smaller part will map to the zero element in the next group. Thus,
+    -- d² ≡ 0
+    property : (n : Index) →
+      let Tₙ₊₂ = seq (succ (succ n)) in let Tₙ₊₁ = seq (succ n) in let Tₙ = seq n in
+      let dₙ₊₁ = fun (succ n) in let dₙ = fun n in
+      dₙ ∘∙ dₙ₊₁ ≡ const∙ Tₙ₊₂ Tₙ
+
+record TypeChainMap {ℓ ℓA ℓB : Level} {N : SuccStr ℓ}
+    (A : TypeChainComplex {ℓ} {ℓA} N)
+    (B : TypeChainComplex {ℓ} {ℓB} N)
+    : Type (ℓ-max ℓ (ℓ-max ℓA ℓB)) where
+  open SuccStr N
+  open TypeChainComplex
+  field
+    f : (n : Index) → A .seq n →∙ B .seq n
+
+    -- The boundary forms a commutative square
+    -- 
+    --   Aₙ──dAₙ─→Aₙ₋₁
+    --   │       │
+    --   fₙ      fₙ₋₁
+    --   ↓       ↓
+    --   Bₙ──dBₙ─→Bₙ₋₁
+    comm : (n : Index) → B .fun n ∘∙ f (succ n) ≡ f n ∘∙ A .fun n
+    
+-- module _ {N : SuccStr ℓ} (CC : TypeChainComplex N) where
+--   open SuccStr N
+--   open TypeChainComplex CC
+--   HomologyGroup : (n : Index) → Ker∙ (fun n) /ₜ λ x y → isInIm∙ (fun (succ n)) {!   !}
diff --git a/src/ThesisWork/ExactCouple.agda b/src/ThesisWork/ExactCouple.agda
index 115e1e0..7ab4e6b 100644
--- a/src/ThesisWork/ExactCouple.agda
+++ b/src/ThesisWork/ExactCouple.agda
@@ -12,21 +12,33 @@ open import Cubical.Algebra.Group.DirProd
 open import Cubical.Algebra.Group.Instances.Int
 
 open import ThesisWork.Graded
+open import ThesisWork.Exactness
 
 private
   variable
     ℓ ℓ' ℓ'' : Level
 
-module _ {R : Ring ℓ} where
+module _ (R : Ring ℓ) where
   ℤ×ℤGroup = DirProd ℤGroup ℤGroup
   ℤ×ℤ = ⟨ ℤ×ℤGroup ⟩
 
+  gg = groupHomOfGradedHom
+
   record ExactCouple : Type (ℓ-suc ℓ) where
+    constructor mkExactCouple
     field
       D E : GradedModule R ℤ×ℤ
       i : GradedHom R ℤ×ℤGroup D D
       j : GradedHom R ℤ×ℤGroup D E
       k : GradedHom R ℤ×ℤGroup E D
+      exactAt-ij : isExactAt (gg i) (gg j)
+      exactAt-jk : isExactAt (gg j) (gg k)
+      exactAt-ik : isExactAt (gg i) (gg k)
 
-deriveExactCouple : {R : Ring ℓ} → ExactCouple {R = R} → ExactCouple {R = R}
-deriveExactCouple = {!   !}
\ No newline at end of file
+  -- FVD thesis Lemma 5.2.2
+  -- Hatcher Spectral Sequences section 5.1
+  derivedCouple : ExactCouple → ExactCouple
+  derivedCouple (mkExactCouple D E i j k eij ejk eik) =
+    {!   !} where
+      D' : GradedModule R ℤ×ℤ
+      D' x = {!   !} , {!   !}
\ No newline at end of file
diff --git a/src/ThesisWork/Exactness.agda b/src/ThesisWork/Exactness.agda
new file mode 100644
index 0000000..2de5b21
--- /dev/null
+++ b/src/ThesisWork/Exactness.agda
@@ -0,0 +1,38 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Exactness where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Equiv
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Data.Sigma
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+-- Definition of exactness for Pointed types
+module _ {A B C : Pointed ℓ} where
+  Ker∙ : (f : A →∙ B) → Type ℓ
+  Ker∙ (f , feq) = Σ (A .fst) λ a → f a ≡ B .snd
+
+  Im∙ : (f : A →∙ B) → Type ℓ
+  Im∙ (f , feq) = Σ (B .fst) λ b → Σ (A .fst) λ a → f a ≡ b
+
+  isExactAt∙ : (f : A →∙ B) (g : B →∙ C) → Type ℓ
+  isExactAt∙ f g = (b : ⟨ B ⟩) → (isInKer∙ g b → isInIm∙ f b) × (isInIm∙ f b → isInKer∙ g b)
+
+module _ {A B C : Group ℓ} where
+  -- Exactness except the intersecting Group is only propositionally equal
+  isWeakExactAt : {B' : Group ℓ} (f : GroupHom A B) (g : GroupHom B' C) (p : B ≡ B') → Type ℓ
+  isWeakExactAt {B' = B'} f g p = (b : ⟨ B ⟩) → (isInKer g (tr b) → isInIm f b) × (isInIm f b → isInKer g (tr b)) where
+    tr = λ (b : ⟨ B ⟩) → subst (λ (a : Σ (Type ℓ) GroupStr) → fst a) p b
+
+  isExactAt : (f : GroupHom A B) (g : GroupHom B C) → Type ℓ
+  isExactAt f g = (b : ⟨ B ⟩) → (isInKer g b → isInIm f b) × (isInIm f b → isInKer g b)
+
+  isWeakExactAtRefl : (f : GroupHom A B) (g : GroupHom B C) → isWeakExactAt f g refl ≡ isExactAt f g
+  isWeakExactAtRefl f g i = (b : ⟨ B ⟩) → (isInKer g (transportRefl b i) → isInIm f b) × (isInIm f b → isInKer g (transportRefl b i))
\ No newline at end of file
diff --git a/src/ThesisWork/Ext.agda b/src/ThesisWork/Ext.agda
index 500d3d6..12b33cf 100644
--- a/src/ThesisWork/Ext.agda
+++ b/src/ThesisWork/Ext.agda
@@ -8,12 +8,21 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.Function
 open import Cubical.Algebra.Module
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.Ring
 
 private
   variable
     ℓ ℓ' ℓ'' : Level
 
+module _ where
+  Kernel : ∀ {G H : Group ℓ} → GroupHom G H → Type _
+  Kernel {G = G} GH = Σ ⟨ G ⟩ (isInKer GH)
+
+  Image : ∀ {G H : Group ℓ} → GroupHom G H → Type _
+  Image {H = H} GH = Σ ⟨ H ⟩ (isInIm GH)
+
 module _ {R : Ring ℓ} where
   idLeftModuleHom : (M : LeftModule R ℓ') → LeftModuleHom M M
   idLeftModuleHom M = (idfun ⟨ M ⟩) , record { pres0 = refl ; pres+ = λ x y → refl ; pres- = λ x → refl ; pres⋆ = λ r y → refl } 
diff --git a/src/ThesisWork/Graded.agda b/src/ThesisWork/Graded.agda
index a2a46a8..2f0501f 100644
--- a/src/ThesisWork/Graded.agda
+++ b/src/ThesisWork/Graded.agda
@@ -54,6 +54,9 @@ module _ (R : Ring ℓ) (G : Group ℓ') (M₁ M₂ : GradedModule R ⟨ G ⟩)
         let e = groupEquivFun equiv in -- the function of the equivalence
         {x y : ⟨ G ⟩} → (p : e x ≡ y) → (M₁ x) -[lm]→ (M₂ y)
 
+groupHomOfGradedHom : ∀ {R : Ring ℓ} {G : Group ℓ'} {M₁ M₂} → GradedHom R G M₁ M₂ → GroupHom G G
+groupHomOfGradedHom (mkGradedHom equiv deg_fn fn') = (equiv .fst .fst) , equiv .snd
+
 idGradedModuleHom : {R : Ring ℓ} {G : Group ℓ'} (M : GradedModule R ⟨ G ⟩) → GradedHom R G M M
 idGradedModuleHom {G = G} M = mkGradedHom idGroupEquiv (λ g → sym (·IdR g)) (λ {x = x} p → J (λ y p → M x -[lm]→ M y) (idLeftModuleHom (M x)) p) where
   open GroupStr (G .snd)
diff --git a/src/ThesisWork/Old/SuccStr.agda b/src/ThesisWork/Old/SuccStr.agda
new file mode 100644
index 0000000..c9e5339
--- /dev/null
+++ b/src/ThesisWork/Old/SuccStr.agda
@@ -0,0 +1,82 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.SuccStr where
+
+open import Cubical.Foundations.Prelude
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+-- Deprecated in favor of the one in the cubical library...
+
+-- -- "Successor structure"
+-- -- 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
+--   open import Cubical.Data.Int
+--   open SuccStr
+--   ℤ-SuccStr : SuccStr ℓ-zero
+--   ℤ-SuccStr .A = ℤ
+--   ℤ-SuccStr .suc = sucℤ
+
+-- -- 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
+
+-- -- 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 using (ℤ) renaming (suc to zsuc)
+
+-- --   -- (ℤ , λ n . n + 1)
+-- --   ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ
+-- --   ℤ-SuccStr = SuccStr ℤ zsuc
+
+-- -- module _ where
+-- --   open import Data.Fin
+-- --   open import Data.Product
+
+-- --   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
+
+-- --   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
\ No newline at end of file
diff --git a/src/ThesisWork/Pi3S2/SuccStr.agda b/src/ThesisWork/Pi3S2/SuccStr.agda
deleted file mode 100644
index 28dd447..0000000
--- a/src/ThesisWork/Pi3S2/SuccStr.agda
+++ /dev/null
@@ -1,79 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module ThesisWork.Pi3S2.SuccStr where
-
-open import Cubical.Foundations.Prelude
-
-private
-  variable
-    ℓ ℓ' ℓ'' : Level
-
--- 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
-  open import Cubical.Data.Int
-  open SuccStr
-  ℤ-SuccStr : SuccStr ℓ-zero
-  ℤ-SuccStr .A = ℤ
-  ℤ-SuccStr .suc = sucℤ
-
--- 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
-
--- 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 using (ℤ) renaming (suc to zsuc)
-
---   -- (ℤ , λ n . n + 1)
---   ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ
---   ℤ-SuccStr = SuccStr ℤ zsuc
-
--- module _ where
---   open import Data.Fin
---   open import Data.Product
-
---   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
-
---   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
\ No newline at end of file
diff --git a/src/ThesisWork/README.md b/src/ThesisWork/README.md
index 68da2a9..d41209b 100644
--- a/src/ThesisWork/README.md
+++ b/src/ThesisWork/README.md
@@ -1,3 +1,37 @@
 # Notes
 
 - Already some existing work by Felix Cherubini (@felixwellen) about spectra here: https://github.com/agda/cubical/pull/723
+
+```mermaid
+%%{init: {"layout": "elk", "flowchart": {"htmlLabels": false}} }%%
+flowchart TB
+    style GradedAbelianGroup fill:skyblue
+    style Prespectrum fill:skyblue
+    style Spectrum fill:skyblue
+    style PointedKernel fill:skyblue
+    style PointedImage fill:skyblue
+    style Exactness fill:skyblue
+
+    GradedAbelianGroup --> ExactCouple
+    GradedAbelianGroup --> SpectralSequence
+    ExactCouple --> DerivedCouple
+
+    PointedKernel --> Exactness
+    PointedImage --> Exactness
+    Exactness --> ExactSequence
+    Exactness --> ChainComplex
+    ChainComplex --> Homology
+    ChainComplex --> CochainComplex
+    CochainComplex --> Cohomology
+    Cohomology --> Theorem5410
+    ExactSequence --> ExactCouple
+    ExactSequence --> Theorem535
+
+    PostnikovTower --> Theorem5410
+    Prespectrum --> Spectrum
+    Spectrum --> nthHomotopyGroupOfSpectrum
+
+    SpectralSequence --> Corollary5411
+    SpectralSequence --> Theorem5410
+    SpectralSequence --> Theorem5412
+```
diff --git a/src/ThesisWork/Spectrum.agda b/src/ThesisWork/Spectrum.agda
index 5779873..749ed75 100644
--- a/src/ThesisWork/Spectrum.agda
+++ b/src/ThesisWork/Spectrum.agda
@@ -8,7 +8,7 @@ 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
+open import Cubical.Structures.Successor
 
 private
   variable
@@ -17,31 +17,45 @@ private
 -- 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
+record Prespectrum {ℓ ℓ' : Level} (N : SuccStr ℓ') : Type (ℓ-max ℓ' (ℓ-suc ℓ)) where
   open SuccStr N
   field
-    Y : A → Pointed ℓ
-    e : (n : A) → Y n →∙ Ω (Y (suc n))
+    Y : Index → Pointed ℓ
+    e : (n : Index) → Y n →∙ Ω (Y (succ n))
 
 ℤ-Prespectrum : Type (ℓ-suc ℓ-zero)
-ℤ-Prespectrum = Prespectrum ℤ-SuccStr
+ℤ-Prespectrum = Prespectrum ℤ+
 
 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
+isPtEquivTo≃∙ : {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) → isPointedEquiv f → A ≃∙ B
+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 {N : SuccStr ℓ} (P : Prespectrum N) : Type ℓ where
+record IsSpectrum {ℓ ℓ' : Level} {N : SuccStr ℓ'} (P : Prespectrum {ℓ = ℓ} N) : Type (ℓ-max ℓ ℓ') where
   open Prespectrum P
   open SuccStr N
   field
-    eIsEquiv : ∀ (n : A) → isPointedEquiv (e n)
+    eIsEquiv : ∀ (n : Index) → isPointedEquiv (e n)
 
 Spectrum : SuccStr ℓ → Type (ℓ-suc ℓ)
 Spectrum {ℓ = ℓ} N = Σ (Prespectrum N) IsSpectrum
 
 ℤ-Spectrum : Type (ℓ-suc ℓ-zero)
-ℤ-Spectrum = Spectrum ℤ-SuccStr
+ℤ-Spectrum = Spectrum ℤ+
+
+-- Also from definition 5.3.1 of FVD thesis
+record PrespectrumMap {ℓN ℓ₁ ℓ₂ : Level} {N : SuccStr ℓN}
+    (PS₁ : Prespectrum {ℓ = ℓ₁} N)
+    (PS₂ : Prespectrum {ℓ = ℓ₂} N)
+  : Type (ℓ-max ℓN (ℓ-max ℓ₁ ℓ₂)) where
+  open Prespectrum PS₁ renaming (Y to Y₁; e to e₁)
+  open Prespectrum PS₂ renaming (Y to Y₂; e to e₂)
+  open SuccStr N
+  field
+    f : (n : Index) → Y₁ n →∙ Y₂ n
+
+    -- TODO: Visualize this
+    p : (n : Index) → (e₂ n ∘∙ f n) ∙∼ (Ω→ (f (succ n)) ∘∙ e₁ n)