diff --git a/src/CubicalHott/HLevels.agda b/src/CubicalHott/HLevels.agda
index 1cc7e90..ce118fb 100644
--- a/src/CubicalHott/HLevels.agda
+++ b/src/CubicalHott/HLevels.agda
@@ -14,6 +14,12 @@ isOfHLevel' (suc n) A = (x y : A) → isOfHLevel' n (x ≡ y)
 TypeOfHLevel' : ∀ ℓ → HLevel → Type (ℓ-suc ℓ)
 TypeOfHLevel' ℓ n = TypeWithStr ℓ (isOfHLevel' n)
 
+1Prop : (T : Type) → isOfHLevel' 1 T → isProp T
+1Prop T T1 x y = let z = T1 x y in fst z
+
+Prop1 : {l : Level} → (T : Type l) → isProp T → isOfHLevel' 1 T
+Prop1 T Tp x y = (Tp x y) , λ q → isProp→isSet Tp x y (Tp x y) q
+
 isOfHLevel→isOfHLevel' : ∀ {l : Level} → (n : ℕ) → (A : Type l)
   → isOfHLevel n A → isOfHLevel' n A
 isOfHLevel→isOfHLevel' zero A z = z
diff --git a/src/CubicalHott/Lemma3-5-1.agda b/src/CubicalHott/Lemma3-5-1.agda
index 784eb24..73170ba 100644
--- a/src/CubicalHott/Lemma3-5-1.agda
+++ b/src/CubicalHott/Lemma3-5-1.agda
@@ -22,27 +22,27 @@ corollary : {l : Level} → {A B : Type l}
   → f ≡ g
 corollary f g p = lemma isPropIsEquiv f g p
 
-corollary-equiv : {l : Level} → {A B : Type l}
-  → (f g : A ≃ B)
-  → (fst f ≡ fst g) ≃ (f ≡ g)
-corollary-equiv f g = isoToEquiv (iso (corollary f g) (cong fst) fg gf) where
-  helper : (f≡g : f ≡ g) → subst (λ x → isEquiv (fst x)) f≡g (snd f) ≡ snd g
-  helper f≡g = isPropIsEquiv (fst g) (subst (λ x → isEquiv (fst x)) f≡g (snd f)) (snd g)
+-- corollary-equiv : {l : Level} → {A B : Type l}
+--   → (f g : A ≃ B)
+--   → (fst f ≡ fst g) ≃ (f ≡ g)
+-- corollary-equiv f g = isoToEquiv (iso (corollary f g) (cong fst) fg gf) where
+--   helper : (f≡g : f ≡ g) → subst (λ x → isEquiv (fst x)) f≡g (snd f) ≡ snd g
+--   helper f≡g = isPropIsEquiv (fst g) (subst (λ x → isEquiv (fst x)) f≡g (snd f)) (snd g)
 
-  helper2 : (f≡g : f ≡ g) → PathP (λ i → isEquiv (fst (f≡g i))) (snd f) (snd g)
-  helper2 f≡g = toPathP (helper f≡g)
+--   helper2 : (f≡g : f ≡ g) → PathP (λ i → isEquiv (fst (f≡g i))) (snd f) (snd g)
+--   helper2 f≡g = toPathP (helper f≡g)
 
-  fg : section (corollary f g) (cong fst)
-  -- Trying to prove that producing full f ≡ g after discarding the second half still produces the original
-  -- However, no matter what the original is, the isEquiv part is a mere prop
-  fg f≡g i j = fst (f≡g j) , {!   !} where
-    -- isEquiv (fst (f≡g j))
-    -- ———— Boundary (wanted) —————————————————————————————————————
-    -- j = i0 ⊢ f .snd
-    -- j = i1 ⊢ g .snd
-    -- i = i0 ⊢ CubicalHott.Lemma3-5-1.goal isPropIsEquiv f g
-    --          (cong (λ r → fst r) f≡g) j j
-    -- i = i1 ⊢ f≡g j .snd
+--   fg : section (corollary f g) (cong fst)
+--   -- Trying to prove that producing full f ≡ g after discarding the second half still produces the original
+--   -- However, no matter what the original is, the isEquiv part is a mere prop
+--   fg f≡g i j = fst (f≡g j) , {!   !} where
+--     -- isEquiv (fst (f≡g j))
+--     -- ———— Boundary (wanted) —————————————————————————————————————
+--     -- j = i0 ⊢ f .snd
+--     -- j = i1 ⊢ g .snd
+--     -- i = i0 ⊢ CubicalHott.Lemma3-5-1.goal isPropIsEquiv f g
+--     --          (cong (λ r → fst r) f≡g) j j
+--     -- i = i1 ⊢ f≡g j .snd
 
