diff --git a/src/CubicalHott/Definition8-1-6.agda b/src/CubicalHott/Definition8-1-6.agda
index 8ae813d..63a9591 100644
--- a/src/CubicalHott/Definition8-1-6.agda
+++ b/src/CubicalHott/Definition8-1-6.agda
@@ -53,7 +53,6 @@ decode (loop i) c j =
     (j = i0) → base
     (j = i1) → loop (i ∨ ~ k)
   in hcomp u (loop⁻ (unglue (i ∨ ~ i) c) j)
-  where
     -- S¹
     -- ———— Boundary (wanted) —————————————————————————————————————
     -- j = i0 ⊢ base
@@ -61,40 +60,27 @@ decode (loop i) c j =
     -- i = i0 ⊢ loop⁻ c j
     -- i = i1 ⊢ loop⁻ c j
 
-    path : subst (λ x' → code x' → base ≡ x') loop loop⁻ ≡ loop⁻
-    path =
-        subst (λ x' → (code x' → base ≡ x')) loop loop⁻
-      ≡⟨⟩
-        subst (λ x' → base ≡ x') loop ∘ loop⁻ ∘ subst code (sym loop)
-      ≡⟨⟩
-        (λ p → p ∙ loop) ∘ loop⁻ ∘ subst code (sym loop)
-      ≡⟨⟩
-        (λ p → p ∙ loop) ∘ (loop⁻ ∘ predℤ)
-      ≡⟨⟩
-        (λ n → loop⁻ (predℤ n) ∙ loop)
-      ≡⟨ funExt lemma1 ⟩
-        loop⁻
-      ∎
+module helper where
+  path : subst (λ x' → code x' → base ≡ x') loop loop⁻ ≡ loop⁻
+  path =
+      subst (λ x' → (code x' → base ≡ x')) loop loop⁻
+    ≡⟨⟩
+      subst (λ x' → base ≡ x') loop ∘ loop⁻ ∘ subst code (sym loop)
+    ≡⟨⟩
+      (λ p → p ∙ loop) ∘ loop⁻ ∘ subst code (sym loop)
+    ≡⟨⟩
+      (λ p → p ∙ loop) ∘ (loop⁻ ∘ predℤ)
+    ≡⟨⟩
+      (λ n → loop⁻ (predℤ n) ∙ loop)
+    ≡⟨ funExt lemma1 ⟩
+      loop⁻
+    ∎
 
-    path2 : PathP (λ i → code (loop i) → base ≡ loop i) loop⁻ loop⁻
-    path2 = toPathP path
+  path2 : PathP (λ i → code (loop i) → base ≡ loop i) loop⁻ loop⁻
+  path2 = toPathP path
 
-    n : ℤ
-    n = unglue (i ∨ ~ i) c
+open helper using (path2)
 
-    -- we are trying to prove that loop⁻ c j ≡ loop⁻ c j
-    -- but on one side it's refl_base, and on the other, it's loop i
-    -- let
-    --   bottomFace = let u = λ j → λ where
-    --       (i = i0) → {!   !}
-    --       (i = i1) → {!   !}
-    --     in hfill u (inS {!   !}) {! j  !}
-
-    --   u = λ k → λ where
-    --     (i = i0) → {!   !}
-    --     (i = i1) → loop⁻ c j
-    --     (j = i0) → base
-    --     (j = i1) → loop (i ∨ ~ k)
-    -- in hcomp u bottomFace
- 
- 
\ No newline at end of file
+decode' : (x : S¹) → code x → base ≡ x
+decode' base c = loop⁻ c
+decode' (loop i) c j = path2 i c j
\ No newline at end of file
diff --git a/src/CubicalHott/Lemma8-3-1.agda b/src/CubicalHott/Lemma8-3-1.agda
index a43c5ef..600c3a4 100644
--- a/src/CubicalHott/Lemma8-3-1.agda
+++ b/src/CubicalHott/Lemma8-3-1.agda
@@ -3,13 +3,23 @@
 module CubicalHott.Lemma8-3-1 where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.HLevels
 open import Cubical.HITs.Truncation
 open import Cubical.Data.Nat
 open import Cubical.Data.Unit
+open import Cubical.Homotopy.Connected
 open import Cubical.Homotopy.Group.Base
 open import Cubical.Homotopy.Loopspace
+open import Cubical.HITs.SetTruncation
 
-lemma : (A : Type) → (a : A)
-  → (n : ℕ) → hLevelTrunc n A → (k : ℕ) → π (k + n) (A , a) ≡ Unit
-lemma A a n x k = {!   !} where
\ No newline at end of file
+
+helper : ∀ {l : Level} → (n : ℕ) → (A∙ @ (A , a) : Pointed l)
+  → isOfHLevel (suc n) A → isOfHLevel n (typ (Ω A∙))
+helper zero A∙@(A , a) prf = refl , (λ y j i → {!   !})
+helper (suc zero) A∙@(A , a) prf = {!   !}
+helper (suc (suc n)) A∙@(A , a) prf = {!   !}
+
+-- lemma : ∀ {l} → (A∙ @ (A , a) : Pointed l)
+--   → (n : ℕ) → hLevelTrunc n A → (k : ℕ) → π (k + n) (A , a) ≡ Lift Unit
+-- lemma A∙ @ (A , a) n x k i = {!   !} where  
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem8-1.agda b/src/CubicalHott/Theorem8-1.agda
index 103002f..61d15b2 100644
--- a/src/CubicalHott/Theorem8-1.agda
+++ b/src/CubicalHott/Theorem8-1.agda
@@ -27,9 +27,12 @@ open import CubicalHott.Definition8-1-6
 decode-encode : (x : S¹) → (p : base ≡ x) → decode x (encode x p) ≡ p
 decode-encode x p = J (λ x' p' → decode x' (encode x' p') ≡ p') refl p
 
+decode'-encode : (x : S¹) → (p : base ≡ x) → decode' x (encode x p) ≡ p
+decode'-encode x p = J (λ x' p' → decode' x' (encode x' p') ≡ p') refl p
+
 -- Lemma 8.1.8
 
-encode-decode-base : (c : ℤ) → encode base (decode base c) ≡ c
+encode-decode-base : (c : ℤ) → encode base (loop⁻ c) ≡ c
 encode-decode-base (pos n) = pos-case n where
   pos-case : (n : ℕ) → encode base (loop⁻ (pos n)) ≡ pos n
   pos-case zero = refl
@@ -52,10 +55,16 @@ encode-decode-base (negsuc n) = neg-case n where
 -- encode-decode : (x : S¹) → (c : code x) → encode x (decode x c) ≡ c
 -- encode-decode (loop i) c = {!   !} -- encode (loop i) (decode (loop i) c) ≡ c
 
+encode-decode' : (x : S¹) → (c : code x) → encode x (decode' x c) ≡ c
+encode-decode' base c = {!   !}
+encode-decode' (loop i) c =
+  encode (loop i) {! decode (loop i) c  !} ≡⟨ {!   !} ⟩
+  c ∎
+
 -- Theorem 8.1.9
 
--- theorem8-1-9 : (x : S¹) → ((base ≡ x) ≃ code x)
--- theorem8-1-9 x = isoToEquiv (iso (encode x) (decode x) (encode-decode x) (decode-encode x))
+theorem8-1-9 : (x : S¹) → ((base ≡ x) ≃ code x)
+theorem8-1-9 x = isoToEquiv (iso (encode x) (decode' x) (encode-decode' x) (decode'-encode x))
 
 cheated-theorem-8-1-9 : (base ≡ base) ≃ ℤ
 cheated-theorem-8-1-9 = isoToEquiv (iso (encode base) (decode base) encode-decode-base (decode-encode base))
diff --git a/src/ThesisWork/ChainComplex.agda b/src/ThesisWork/ChainComplex.agda
new file mode 100644
index 0000000..588517f
--- /dev/null
+++ b/src/ThesisWork/ChainComplex.agda
@@ -0,0 +1,11 @@
+-- lean2/hott/homotopy/chain_complex.lean
+
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.ChainComplex where
+
+open import Cubical.Foundations.Prelude
+open import Agda.Primitive
+
+SuccStr : ∀ {l} → Type (lsuc l)
+SuccStr {l} = Σ (Type l) (λ carrier → carrier → carrier)
diff --git a/src/ThesisWork/Cohomology.agda b/src/ThesisWork/Cohomology.agda
new file mode 100644
index 0000000..0e0fac8
--- /dev/null
+++ b/src/ThesisWork/Cohomology.agda
@@ -0,0 +1,10 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Cohomology where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Algebra.AbGroup
+
+Cohomology : ∀ {l} → (X : Pointed l) → AbGroup l
+Cohomology = {!   !}
\ No newline at end of file
diff --git a/src/ThesisWork/Spectrum.agda b/src/ThesisWork/Spectrum.agda
new file mode 100644
index 0000000..1c1510c
--- /dev/null
+++ b/src/ThesisWork/Spectrum.agda
@@ -0,0 +1,3 @@
+{-# OPTIONS --cubical #-}
+
+module ThesisWork.Spectrum where
diff --git a/type-theory.agda-lib b/type-theory.agda-lib
index fa954a9..57b94f3 100644
--- a/type-theory.agda-lib
+++ b/type-theory.agda-lib
@@ -1,2 +1,2 @@
-include: src
+include: src src/ThesisWork
 depend: standard-library cubical agda-unimath