diff --git a/src/CubicalHott/HLevels.agda b/src/CubicalHott/HLevels.agda
new file mode 100644
index 0000000..1cc7e90
--- /dev/null
+++ b/src/CubicalHott/HLevels.agda
@@ -0,0 +1,40 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.HLevels where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+open import Data.Nat
+
+isOfHLevel' : ∀ {ℓ : Level} → ℕ → Type ℓ → Type ℓ
+isOfHLevel' 0 A = isContr A
+isOfHLevel' (suc n) A = (x y : A) → isOfHLevel' n (x ≡ y)
+
+TypeOfHLevel' : ∀ ℓ → HLevel → Type (ℓ-suc ℓ)
+TypeOfHLevel' ℓ n = TypeWithStr ℓ (isOfHLevel' n)
+
+isOfHLevel→isOfHLevel' : ∀ {l : Level} → (n : ℕ) → (A : Type l)
+  → isOfHLevel n A → isOfHLevel' n A
+isOfHLevel→isOfHLevel' zero A z = z
+isOfHLevel→isOfHLevel' (suc zero) A z =
+  λ x y → (z x y) , λ q → isProp→isSet z x y (z x y) q
+isOfHLevel→isOfHLevel' (suc (suc n)) A z =
+  λ x y p q → isOfHLevel→isOfHLevel' (suc n) (x ≡ y) (z x y) p q
+
+isOfHLevel'→isOfHLevel : ∀ {l : Level} → (n : ℕ) → (A : Type l)
+  → isOfHLevel' n A → isOfHLevel n A
+isOfHLevel'→isOfHLevel zero A z = z 
+isOfHLevel'→isOfHLevel (suc zero) A z =
+  λ x y → let z1 = z x y in fst z1 
+isOfHLevel'→isOfHLevel (suc (suc n)) A z =
+  λ x y →
+    let IHf = λ p q → z x y p q in
+    let IH = isOfHLevel'→isOfHLevel (suc n) (x ≡ y) IHf in
+    IH
+
+TypeOfHLevel→TypeOfHLevel' : ∀ (l : Level) → (n : ℕ) → TypeOfHLevel l n → TypeOfHLevel' l n
+TypeOfHLevel→TypeOfHLevel' l n (T , T-n-type) = T , isOfHLevel→isOfHLevel' n T T-n-type
+
+TypeOfHLevel'→TypeOfHLevel : ∀ (l : Level) → (n : ℕ) → TypeOfHLevel' l n → TypeOfHLevel l n
+TypeOfHLevel'→TypeOfHLevel l n (T , T-n-type) = T , isOfHLevel'→isOfHLevel n T T-n-type
\ No newline at end of file
diff --git a/src/CubicalHott/Lemma3-5-1.agda b/src/CubicalHott/Lemma3-5-1.agda
index 0dc936e..784eb24 100644
--- a/src/CubicalHott/Lemma3-5-1.agda
+++ b/src/CubicalHott/Lemma3-5-1.agda
@@ -3,6 +3,9 @@
 module CubicalHott.Lemma3-5-1 where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
 
 lemma : {l l2 : Level} → {A : Type l} → {P : A → Type l2}
   → ((x : A) → isProp (P x))
@@ -12,4 +15,34 @@ lemma : {l l2 : Level} → {A : Type l} → {P : A → Type l2}
 lemma {P = P} Px-isProp u v p i = p i , goal i where
   goal : PathP (λ i → P (p i)) (snd u) (snd v)
   goal = toPathP (Px-isProp (fst v) (subst P p (snd u)) (snd v))
-  
\ No newline at end of file
+  
+corollary : {l : Level} → {A B : Type l}
+  → (f g : A ≃ B)
+  → fst f ≡ fst g
+  → 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)
+
+  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
+
+  gf : retract (corollary f g) (cong fst)
+  gf x = refl
diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda
index e6cbac1..8e99cf2 100644
--- a/src/CubicalHott/Theorem7-1-11.agda
+++ b/src/CubicalHott/Theorem7-1-11.agda
@@ -11,67 +11,97 @@ open import Cubical.Foundations.Univalence
 open import Cubical.Data.Nat
 open import Data.Unit
 