-  gf : retract (corollary f g) (cong fst)
-  gf x = refl
+--   gf : retract (corollary f g) (cong fst)
+--   gf x = refl
diff --git a/src/CubicalHott/Lemma8-3-1.agda b/src/CubicalHott/Lemma8-3-1.agda
index 600c3a4..5da3b24 100644
--- a/src/CubicalHott/Lemma8-3-1.agda
+++ b/src/CubicalHott/Lemma8-3-1.agda
@@ -14,12 +14,13 @@ open import Cubical.Homotopy.Loopspace
 open import Cubical.HITs.SetTruncation
 
 
-helper : ∀ {l : Level} → (n : ℕ) → (A∙ @ (A , a) : Pointed l)
+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 zero A∙@(A , a) prf = refl , {!   !}
 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
+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 = {!   !} 
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda
index 8e99cf2..de1ca70 100644
--- a/src/CubicalHott/Theorem7-1-11.agda
+++ b/src/CubicalHott/Theorem7-1-11.agda
@@ -7,6 +7,8 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Core.Glue
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+open import Cubical.Functions.Embedding
 open import Cubical.Foundations.Univalence
 open import Cubical.Data.Nat
 open import Data.Unit
@@ -17,60 +19,97 @@ open import CubicalHott.Theorem7-1-8 renaming (theorem to theorem7-1-8)
 open import CubicalHott.Theorem7-1-10 renaming (theorem to theorem7-1-10)
 open import CubicalHott.HLevels
 
+lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
+lemma {l = l} zero = goal2 where
+  eqv : (x y : TypeOfHLevel l zero) → fst x ≡ fst y
+  eqv x y = ua (isoToEquiv (iso (λ _ → fst (snd y)) (λ _ → fst (snd x)) (snd (snd y)) (snd (snd x))))
+
+  goal2 : isProp (TypeOfHLevel l zero)
+  goal2 x y = lemma3-5-1 (λ _ → theorem7-1-10 zero) x y (eqv x y)
+
+lemma {l = l} (suc zero) x @ (X , Xprop) y @ (Y , Yprop) = goal1 where
+  IH : isProp (TypeOfHLevel l 0)
+  IH = lemma zero
+
+  goal1 : isProp (x ≡ y)
+  goal1 p q = {!   !}
+
+lemma {l = l} (suc (suc n)) x @ (X , px) y @ (Y , py) p q = {!   !} where
+  IH : isOfHLevel (suc (suc n)) (TypeOfHLevel l (suc n))
+  IH = lemma (suc n)
+
+  goal2 : isEmbedding {A = X ≃ Y} {B = X → Y} fst
+  goal2 x≃y1 x≃y2 = isoToIsEquiv (iso (cong fst) g (λ _ → refl) gf) where
+    g : fst x≃y1 ≡ fst x≃y2 → x≃y1 ≡ x≃y2
+    g = lemma3-5-1 isPropIsEquiv x≃y1 x≃y2
+
+    gf : retract (cong fst) g
+    gf p i j = fst (p j) , {!   !}
+
+
 helper : ∀ {l} → (n : HLevel) → isOfHLevel' (suc n) (TypeOfHLevel l n)
-helper zero TA @ (A , a , Acontr) TB @ (B , b , Bcontr) =
-  (λ i → A≡B i , goal2 i) , goal6 where
-    eqv1 : A ≃ B
-    eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
-    A≡B : A ≡ B
-    A≡B = ua eqv1
-    a≡b : PathP (λ i → A≡B i) a b
-    a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
+helper {l = l} zero = goal1 where
+  eqv : (x y : TypeOfHLevel l zero) → fst x ≡ fst y
+  eqv x y = ua (isoToEquiv (iso (λ _ → fst (snd y)) (λ _ → fst (snd x)) (snd (snd y)) (snd (snd x))))
 
