diff --git a/src/CubicalHott/Lemma6-10-2.agda b/src/CubicalHott/Lemma6-10-2.agda
index ae0d1d8..965058a 100644
--- a/src/CubicalHott/Lemma6-10-2.agda
+++ b/src/CubicalHott/Lemma6-10-2.agda
@@ -3,6 +3,7 @@
 module CubicalHott.Lemma6-10-2 where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
 open import Cubical.Functions.Surjection
 open import Cubical.HITs.SetQuotients
 open import Cubical.HITs.PropositionalTruncation
@@ -14,4 +15,9 @@ private
 lemma : (A : Type l) (R : A → A → Type l)
   → (q : A → A / R)
   → isSurjection q
-lemma {l} A R q x = {!   !}
+lemma {l} A R q x = elimProp f1 f2 x where
+  f1 : (z : A / R) → isProp ∥ fiber q x ∥₁
+  f1 z x y = {!   !}
+
+  f2 : (a : A) → ∥ fiber q x ∥₁
+  f2 a = ∣ (a , {!   !}) ∣₁
diff --git a/src/CubicalHott/Lemma7-2-8.agda b/src/CubicalHott/Lemma7-2-8.agda
new file mode 100644
index 0000000..f5549d2
--- /dev/null
+++ b/src/CubicalHott/Lemma7-2-8.agda
@@ -0,0 +1,13 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma7-2-8 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Data.Nat
+
+lemma : {n : ℕ} → {X : Type}
+  → ((x : X) → isOfHLevel (suc n) X)
+  → isOfHLevel (suc n) X
+lemma {zero} {X} f x y = f x x y 
+lemma {suc n} {X} f x y = f x x y
\ No newline at end of file
diff --git a/src/CubicalHott/Lemma7-3-1.agda b/src/CubicalHott/Lemma7-3-1.agda
index 513a5ac..fc860f5 100644
--- a/src/CubicalHott/Lemma7-3-1.agda
+++ b/src/CubicalHott/Lemma7-3-1.agda
@@ -4,8 +4,13 @@ module CubicalHott.Lemma7-3-1 where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Data.Unit
 open import Cubical.HITs.Truncation
-open import Data.Nat
+open import Cubical.Data.Nat
 
 lemma : {A : Type} → (n : ℕ) → isOfHLevel n (∥ A ∥ n)
-lemma {A} n = {!   !}
\ No newline at end of file
+lemma {A} zero = tt* , helper where
+  helper : (y : ∥ A ∥ zero) → tt* ≡ y
+  helper tt* = refl
+lemma {A} (suc zero) x y = {!   !}
+lemma {A} (suc (suc n)) = {!   !}
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem3-2-2.agda b/src/CubicalHott/Theorem3-2-2.agda
new file mode 100644
index 0000000..bb0a80c
--- /dev/null
+++ b/src/CubicalHott/Theorem3-2-2.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem3-2-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Nat
+open import Cubical.Data.Bool
+
+-- Trying to give a cubical interpretation of this
+
+theorem : ¬ ((A : Type) → (¬ (¬ A) → A))
+theorem f = {!   !} where
+  apdfp : PathP (λ i → ¬ ¬ notEq i → notEq i) (f Bool) (f Bool)
+  apdfp = congP (λ i A → {! ¬ ¬ A → A  !}) notEq
+
+  u : ¬ ¬ Bool
+  u = λ p → p true
+
+  -- foranyu : PathP (λ i → {!   !}) (fbool u) (fbool u)
+  -- foranyu i = {!  apdfp i u !}
+  
diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda
index 0826a80..e6cbac1 100644
--- a/src/CubicalHott/Theorem7-1-11.agda
+++ b/src/CubicalHott/Theorem7-1-11.agda
@@ -73,9 +73,13 @@ lemma zero (A , a , Acontr) (B , b , Bcontr) i =
     --       in hfill u (inS (a≡b {! j  !})) j
     --   in {!   !}
 
-lemma (suc zero) (A , A-prop) (B , B-prop) p q =
-  let IH = lemma zero 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 {!   !}
+  -- overall goal is p ≡ q
+  -- p : (A , A-prop) ≡ (B , B-prop) where both are type Σ Type isProp
+  -- q : (A , A-prop) ≡ (B , B-prop)
+
+  -- cong_fst(p) : A ≡ B
 
 lemma (suc (suc n)) x y p q =
   let IH = lemma (suc n) in