-open import CubicalHott.Lemma3-5-1 renaming (lemma to lemma3-5-1)
+open import CubicalHott.Lemma3-5-1 renaming (lemma to lemma3-5-1; corollary to corollary3-5-1)
+open import CubicalHott.Theorem7-1-6 renaming (theorem to theorem7-1-6)
 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 zero (A , a , Acontr) (B , b , Bcontr) i =
-  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
+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
 
-    helper2 : (x : B) → isProp ((y : B) → x ≡ y)
-    helper2 x f1 f2 =
-      let helper = isProp→isSet (isContr→isProp (b , Bcontr)) in
-      funExt (λ (y : B) → helper x y (f1 y) (f2 y))
+    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))
 
-    helper : subst isContr A≡B (a , Acontr) ≡ (b , Bcontr)
-    helper = lemma3-5-1 helper2 (subst isContr A≡B (a , Acontr)) (b , Bcontr) (fromPathP a≡b)
+    goal6 : (q : TA ≡ TB) → (λ i → A≡B i , goal2 i) ≡ q
+    goal6 q = {!   !}
 
-    goal : PathP (λ i → isContr (A≡B i)) (a , Acontr) (b , Bcontr)
-    goal = toPathP helper
+  -- A≡B i , goal i where
+  --   -- isContr (A≡B i)
+  --   -- Acontr ≡ Bcontr
 
-    -- -- eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
-    -- -- eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y
+  --   -- A≡B i , a≡b i , λ y j → wtf i y j where
+  --   eqv1 : A ≃ B
+  --   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
 
-    -- -- T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
-    -- -- e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
-    -- -- Uhh = primGlue ((y : B) → b ≡ y) T1 e1
+  --   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
+
+helper {l = l} (suc n) (X , px) (Y , py) p q = {!   !} where
+  goal1 : ((X , px) ≡ (Y , py)) ≃ (X ≃ Y)
+  goal1 = let z = pathToEquiv {!   !} in {! !}
+
+
+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
+
+--     -- -- T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
+--     -- -- e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
+--     -- -- Uhh = primGlue ((y : B) → b ≡ y) T1 e1
         
-    -- -- uhh : Uhh
-    -- -- uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) λ y j → {! Bcontr y j  !}
+--     -- -- uhh : Uhh
+--     -- -- uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) λ y j → {! Bcontr y j  !}
 
-    -- Acontr-is-Prop : isProp ((y : A) → a ≡ y)
+--     -- Acontr-is-Prop : isProp ((y : A) → a ≡ y)
 
-    -- wtf : PathP (λ i → (y : A≡B i) → a≡b i ≡ y) Acontr Bcontr
-    -- wtf = λ i y j → {!   !}
+--     -- wtf : PathP (λ i → (y : A≡B i) → a≡b i ≡ y) Acontr Bcontr
+--     -- wtf = λ i y j → {!   !}
 
 
-    --   -- a≡b i ≡ y
-    --   -- ———— Boundary (wanted) —————————————————————————————————————
-    --   -- i = i0 ⊢ λ i₁ → Acontr y i₁
-    --   -- i = i1 ⊢ λ i₁ → Bcontr y i₁
+--     --   -- a≡b i ≡ y
+--     --   -- ———— Boundary (wanted) —————————————————————————————————————
+--     --   -- i = i0 ⊢ λ i₁ → Acontr y i₁
+--     --   -- i = i1 ⊢ λ i₁ → Bcontr y i₁
 
-    -- z = let
-    --     z1 = λ (y : A≡B i) (j : I) →
-    --       let u = λ k → λ where
-    --         (i = i0) → Acontr y (~ j)
-    --         (i = i1) → Bcontr y j
-    --         (j = i0) → a≡b i
-    --         (j = i1) → {!  y i !}
-    --       in hfill u (inS (a≡b {! j  !})) j
-    --   in {!   !}
+--     -- z = let
+--     --     z1 = λ (y : A≡B i) (j : I) →
+--     --       let u = λ k → λ where
+--     --         (i = i0) → Acontr y (~ j)
+--     --         (i = i1) → Bcontr y j
+--     --         (j = i0) → a≡b i
+--     --         (j = i1) → {!  y i !}
+--     --       in hfill u (inS (a≡b {! j  !})) j
+--     --   in {!   !}
 
 lemma {l = l} (suc zero) (A , A-prop) (B , B-prop) p q i j = {!   !} , {!   !} where
   z1 = let z = lemma {l = l} zero in {!   !}