-    goal2 : PathP (λ i → isContr (A≡B i)) (a , Acontr) (b , Bcontr)
-    goal3 : subst isContr A≡B (a , Acontr) ≡ (b , Bcontr)
-    goal2 = toPathP goal3
-    goal4 : (x : B) → isProp ((y : B) → x ≡ y)
-    goal3 = lemma3-5-1 goal4 (subst isContr A≡B (a , Acontr)) (b , Bcontr) (fromPathP a≡b)
-    goal5 : isSet B
-    goal4 x f1 f2 = funExt λ (y : B) → goal5 x y (f1 y) (f2 y)
-    goal5 = isProp→isSet (isContr→isProp (b , Bcontr))
+  goal2 : isProp (TypeOfHLevel l zero)
+  goal2 x y = lemma3-5-1 (λ _ → theorem7-1-10 zero) x y (eqv x y)
 
-    goal6 : (q : TA ≡ TB) → (λ i → A≡B i , goal2 i) ≡ q
-    goal6 q = {!   !}
-
-  -- A≡B i , goal i where
-  --   -- isContr (A≡B i)
-  --   -- Acontr ≡ Bcontr
-
-  --   -- A≡B i , a≡b i , λ y j → wtf i y j where
-  --   eqv1 : A ≃ B
-  --   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
-
-  --   A≡B : A ≡ B
-  --   A≡B = ua eqv1
-
-  --   a≡b : PathP (λ i → A≡B i) a b
-  --   a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
-
-  --   helper3 : (x : B) → isProp ((y : B) → x ≡ y)
-  --   helper3 x f1 f2 =
-  --     let helper = isProp→isSet (isContr→isProp (b , Bcontr)) in
-  --     funExt (λ (y : B) → helper x y (f1 y) (f2 y))
-
-  --   helper2 : subst isContr A≡B (a , Acontr) ≡ (b , Bcontr)
-  --   helper2 = lemma3-5-1 helper3 (subst isContr A≡B (a , Acontr)) (b , Bcontr) (fromPathP a≡b)
-
-  --   goal : PathP (λ i → isContr (A≡B i)) (a , Acontr) (b , Bcontr)
-  --   goal = toPathP helper2
+  goal1 : (x y : TypeOfHLevel l zero) → isContr (x ≡ y)
+  goal1 = Prop1 (TypeOfHLevel l zero) goal2
 
 helper {l = l} (suc n) (X , px) (Y , py) p q = {!   !} where
