diff --git a/src/CubicalHott/Definition8-1-6.agda b/src/CubicalHott/Definition8-1-6.agda
new file mode 100644
index 0000000..4e201d8
--- /dev/null
+++ b/src/CubicalHott/Definition8-1-6.agda
@@ -0,0 +1,73 @@
+{-# OPTIONS --cubical #-}
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module CubicalHott.Definition8-1-6 where
+
+open import Cubical.Data.Int
+open import Cubical.Data.Nat hiding (_+_) renaming (suc to nsuc)
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Univalence
+open import Cubical.HITs.S1 hiding (encode; decode)
+open import Cubical.Homotopy.Group.Base
+
+open import CubicalHott.Theorem8-1-part1
+
+-- Definition 8.1.6
+
+lemma1 : (x : ℤ) → loop⁻ (predℤ x) ∙ loop ≡ loop⁻ x
+lemma1 (pos zero) = rCancel (sym loop)
+lemma1 (pos (nsuc n)) = refl
+lemma1 (negsuc zero) = sym (assoc (sym loop) (sym loop) loop) ∙ cong (λ p → sym loop ∙ p) (lCancel loop) ∙ sym (rUnit (sym loop))
+lemma1 (negsuc (nsuc n)) =
+  sym (assoc (loop⁻ (negsuc (nsuc n))) (sym loop) loop)
+  ∙ sym (assoc (loop⁻ (negsuc n)) (sym loop) (sym loop ∙ loop))
+  ∙ cong (λ p → loop⁻ (negsuc n) ∙ p) (cong (λ p → sym loop ∙ p) (lCancel loop) ∙ sym (rUnit (sym loop)))
+
+decode : (x : S¹) → code x → base ≡ x
+decode base c = loop⁻ c
+decode (loop i) c j = {!   !} where
+  -- S¹
+  -- ———— Boundary (wanted) —————————————————————————————————————
+  -- j = i0 ⊢ base
+  -- j = i1 ⊢ loop i
+  -- 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⁻
+    ∎
+
+  path2 : PathP (λ i → code (loop i) → base ≡ loop i) loop⁻ loop⁻
+  path2 = toPathP path
+
+  n : ℤ
+  n = unglue (i ∨ ~ i) c
+
+  -- 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
+
diff --git a/src/CubicalHott/Lemma2-4-3.agda b/src/CubicalHott/Lemma2-4-3.agda
new file mode 100644
index 0000000..39844b0
--- /dev/null
+++ b/src/CubicalHott/Lemma2-4-3.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma2-4-3 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Homotopy.Base
+
+postulate
+  lemma : {A B : Type} → (f g : A → B) → (H : f ∼ g) → {x y : A} → (p : x ≡ y)
+    → H x ∙ cong g p ≡ cong f p ∙ H y
+-- lemma f g H {x} {y} p i j =
+--   -- B
+--   -- ———— Boundary (wanted) —————————————————————————————————————
+--   -- j = i0 ⊢ f x
+--   -- j = i1 ⊢ g y
+--   -- i = i0 ⊢ hcomp (doubleComp-faces (λ _ → f x) (cong g p) j) (H x j)
+--   -- i = i1 ⊢ hcomp (doubleComp-faces (λ _ → f x) (H y) j) (cong f p j)
+--   let u = λ k → λ where
+--     (i = i0) → {!   !}
+--     (i = i1) → {!   !}
+--     (j = i0) → f x
+--     (j = i1) → g y
+--   in hcomp u {!   !}
\ No newline at end of file
diff --git a/src/CubicalHott/Lemma8-3-1.agda b/src/CubicalHott/Lemma8-3-1.agda
new file mode 100644
index 0000000..c356c0d
--- /dev/null
+++ b/src/CubicalHott/Lemma8-3-1.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma8-3-1 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.HITs.Truncation
+open import Cubical.Data.Nat
+open import Cubical.Data.Unit
+open import Cubical.Homotopy.Group.Base
+open import Cubical.Homotopy.Loopspace
+
+lemma : (A : Type) → (a : A)
+  → (n : ℕ) → hLevelTrunc n A → (k : ℕ) → π (k + n) (A , a) ≡ Unit
+lemma A a n x k = {!   !} where
+  lemma1 : (n : ℕ) → 
\ No newline at end of file
diff --git a/src/CubicalHott/Section6-8.agda b/src/CubicalHott/Section6-8.agda
new file mode 100644
index 0000000..c933c3c
--- /dev/null
+++ b/src/CubicalHott/Section6-8.agda
@@ -0,0 +1,38 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Section6-8 where
+
+open import Cubical.HITs.Pushout
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.HITs.Susp
+open import Cubical.Data.Unit
+
+Susp' : ∀ {l : Level} → (A : Type l) → Type l
+Susp' A = Pushout {A = A} (λ _ → tt) λ _ → tt 
+
+Susp≡Susp' : ∀ {l} → Susp {l} ≡ Susp' {l}
+Susp≡Susp' {l} = funExt p where
+  p : (A : Type l) → Susp A ≡ Susp' A
+  p A = ua (isoToEquiv (iso f g fg gf)) where
+    f : Susp A → Susp' A
+    f north = inl tt
+    f south = inr tt
+    f (merid a i) = push a i 
+
+    g : Susp' A → Susp A
+    g (inl x) = north
+    g (inr x) = south
+    g (push a i) = merid a i
+
+    fg : section f g
+    fg (inl x) = refl
+    fg (inr x) = refl
+    fg (push a i) = refl
+
+    gf : retract f g
+    gf north = refl 
+    gf south = refl
+    gf (merid a i) = refl
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem7-1-4.agda b/src/CubicalHott/Theorem7-1-4.agda
index d1cff02..c6eaf32 100644
--- a/src/CubicalHott/Theorem7-1-4.agda
+++ b/src/CubicalHott/Theorem7-1-4.agda
@@ -3,12 +3,15 @@
 module CubicalHott.Theorem7-1-4 where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Homotopy.Base
 open import Cubical.Data.Nat
 
+open import CubicalHott.Lemma2-4-3 renaming (lemma to lemma2-4-3)
+
 theorem : {X Y : Type}
   → (p : X → Y)
   → (s : Y → X)
@@ -24,22 +27,10 @@ theorem {X} {Y} p s r (suc zero) xHlevel a b =
     step3 = (sym (r a)) ∙ step2 ∙ r b
   in step3
 theorem {X} {Y} p s r (suc (suc n)) xHlevel a b =
-  {!   !} where
-    ε : (p ∘ s) ∼ idfun Y
+  theorem (λ q → sym (r a) ∙ cong p q ∙ r b) (cong s) f (suc n) (xHlevel (s a) (s b)) where
+    f : retract (cong s) (λ q → sym (r a) ∙ cong p q ∙ r b)
+    f q =  cong (sym (r a) ∙_) helper ∙ assoc (sym (r a)) (r a) q ∙ cong (_∙ q) (lCancel (r a)) ∙ sym (lUnit q) where
+      helper : cong p (cong s q) ∙ r b ≡ r a ∙ q
+      helper = sym (lemma2-4-3 (p ∘ s) (idfun Y) r q)
+
     
-
-  -- -- X is h-level (n+2)
-  -- -- If X is h-level (n+1), then Y is h-level (n+1)
-  -- theorem f (cong p') z (suc n) xOfHLevel where
-    -- f : p' a ≡ p' b → a ≡ b
-    -- f = λ q → sym (r a) ∙ cong p q ∙ r b
-
-    -- z : retract (λ q i → p' (q i)) f
-    -- z q =
-    --   f (λ i → p' (q i)) ≡⟨⟩
-    --   sym (r a) ∙ cong p (λ i → p' (q i)) ∙ r b ≡⟨ {!   !} ⟩
-    --   sym (r a) ∙ cong p (λ i → p' (q i)) ∙ r b ≡⟨ {!   !} ⟩
-    --   q ∎
-
-    -- xOfHLevel = xHlevel (p' a) (p' b)
-
diff --git a/src/CubicalHott/Theorem7-2-1.agda b/src/CubicalHott/Theorem7-2-1.agda
new file mode 100644
index 0000000..bf3035b
--- /dev/null
+++ b/src/CubicalHott/Theorem7-2-1.agda
@@ -0,0 +1,11 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-2-1 where
+
+open import Cubical.Foundations.Prelude
+
+forwards : {X : Type} → ((x : X) → (p : x ≡ x) → p ≡ refl) → isSet X
+forwards f x y p q = J (λ y' p' → (q' : x ≡ y') → p' ≡ q') (λ q' → sym (f x q')) p q
+
+backwards : {X : Type} → isSet X → (x : X) → (p : x ≡ x) → p ≡ refl
+backwards X-set x p = X-set x x p refl
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem7-2-2.agda b/src/CubicalHott/Theorem7-2-2.agda
new file mode 100644
index 0000000..6d922df
--- /dev/null
+++ b/src/CubicalHott/Theorem7-2-2.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-2-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Data.Sigma
+
+theorem : {X : Type}
+  → (R : X → X → Type)
+  → ((x : X) → R x x → x ≡ x)
+  → ((x y : X) → (R x y) → x ≡ y)
+  → isSet X
+theorem R r f x y p q = {!   !}
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem8-1-part1.agda b/src/CubicalHott/Theorem8-1-part1.agda
new file mode 100644
index 0000000..517e644
--- /dev/null
+++ b/src/CubicalHott/Theorem8-1-part1.agda
@@ -0,0 +1,61 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem8-1-part1 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Function
+open import Cubical.HITs.S1 hiding (encode; decode)
+open import Cubical.Data.Nat hiding (_+_) renaming (suc to nsuc)
+open import Cubical.Data.Int
+
+open import CubicalHott.Lemma2-3-10 renaming (lemma to lemma2-3-10)
+
+private
+  variable
+    l : Level
+
+-- Definition 8.1.1
+
+suc≃ : ℤ ≃ ℤ
+suc≃ = isoToEquiv (iso sucℤ predℤ sec ret) where
+  sec : section sucℤ predℤ
+  sec (pos zero) = refl
+  sec (pos (nsuc n)) = refl
+  sec (negsuc zero) = refl
+  sec (negsuc (nsuc n)) = refl
+
+  ret : retract sucℤ predℤ
+  ret (pos zero) = refl
+  ret (pos (nsuc n)) = refl
+  ret (negsuc zero) = refl
+  ret (negsuc (nsuc n)) = refl
+
+suc≡ : ℤ ≡ ℤ
+suc≡ = ua suc≃
+
+code : S¹ → Type
+code base = ℤ
+code (loop i) = suc≡ i
+
+loop⁻ : ℤ → base ≡ base
+loop⁻ (pos zero) = refl
+loop⁻ (pos (nsuc n)) = loop⁻ (pos n) ∙ loop
+loop⁻ (negsuc zero) = sym loop
+loop⁻ (negsuc (nsuc n)) = loop⁻ (negsuc n) ∙ sym loop
+
+-- Lemma 8.1.2
+
+lemma8-1-2a : (x : ℤ) → subst code loop x ≡ sucℤ x
+lemma8-1-2a x =
+  subst code loop x ≡⟨ lemma2-3-10 (idfun S¹) code loop x ⟩
+  subst (idfun Type) (cong code loop) x ≡⟨⟩
+  subst (idfun Type) suc≡ x ≡⟨⟩
+  sucℤ x ∎
+
+-- Definition 8.1.5
+
+encode : (x : S¹) → base ≡ x → code x
+encode s p = subst code p (pos zero)
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem8-1.agda b/src/CubicalHott/Theorem8-1.agda
index 1d80c7c..52aedca 100644
--- a/src/CubicalHott/Theorem8-1.agda
+++ b/src/CubicalHott/Theorem8-1.agda
@@ -15,100 +15,12 @@ open import Cubical.HITs.SetTruncation
 open import Cubical.Homotopy.Loopspace
 open import Cubical.Data.Nat hiding (pred; _+_) renaming (suc to nsuc)
 open import Cubical.Data.Int
-open import Cubical.Data.Int.Base
+-- open import Cubical.Data.Int.Base
 
-open import CubicalHott.Lemma2-3-10 renaming (lemma to lemma2-3-10)
+-- open import CubicalHott.Lemma2-3-10 renaming (lemma to lemma2-3-10)
+open import CubicalHott.Theorem8-1-part1
+open import CubicalHott.Definition8-1-6
 
-private
-  variable
-    l : Level
-
--- Definition 8.1.1
-
-suc≃ : ℤ ≃ ℤ
-suc≃ = isoToEquiv (iso sucℤ predℤ sec ret) where
-  sec : section sucℤ predℤ
-  sec (pos zero) = refl
-  sec (pos (nsuc n)) = refl
-  sec (negsuc zero) = refl
-  sec (negsuc (nsuc n)) = refl
-
-  ret : retract sucℤ predℤ
-  ret (pos zero) = refl
-  ret (pos (nsuc n)) = refl
-  ret (negsuc zero) = refl
-  ret (negsuc (nsuc n)) = refl
-
-suc≡ : ℤ ≡ ℤ
-suc≡ = ua suc≃
-
-code : S¹ → Type
-code base = ℤ
-code (loop i) = suc≡ i
-
-loop⁻ : ℤ → base ≡ base
-loop⁻ (pos zero) = refl
-loop⁻ (pos (nsuc n)) = loop⁻ (pos n) ∙ loop
-loop⁻ (negsuc zero) = sym loop
-loop⁻ (negsuc (nsuc n)) = loop⁻ (negsuc n) ∙ sym loop
-
--- Lemma 8.1.2
-
-lemma8-1-2a : (x : ℤ) → subst code loop x ≡ sucℤ x
-lemma8-1-2a x =
-  subst code loop x ≡⟨ lemma2-3-10 (idfun S¹) code loop x ⟩
-  subst (idfun Type) (cong code loop) x ≡⟨⟩
-  subst (idfun Type) suc≡ x ≡⟨⟩
-  sucℤ x ∎
-
--- Definition 8.1.5
-
-encode : (x : S¹) → base ≡ x → code x
-encode s p = subst code p (pos zero)
-
--- Definition 8.1.6
-
-lemma1 : (x : ℤ) → loop⁻ (predℤ x) ∙ loop ≡ loop⁻ x
-lemma1 (pos zero) = rCancel (sym loop)
-lemma1 (pos (nsuc n)) = refl
-lemma1 (negsuc zero) =
-  sym (assoc ? ? ?)
-  ∙ cong (λ p → sym loop ∙ p) (lCancel ?)
-  ∙ sym (rUnit (sym loop))
-lemma1 (negsuc (nsuc n)) = {! refl  !}
-
-decode : (x : S¹) → code x → base ≡ x
-decode base c = loop⁻ c
-decode (loop i) c j = path j (unglue (~ i ∨ i) c) {! i  !} 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⁻
-    ∎
-  -- 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
 
 -- Theorem 8.1.9