diff --git a/resources/AT+.pdf b/resources/AT+.pdf
new file mode 100644
index 0000000..194480f
Binary files /dev/null and b/resources/AT+.pdf differ
diff --git a/resources/VanDoornDissertation/dissertation-ebook.pdf b/resources/VanDoornDissertation/dissertation-ebook.pdf
new file mode 100644
index 0000000..9aa4b07
Binary files /dev/null and b/resources/VanDoornDissertation/dissertation-ebook.pdf differ
diff --git a/resources/VanDoornDissertation/dissertation.pdf b/resources/VanDoornDissertation/dissertation.pdf
index 9aa4b07..8b072c3 100644
Binary files a/resources/VanDoornDissertation/dissertation.pdf and b/resources/VanDoornDissertation/dissertation.pdf differ
diff --git a/src/ThesisWork/ChainComplex.agda b/src/ThesisWork/Pi3S2/ChainComplex.agda
similarity index 50%
rename from src/ThesisWork/ChainComplex.agda
rename to src/ThesisWork/Pi3S2/ChainComplex.agda
index 588517f..5cbe640 100644
--- a/src/ThesisWork/ChainComplex.agda
+++ b/src/ThesisWork/Pi3S2/ChainComplex.agda
@@ -2,10 +2,9 @@
 
 {-# OPTIONS --cubical #-}
 
-module ThesisWork.ChainComplex where
+module ThesisWork.Pi3S2.ChainComplex where
 
 open import Cubical.Foundations.Prelude
 open import Agda.Primitive
 
-SuccStr : ∀ {l} → Type (lsuc l)
-SuccStr {l} = Σ (Type l) (λ carrier → carrier → carrier)
+data ChainComplex : Type where
\ No newline at end of file
diff --git a/src/ThesisWork/LES.agda b/src/ThesisWork/Pi3S2/LES.agda
similarity index 99%
rename from src/ThesisWork/LES.agda
rename to src/ThesisWork/Pi3S2/LES.agda
index 8c7ef97..4933405 100644
--- a/src/ThesisWork/LES.agda
+++ b/src/ThesisWork/Pi3S2/LES.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --cubical #-}
 
-module ThesisWork.LES where
+module ThesisWork.Pi3S2.LES where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Pointed
diff --git a/src/ThesisWork/Pi3S2/Lemma4-1-5.agda b/src/ThesisWork/Pi3S2/Lemma4-1-5.agda
new file mode 100644
index 0000000..c8ce4e7
--- /dev/null
+++ b/src/ThesisWork/Pi3S2/Lemma4-1-5.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Pi3S2.Lemma4-1-5 where
+
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Homotopy.Loopspace
+
+fiberF : {l : Level} {A∙ B∙ : Pointed l} → (f : A∙ →∙ B∙) → Pointed l
+fiberF {A∙ = A∙ @ (A , a)} {B∙ = B∙ @ (B , b)} f = fiber (fst f) b , a , (snd f)
+
+lemma : ∀ {l : Level} {A∙ @ (A , a) B∙ @ (B , b) : Pointed l}
+  → (f : A∙ →∙ B∙)
+  → let
+      p₁ : fiberF f →∙ A∙
+      p₁ = fst , refl
+    in fiberF p₁ ≃∙ (Ω B∙)
+lemma {A∙ = A∙ @ (A , a0)} {B∙ = B∙ @ (B , b0)} f∙ @ (f , f-eq) = eqv , {!   !} where
+  eqv : fst (fiberF ((λ r → fst r) , refl)) ≃ fst (Ω B∙)
+  eqv =
+      fst (fiberF ((λ r → fst r) , refl))
+    ≃⟨ {!   !} ⟩
+      Σ (fst (fiberF f∙)) (λ fibf @ (a , p) → a ≡ a0)
+    ≃⟨ {!   !} ⟩
+      Σ A (λ a → (a ≡ a0) × (f a ≡ b0))
+    ≃⟨ {!   !} ⟩
+      f a0 ≡ b0
+    ≃⟨ {!   !} ⟩
+      b0 ≡ b0
+    ≃⟨ idEquiv (b0 ≡ b0) ⟩
+      fst (Ω B∙)
+    ■
diff --git a/src/ThesisWork/Pi3S2/SuccStr.agda b/src/ThesisWork/Pi3S2/SuccStr.agda
new file mode 100644
index 0000000..5a6d612
--- /dev/null
+++ b/src/ThesisWork/Pi3S2/SuccStr.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Pi3S2.SuccStr where
+
+open import Cubical.Foundations.Prelude
+open import Data.Nat
+
+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 renaming (suc to zsuc)
+
+  -- (ℤ , λ n . n + 1)
+  ℤ-SuccStr : (i : ℤ) → (n : ℕ) → ℤ
+  ℤ-SuccStr = SuccStr ℤ zsuc
\ No newline at end of file
diff --git a/src/ThesisWork/README.md b/src/ThesisWork/README.md
new file mode 100644
index 0000000..34c35f9
--- /dev/null
+++ b/src/ThesisWork/README.md
@@ -0,0 +1,3 @@
+# Notes
+
+- Already some existing work by Felix Cherubini (@felixwellen) about spectra here: https://github.com/agda/cubical/pull/723