-  goal1 : ((X , px) ≡ (Y , py)) ≃ (X ≃ Y)
-  goal1 = let z = pathToEquiv {!   !} in {! !}
+  goal1 : {n : ℕ} → ((X , px) : TypeOfHLevel l n) → ((Y , py) : TypeOfHLevel l n)
+    → ((X , px) ≡ (Y , py)) ≃ (X ≃ Y)
+  goal1 {n = n} (X , px) (Y , py) =
+    (X , px) ≡ (Y , py) ≃⟨ isoToEquiv (iso f g (λ _ → refl) gf) ⟩
+    X ≡ Y ≃⟨ univalence ⟩
+    X ≃ Y ■ where
+      f : (X , px) ≡ (Y , py) → X ≡ Y
+      f = cong fst
+
+      g : X ≡ Y → (X , px) ≡ (Y , py)
+      g p = lemma3-5-1 (λ x → theorem7-1-10 n) (X , px) (Y , py) p
+
+      gf : retract f g
+      gf p i j = fst (p j) , {!   !}
+        where
+          wtf =
+            let z1 = helper n (X , px) (Y , py) in
+            let z2 = isOfHLevel'→isOfHLevel n ((X , px) ≡ (Y , py)) z1 in
+            {!   !}
+          prop-helper : isProp (isOfHLevel n Y)
+          prop-helper = theorem7-1-10 n
+  
+  goal2 : isEmbedding {A = X ≃ Y} {B = X → Y} fst
+  goal2 x≃y1 x≃y2 = isoToIsEquiv (iso (cong fst) g (λ _ → refl) gf) where
+    g : fst x≃y1 ≡ fst x≃y2 → x≃y1 ≡ x≃y2
+    g = lemma3-5-1 isPropIsEquiv x≃y1 x≃y2
+
+    gf : retract (cong fst) g
+    gf p i j = fst (p j) , {!   !}
+      -- Goal here is to use toPathP, convert them both
+
+      -- isEquiv (fst (p j))
+      -- ———— Boundary (wanted) —————————————————————————————————————
+      -- j = i0 ⊢ x≃y1 .snd
+      -- j = i1 ⊢ x≃y2 .snd
+      -- i = i0 ⊢ CubicalHott.Lemma3-5-1.goal isPropIsEquiv x≃y1 x≃y2
+      --          (cong (λ r → fst r) p) j j
+      -- i = i1 ⊢ p j .snd
+
+    -- toPathP {A = {!   !}} z j where
+      -- z : transport (λ i → isEquiv (fst (p i))) (snd x≃y1) ≡ snd x≃y2
+      -- z = isPropIsEquiv (fst x≃y2) (subst (λ x → isEquiv (fst x)) p (snd x≃y1)) (snd x≃y2)
+
+  goal3 : isOfHLevel n (X → Y)
+  goal3 = theorem7-1-6 {!   !} goal2 {! suc n  !} {!   !} {!   !}
+
+  goal4 : isOfHLevel n (p ≡ q)
+  goal4 = {!   !}
+
 
 
-lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
-lemma {l = l} n = isOfHLevel'→isOfHLevel (suc n) (TypeOfHLevel l n) (helper n)
 
 --     -- -- eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
 --     -- -- eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y
@@ -156,3 +195,4 @@ lemma {l = l} (suc zero) (A , A-prop) (B , B-prop) p q i j = {!   !} , {!   !} w
 -- --     -- (glue (λ { (i = i1) → {!   !} }) {!   !})
 -- --     -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b))
 -- -- lemma (suc n) x y = {!   !}
+   
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem7-1-9.agda b/src/CubicalHott/Theorem7-1-9.agda
index deffcc3..c344836 100644
--- a/src/CubicalHott/Theorem7-1-9.agda
+++ b/src/CubicalHott/Theorem7-1-9.agda
@@ -22,6 +22,7 @@ theorem (suc zero) prf f1 f2 i x =
   result i
 theorem {A = A} {B = B} (2+ n) prf f1 f2 =
   subst (isOfHLevel (suc n)) funExtPath (theorem (suc n) λ a → prf a (f1 a) (f2 a))
+
   -- goal1 where
   -- goal1 : isOfHLevel (suc n) (f1 ≡ f2)
   -- goal2 : isOfHLevel (suc n) ((a : A) → f1 a ≡ f2 a)