diff --git a/src/CubicalHott/Theorem7-2-7.agda b/src/CubicalHott/Theorem7-2-7.agda
new file mode 100644
index 0000000..53b2799
--- /dev/null
+++ b/src/CubicalHott/Theorem7-2-7.agda
@@ -0,0 +1,17 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-2-7 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+open import Cubical.Homotopy.Loopspace
+open import Data.Nat
+
+open import CubicalHott.Lemma7-2-8 renaming (lemma to lemma7-2-8)
+
+theorem : {n : ℕ} → {X : Type}
+  → ((x : X) → isOfHLevel (suc n) (typ (Ω (X , x))))
+  → isOfHLevel (suc (suc n)) X
+theorem {n} {X} f x y =
+  lemma7-2-8 λ p → J (λ y' p' → isOfHLevel (suc n) (x ≡ y')) (f x) p
diff --git a/src/CubicalHott/Theorem7-2-9.agda b/src/CubicalHott/Theorem7-2-9.agda
new file mode 100644
index 0000000..edc4b46
--- /dev/null
+++ b/src/CubicalHott/Theorem7-2-9.agda
@@ -0,0 +1,20 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-2-9 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Structure
+open import Cubical.Homotopy.Loopspace
+open import Cubical.Data.Nat
+
+open import CubicalHott.Exercise3-5 renaming (exercise to exercise3-5)
+open import CubicalHott.Theorem7-2-1 renaming (forwards to theorem7-2-1)
+
+theorem : {n : ℕ} → {A : Type}
+  → ((a : A) → isContr (typ ((Ω^ suc (suc n)) (A , a))))
+  → isOfHLevel (suc n) A
+theorem {zero} f = invEq exercise3-5 λ x → x , λ y → {!   !}
+theorem {suc zero} f = theorem7-2-1 (λ x p → let z = snd (f x) in {!   !}) 
+theorem {suc (suc n)} f x y = {!   !} 
\ No newline at end of file
diff --git a/src/Misc/FiveLemma.agda b/src/Misc/FiveLemma.agda
new file mode 100644
index 0000000..a287655
--- /dev/null
+++ b/src/Misc/FiveLemma.agda
@@ -0,0 +1,88 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma where
+
+open import Agda.Primitive
+open import Cubical.Data.Sigma
+open import Cubical.Categories.Abelian
+open import Cubical.Categories.Additive
+open import Cubical.Categories.Category
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Functions.Embedding
+open import Cubical.Functions.Surjection
+
+private
+  variable
+    ℓ ℓ' : Level
+
+-- kernel : {l : Level} → {A B : Pointed l} → (f : A →∙ B) → Type l
+-- kernel {l} {A = A @ A , a} {B = B @ B , b} (f , f-eq) =
+--   -- all elements of A that map to the base point b of B
+--   Σ A λ a → f a ≡ b
+
+-- image : {l : Level} → {A B : Pointed l} → (f : A →∙ B) → Type l
+-- image {l} {A = A @ A , a} {B = B @ B , b} (f , f-eq) =
+--   -- all elements of B such that
+--   Σ B (λ b →
+--     -- there exists some A such that f(a) is b
+--     Σ A λ a → f a ≡ b
+--   )
+
+-- module _ (C : Category ℓ ℓ') where
+--   open Category C
+
+--   module _ {x y : ob} where
+
+--     record IsImage {i : ob} (f : Hom[ x , y ]) (m : Hom[ i , y ]) : Type (ℓ-max ℓ ℓ') where
+--       field
+--         e : Hom[ x , i ]
+--         req1 : f ≡ (_⋆_ e m)
+--         req2 : (i' : ob) → (e' : Hom[ x , i' ]) → (m' : Hom[ i' , y ]) → f ≡ (_⋆_ e' m')
+--           → ∃![ v ∈ Hom[ i , i' ] ] (m ≡ (_⋆_ v m'))
+
+
+--     record Image (f : Hom[ x , y ]) : Type (ℓ-max ℓ ℓ') where
+--       field
+--         i : ob
+--         m : Hom[ i , y ]
+--         isIm : IsImage f m
+
+--   im : ∀ {x y : ob} → (f : Hom[ x , y ]) → Image f
+--   im {x} {y} f = record { i = {!   !} ; m = {!   !} ; isIm = {!   !} }
+
+module fiveLemma (AC : AbelianCategory ℓ ℓ') where
+  open AbelianCategory AC
+
+  module _
+    (A B C D E A' B' C' D' E' : ob)
+    (f : Hom[ A , B ])
+    (g : Hom[ B , C ])
+    (h : Hom[ C , D ])
+    (j : Hom[ D , E ])
+    (l : Hom[ A , A' ])
+    (m : Hom[ B , B' ])
+    (n : Hom[ C , C' ])
+    (p : Hom[ D , D' ])
+    (q : Hom[ E , E' ])
+    (r : Hom[ A' , B' ])
+    (s : Hom[ B' , C' ])
+    (t : Hom[ C' , D' ])
+    (u : Hom[ D' , E' ])
+    (fgExact : ker g ≃ ?)
+    where
+      z = let z1 = ker f in {!   !}
+        -- lemma : isExact f g → isExact g h → isExact h j
+        --   → isExact r s → isExact s t → isExact t u
+        --   → isSurjection (fst l) → isEquiv (fst m) → isEquiv (fst p) → isEmbedding (fst q)
+        --   → isEquiv (fst n)
+        -- lemma fgIsExact ghIsExact hjIsExact rsIsExact stIsExact tuIsExact lIsSurjection mIsEquiv pIsEquiv qIsInjection =
+        --   isEmbedding×isSurjection→isEquiv (nIsEmbedding , nIsSurjection) where
+        --     nIsEmbedding : isEmbedding (fst n)
+        --     nIsEmbedding c1 c2 = {!   !}
+
+        --     nIsSurjection : isSurjection (fst n)
+        --     nIsSurjection b = {!   !} 
\ No newline at end of file
diff --git a/src/Misc/SnakeLemma.agda b/src/Misc/SnakeLemma.agda
new file mode 100644
index 0000000..6cc9a42
--- /dev/null
+++ b/src/Misc/SnakeLemma.agda
@@ -0,0 +1,4 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.SnakeLemma where
+