@@ -81,35 +111,48 @@ lemma {l = l} (suc zero) (A , A-prop) (B , B-prop) p q i j = {!   !} , {!   !} w
 
   -- cong_fst(p) : A ≡ B
 
-lemma (suc (suc n)) x y p q =
-  let IH = lemma (suc n) in
-  {!   !}
+--   -- we know that A ≡ B in two different ways
+--   -- if A is a prop, then (x y : A) → x ≡ y
+--   -- if A is empty, then B is also empty
+--   -- but we can't choose a contractible center (no AOC)
+  
+--   -- "for any two proofs that A ≡ B and that A-prop ≡ B-prop"
+--   -- p : (A , A-prop) ≡ (B , B-prop)
+--   -- p = λ i → <something s.t at i=0, returns A , A-prop>
+--   -- so (p i0) : Σ Type isProp = (A , A-prop)
+--   -- p ≡_{Σ Type isProp} q
+--   -- through lemma 3.5.1, if the isProp is a prop for every type, then we only have to compare the Type
+--   -- 
+--   {!   !}
 
--- lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
--- lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where
+-- lemma (suc (suc n)) x y p q =
+--   let IH = lemma (suc n) in
+--   {!   !}
 
---   eqv1 : A ≃ B
---   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
+-- -- lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
+-- -- lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where
 
---   T = λ { (i = i0) → A ; (i = i1) → B }
---   e = λ { (i = i0) → eqv1 ; (i = i1) → idEquiv B }
+-- --   eqv1 : A ≃ B
+-- --   eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
 
---   G = primGlue B T e
---   g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b
+-- --   T = λ { (i = i0) → A ; (i = i1) → B }
+-- --   e = λ { (i = i0) → eqv1 ; (i = i1) → idEquiv B }
 
---   -- at i = i0, y = a
---   -- at i = i1, y = b
+-- --   G = primGlue B T e
+-- --   g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b
 
---   -- For some arbitrary y : G, prove g ≡ y
---   contr : (y : G) → g ≡ y
---   contr y j = {!   !}
---     -- let p = λ where
---     --   (i = i0) → {!   !} -- Acontr (unglue {A = A} (~ i) {T = T} {e = λ { (i = i0) → idEquiv A }} y) j
---     --   (i = i1) → Bcontr (unglue {A = B} i {T = T} {e = λ { (i = i1) → idEquiv B }} y) j
---     -- in glue p (Bcontr {! g  !} {! j  !})
+-- --   -- at i = i0, y = a
+-- --   -- at i = i1, y = b
 
---     -- unglue i {!   !}
---     -- (glue (λ { (i = i1) → {!   !} }) {!   !})
---     -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b))
--- lemma (suc n) x y = {!   !}
-     
\ No newline at end of file
+-- --   -- For some arbitrary y : G, prove g ≡ y
+-- --   contr : (y : G) → g ≡ y
+-- --   contr y j = {!   !}
+-- --     -- let p = λ where
+-- --     --   (i = i0) → {!   !} -- Acontr (unglue {A = A} (~ i) {T = T} {e = λ { (i = i0) → idEquiv A }} y) j
+-- --     --   (i = i1) → Bcontr (unglue {A = B} i {T = T} {e = λ { (i = i1) → idEquiv B }} y) j
+-- --     -- in glue p (Bcontr {! g  !} {! j  !})
+
+-- --     -- unglue i {!   !}
+-- --     -- (glue (λ { (i = i1) → {!   !} }) {!   !})
+-- --     -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b))
+-- -- lemma (suc n) x y = {!   !}
diff --git a/src/CubicalHott/Theorem7-1-6.agda b/src/CubicalHott/Theorem7-1-6.agda
index 7f53c93..c9cab8d 100644
--- a/src/CubicalHott/Theorem7-1-6.agda
+++ b/src/CubicalHott/Theorem7-1-6.agda
@@ -9,7 +9,7 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Functions.Embedding
 open import Data.Nat
 
-theorem : {X Y : Type}
+theorem : {l : Level} → {X Y : Type l}
   → (f : X → Y) → isEmbedding f
   → (n : HLevel)
   → isOfHLevel (suc n) Y → isOfHLevel (suc n) X