diff --git a/src/CubicalHott/Theorem7-2-2.agda b/src/CubicalHott/Theorem7-2-2.agda
index 6d922df..be5d13d 100644
--- a/src/CubicalHott/Theorem7-2-2.agda
+++ b/src/CubicalHott/Theorem7-2-2.agda
@@ -11,4 +11,5 @@ theorem : {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
+theorem R f1 f2 x y p q =
+  {!   !}
\ No newline at end of file
diff --git a/src/ThesisWork/LES.agda b/src/ThesisWork/LES.agda
deleted file mode 100644
index 8c7ef97..0000000
--- a/src/ThesisWork/LES.agda
+++ /dev/null
@@ -1,93 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module ThesisWork.LES where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Pointed
-open import Cubical.Foundations.Equiv
-open import Data.Nat
-open import Data.Fin
-open import Data.Product
-open import Cubical.Homotopy.Base
-open import Cubical.Homotopy.Loopspace
-open import Cubical.Homotopy.Group.Base
-open import Cubical.Homotopy.Group.LES
-open import Cubical.HITs.SetTruncation renaming (map to mapTrunc)
-open import Cubical.HITs.SetTruncation.Fibers
-
-private
-  variable
-    X Y : Type
-
-LES-node : ∀ {l} → {X Y : Pointed l} → (f : X →∙ Y) → ℕ × Fin 3 → Type l
-LES-node {Y = Y} f (n , zero) = π n Y
-LES-node {X = X} f (n , suc zero) = π n X
-LES-node {X = (X , x)} {Y = (Y , y)} (f , f-eq) (n , suc (suc zero)) =
-    let F = fiber f y in
-    π n (F , x , f-eq)
-
-sucF : ℕ × Fin 3 → ℕ × Fin 3
-sucF (n , zero) = n , suc zero
-sucF (n , suc zero) = n , suc (suc zero)
-sucF (n , suc (suc zero)) = suc n , zero
-
-LES-edge : ∀ {l} → {X∙ Y∙ : Pointed l} → (f∙ : X∙ →∙ Y∙) → (n : ℕ × Fin 3)
-    → LES-node f∙ (sucF n) → LES-node f∙ n
-LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , zero) = h n where
-    h1 : ∀ (n : ℕ) → (Ω^ n) X∙ →∙ (Ω^ n) Y∙
-    h1 zero = f∙
-    h1 (suc n) = (λ x → refl) , helper where
-        helper : refl ≡ snd (Ω ((Ω^ n) Y∙))
-        helper i j = (Ω^ n) (Y , y) .snd
-
-        -- helper = λ i j →
-        --     let
-        --         top : (Ω^ n) (Y , y) .fst
-        --         top = {!  refl !}
-        --         u = λ k → λ where
-        --             (i = i0) → {!   !}
-        --             (i = i1) → {!   !}
-        --             (j = i0) → {!   !}
-        --             (j = i1) → {!   !}
-        --     in hcomp u {!   !}
-
-    h : ∀ (n : ℕ) → π n X∙ → π n Y∙
-    h n = mapTrunc (fst (h1 n))
-
-    -- h zero ∣ a ∣₂ = ∣ f a ∣₂
-    -- h (suc n) ∣ a ∣₂ = let IH = h n ∣ a i0 ∣₂ in ∣ {!   !} ∣₂
-    -- h zero (squash₂ a b p q i j) = squash₂ (h 0 a) (h 0 b) (cong (h 0) p) (cong (h 0) q) i j
-    -- h (suc n) (squash₂ a b p q i j) = {!   !}
-
-LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , suc zero) = h n where
-    F = fiber f y
-    
-    h1 : ∀ (n : ℕ) → (Ω^ n) (F , x , f-eq) →∙ (Ω^ n) X∙
-    h1 zero = fst , refl
-    h1 (suc n) = (λ f i → (Ω^ n) (X , x) .snd) , λ i j → (Ω^ n) (X , x) .snd
-
-    h : ∀ (n : ℕ) → π n (F , x , f-eq) → π n X∙
-    h n = mapTrunc (fst (h1 n))
-
-LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , suc (suc zero)) = h n where
-    F = fiber f y
-
-    h1 : ∀ (n : ℕ) → (Ω^ (suc n)) Y∙ →∙ (Ω^ n) (F , x , f-eq)
-    h1 zero = (λ y → x , f-eq) , refl
-    h1 (suc n) = (λ y i → (Ω^ n) (F , x , f-eq) .snd) , λ i j → (Ω^ n) (F , x , f-eq) .snd
-
-    h : ∀ (n : ℕ) → π (suc n) Y∙ → π n (F , x , f-eq)
-    h n = mapTrunc (fst (h1 n))
-
--- LES-edge f n_ with mapN n_
--- LES-edge {X = X∙ @ (X , x)} {Y = Y∙ @ (Y , y)} f n_ | (n , zero) = {! h  !} where
---     h : π n X∙ → π n Y∙
---     h ∣ x ∣₂ = ∣ {!   !} ∣₂
---     h (squash₂ z z₁ p q i i₁) = {!   !}
---     -- z : LES-node f (mapN (suc n_))
---     -- z : π n X
---     -- z : ∥ typ ((Ω^ 0) X) ∥₂
---     -- z : ∥ typ X ∥₂
---     -- z : ∥ typ X ∥₂
--- LES-edge f n_ | (n , suc zero) = λ z → {!   !}       
--- LES-edge f n_ | (n , suc (suc zero)) = λ z → {!   !} 
\ No newline at end of file