diff --git a/src/CubicalHott/Chapter3.agda b/src/CubicalHott/Chapter3.agda
index d590722..914330e 100644
--- a/src/CubicalHott/Chapter3.agda
+++ b/src/CubicalHott/Chapter3.agda
@@ -1,51 +1,51 @@
-{-# OPTIONS --cubical #-}
-module CubicalHott.Chapter3 where
-
-open import CubicalHott.Prelude
-open import CubicalHott.Chapter2
-open import Cubical.Data.Bool
-open import Cubical.Data.Equality using (id; ap)
-
-private
-  variable
-    l : Level
-
-module example319 where
-  lemma : ¬ isSet (Type l)
-  lemma {l} p = remark2126.lemma fatal where
-    not* : Bool* {l} → Bool* {l}
-    not* (lift false) = lift true
-    not* (lift true) = lift false
-
-    notnot* : (x : Bool* {l}) → not* (not* x) ≡ x
-    notnot* (lift true) = refl
-    notnot* (lift false) = refl
-
-    notIso* : Iso (Bool* {l}) (Bool* {l})
-    Iso.fun notIso* = not*
-    Iso.inv notIso* = not*
-    Iso.rightInv notIso* = notnot*
-    Iso.leftInv notIso* = notnot*
-
-    notEquiv* : Bool* {l} ≃ Bool* {l}
-    notEquiv* = not* , isoToIsEquiv notIso*
-
-    fPath : Bool* {ℓ = l} ≡ Bool* {ℓ = l}
-    fPath = ua notEquiv*
-
-    getFunc : Bool* ≡ Bool* → Bool* → Bool*
-    getFunc path = pathToEquiv path .fst
-    
-    left : getFunc fPath ≡ not*
-    left = cong fst (pathToEquiv-ua notEquiv*)
-
-    right : getFunc fPath ≡ id
-    right = cong getFunc (helper ∙ sym uaIdEquiv) ∙ cong fst (pathToEquiv-ua (idEquiv Bool*)) where
-      helper : fPath ≡ refl
-      helper = p Bool* Bool* fPath refl
-
-    bogus : not* ≡ id
-    bogus = sym left ∙ right
-
-    fatal : true ≡ false
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter3 where
+
+open import CubicalHott.Prelude
+open import CubicalHott.Chapter2
+open import Cubical.Data.Bool
+open import Cubical.Data.Equality using (id; ap)
+
+private
+  variable
+    l : Level
+
+module example319 where
+  lemma : ¬ isSet (Type l)
+  lemma {l} p = remark2126.lemma fatal where
+    not* : Bool* {l} → Bool* {l}
+    not* (lift false) = lift true
+    not* (lift true) = lift false
+
+    notnot* : (x : Bool* {l}) → not* (not* x) ≡ x
+    notnot* (lift true) = refl
+    notnot* (lift false) = refl
+
+    notIso* : Iso (Bool* {l}) (Bool* {l})
+    Iso.fun notIso* = not*
+    Iso.inv notIso* = not*
+    Iso.rightInv notIso* = notnot*
+    Iso.leftInv notIso* = notnot*
+
+    notEquiv* : Bool* {l} ≃ Bool* {l}
+    notEquiv* = not* , isoToIsEquiv notIso*
+
+    fPath : Bool* {ℓ = l} ≡ Bool* {ℓ = l}
+    fPath = ua notEquiv*
+
+    getFunc : Bool* ≡ Bool* → Bool* → Bool*
+    getFunc path = pathToEquiv path .fst
+    
+    left : getFunc fPath ≡ not*
+    left = cong fst (pathToEquiv-ua notEquiv*)
+
+    right : getFunc fPath ≡ id
+    right = cong getFunc (helper ∙ sym uaIdEquiv) ∙ cong fst (pathToEquiv-ua (idEquiv Bool*)) where
+      helper : fPath ≡ refl
+      helper = p Bool* Bool* fPath refl
+
+    bogus : not* ≡ id
+    bogus = sym left ∙ right
+
+    fatal : true ≡ false
     fatal = cong (λ f → lower (f (lift true))) (sym bogus) 
\ No newline at end of file
diff --git a/src/CubicalHott/Chapter6.agda b/src/CubicalHott/Chapter6.agda
index 6aaa234..1e674b6 100644
--- a/src/CubicalHott/Chapter6.agda
+++ b/src/CubicalHott/Chapter6.agda
@@ -1,103 +1,103 @@
-{-# OPTIONS --cubical #-}
-module CubicalHott.Chapter6 where
-
-open import CubicalHott.Prelude
-open import CubicalHott.Chapter3
-open import Cubical.Data.Equality.Conversion
-open import Cubical.HITs.Susp
-open import Cubical.HITs.S1
-open import Cubical.Data.Int
-open import Cubical.Data.Nat
-open import Cubical.Data.Bool
-
-private
-  variable
-    l l2 : Level
-
--- Equation 6.2.2
-
-dep-path : {A : Type} → (P : A → Type) → {x y : A} → (p : x ≡ y) → (u : P x) → (v : P y) → Type
-dep-path P p u v = subst P p u ≡ v
-
-syntax dep-path P p u v = u ≡[ P , p ] v
-
--- Lemma 6.2.5
-
-module lemma625 where
-  f : {A : Type} {a : A} {p : a ≡ a} → S¹ → A
-  f {a = a} base = a 
-  f {p = p} (loop i) = p i
-
--- Lemma 6.2.8
-
--- module lemma628 where
---   lemma : {A : Type}
---     → (f g : S¹ → A)
---     → (p : f base ≡ g base)
---     → (q : cong f loop ≡[ (λ x → x ≡ x) , p ] cong g loop)
---     → (x : S¹) → f x ≡ g x
---   lemma f g p q base i = p i 
---   lemma f g p q (loop j) i = {!   !}
-
--- Interval
-
-data [0,1] : Type where
-  ii0 : [0,1]
-  ii1 : [0,1]
-  seg : ii0 ≡ ii1
-
--- Lemma 6.3.1
-
-module lemma631 where
-  lemma : isContr [0,1]
-  lemma = ii0 , f where
-    f : (y : [0,1]) → ii0 ≡ y
-    f ii0 = refl 
-    f ii1 = seg
-    f (seg i) j = seg (i ∧ j) 
-    
--- Lemma 6.3.2
-
-module lemma632 where
-  lemma : {A B : Type}
-    → (f g : A → B)
-    → ((x : A) → f x ≡ g x)
-    → f ≡ g
-  lemma {A} {B} f g p i = q (seg i) where
-    p̃ : (x : A) → [0,1] → B
-    p̃ x ii0 = f x
-    p̃ x ii1 = g x
-    p̃ x (seg i) = p x i
-
-    q : [0,1] → (A → B)
-    q i x = p̃ x i
-    
--- Lemma 6.4.1
-
--- module lemma641 where
---   lemma : loop ≢ refl
---   lemma loop≡refl = example319.lemma g where
---     goal : {A : Type l} {x : A} {p : x ≡ x} → (q' : x ≡ x) → refl ≡ q'
---     goal {A = A} {x} {p} q' = z1 ∙ {!   !} ∙ z3 where
---       f : S¹ → A
---       f base = x
---       f (loop i) = q' i
-
---       z1 : refl ≡ cong f refl
---       z1 = refl
---       z2 : cong f refl ≡ cong f loop
---       z2 = cong (cong f) loop≡refl
---       z3 : cong f loop ≡ q'
---       z3 = refl
-    
---     g : isSet Type
---     g x y p q = J (λ y' p' → (q' : x ≡ y') → p' ≡ q') goal p q
-
--- Corollary 6.10.13
-
-module corollary61013 where
-  p^ : {A : Type l} {a : A} {p : a ≡ a} → (n : ℤ) → a ≡ a
-  p^ (pos zero) = refl
-  p^ {p = p} (pos (suc x)) = p^ {p = p} (pos x) ∙ p
-  p^ {p = p} (negsuc zero) = p^ {p = p} (pos zero) ∙ sym p
-  p^ {p = p} (negsuc (suc n)) = p^ {p = p} (negsuc n) ∙ sym p ∙ sym p
+{-# OPTIONS --cubical #-}
+module CubicalHott.Chapter6 where
+
+open import CubicalHott.Prelude
+open import CubicalHott.Chapter3
+open import Cubical.Data.Equality.Conversion
+open import Cubical.HITs.Susp
+open import Cubical.HITs.S1
+open import Cubical.Data.Int
+open import Cubical.Data.Nat
+open import Cubical.Data.Bool
+
+private
+  variable
+    l l2 : Level
+
+-- Equation 6.2.2
+
+dep-path : {A : Type} → (P : A → Type) → {x y : A} → (p : x ≡ y) → (u : P x) → (v : P y) → Type
+dep-path P p u v = subst P p u ≡ v
+
+syntax dep-path P p u v = u ≡[ P , p ] v
+
+-- Lemma 6.2.5
+
+module lemma625 where
+  f : {A : Type} {a : A} {p : a ≡ a} → S¹ → A
+  f {a = a} base = a 
+  f {p = p} (loop i) = p i
+
+-- Lemma 6.2.8
+
+-- module lemma628 where
+--   lemma : {A : Type}
+--     → (f g : S¹ → A)
+--     → (p : f base ≡ g base)
+--     → (q : cong f loop ≡[ (λ x → x ≡ x) , p ] cong g loop)
+--     → (x : S¹) → f x ≡ g x
+--   lemma f g p q base i = p i 
+--   lemma f g p q (loop j) i = {!   !}
+
+-- Interval
+
+data [0,1] : Type where
+  ii0 : [0,1]
+  ii1 : [0,1]
+  seg : ii0 ≡ ii1
+
+-- Lemma 6.3.1
+
+module lemma631 where
+  lemma : isContr [0,1]
+  lemma = ii0 , f where
+    f : (y : [0,1]) → ii0 ≡ y
+    f ii0 = refl 
+    f ii1 = seg
+    f (seg i) j = seg (i ∧ j) 
+    
+-- Lemma 6.3.2
+
+module lemma632 where
+  lemma : {A B : Type}
+    → (f g : A → B)
+    → ((x : A) → f x ≡ g x)
+    → f ≡ g
+  lemma {A} {B} f g p i = q (seg i) where
+    p̃ : (x : A) → [0,1] → B
+    p̃ x ii0 = f x
+    p̃ x ii1 = g x
+    p̃ x (seg i) = p x i
+
+    q : [0,1] → (A → B)
+    q i x = p̃ x i
+    
+-- Lemma 6.4.1
+
+-- module lemma641 where
+--   lemma : loop ≢ refl
+--   lemma loop≡refl = example319.lemma g where
+--     goal : {A : Type l} {x : A} {p : x ≡ x} → (q' : x ≡ x) → refl ≡ q'
+--     goal {A = A} {x} {p} q' = z1 ∙ {!   !} ∙ z3 where
+--       f : S¹ → A
+--       f base = x
+--       f (loop i) = q' i
+
+--       z1 : refl ≡ cong f refl
+--       z1 = refl
+--       z2 : cong f refl ≡ cong f loop
+--       z2 = cong (cong f) loop≡refl
+--       z3 : cong f loop ≡ q'
+--       z3 = refl
+    
+--     g : isSet Type
+--     g x y p q = J (λ y' p' → (q' : x ≡ y') → p' ≡ q') goal p q
+
+-- Corollary 6.10.13
+
+module corollary61013 where
+  p^ : {A : Type l} {a : A} {p : a ≡ a} → (n : ℤ) → a ≡ a
+  p^ (pos zero) = refl
+  p^ {p = p} (pos (suc x)) = p^ {p = p} (pos x) ∙ p
+  p^ {p = p} (negsuc zero) = p^ {p = p} (pos zero) ∙ sym p
+  p^ {p = p} (negsuc (suc n)) = p^ {p = p} (negsuc n) ∙ sym p ∙ sym p
diff --git a/src/CubicalHott/Lemma3-11-4.agda b/src/CubicalHott/Lemma3-11-4.agda
new file mode 100644
index 0000000..8d92639
--- /dev/null
+++ b/src/CubicalHott/Lemma3-11-4.agda
@@ -0,0 +1,8 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma3-11-4 where
+
+open import Cubical.Foundations.Prelude
+
+lemma : {A : Type} → isProp (isContr A)
+lemma (x , px) (y , py) i = px y i , {!   !}
\ No newline at end of file
diff --git a/src/CubicalHott/Prelude.agda b/src/CubicalHott/Prelude.agda
index 775ea56..c762eab 100644
--- a/src/CubicalHott/Prelude.agda
+++ b/src/CubicalHott/Prelude.agda
@@ -1,18 +1,18 @@
-{-# OPTIONS --cubical #-}
-module CubicalHott.Prelude where
-
-open import Agda.Primitive using (Level) public
-open import Cubical.Foundations.Equiv public
-open import Cubical.Foundations.Isomorphism public
-open import Cubical.Foundations.Prelude public
-open import Cubical.Foundations.Univalence public
-open import Cubical.Foundations.Function public
-open import Cubical.Relation.Nullary public
-open import Cubical.Data.Equality using (id) public
-
-private
-  variable
-    l : Level
-
-_≢_ : ∀ {A : Type l} → A → A → Type l
+{-# OPTIONS --cubical #-}
+module CubicalHott.Prelude where
+
+open import Agda.Primitive using (Level) public
+open import Cubical.Foundations.Equiv public
+open import Cubical.Foundations.Isomorphism public
+open import Cubical.Foundations.Prelude public
+open import Cubical.Foundations.Univalence public
+open import Cubical.Foundations.Function public
+open import Cubical.Relation.Nullary public
+open import Cubical.Data.Equality using (id) public
+
+private
+  variable
+    l : Level
+
+_≢_ : ∀ {A : Type l} → A → A → Type l
 a ≢ b = ¬ a ≡ b
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem2-7-2.agda b/src/CubicalHott/Theorem2-7-2.agda
index 2891cb8..ef4ac2a 100644
--- a/src/CubicalHott/Theorem2-7-2.agda
+++ b/src/CubicalHott/Theorem2-7-2.agda
@@ -1,55 +1,55 @@
-{-# OPTIONS --cubical #-}
-
-module CubicalHott.Theorem2-7-2 where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Equiv
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Data.Sigma
-
-theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
-  → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
-theorem {P = P} {w = w} {w' = w'} =
-  isoToEquiv (iso f g fg gf) where
-    f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
-    f x = cong fst x , cong snd x
-
-    g : Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w')) → w ≡ w'
-    g x i = fst x i , snd x i
-
-    fg : section f g
-    fg b = refl
-
-    gf : retract f g
-    gf b = refl
-
-
--- theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
---   → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
--- theorem {P = P} {w = w} {w' = w'} =
---   isoToEquiv (iso f g {!   !} {!   !}) where
---     f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
---     f = J (λ y' p' → Σ (fst w ≡ fst y') (λ q → subst P q (snd w) ≡ snd y'))
---       (refl , transportRefl (snd w))
---       -- subst P (λ _ → fst w) (snd w) ≡ w .snd
---     -- x = (λ i → fst (x i)) , J (λ y' p' → {!   !}) {!   !} x where
---       -- subst P (λ i → fst (x i)) (snd w) ≡ snd w'
---       -- P (fst w')
---       -- ———— Boundary (wanted) —————————————————————————————————————
---       -- i = i0 ⊢ transp (λ i₁ → P (fst (x i₁))) i0 (snd w)
---       -- i = i1 ⊢ snd w'
-
---     g : Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w') → w ≡ w'
---     g x i = fst x i , {!   !}
---     -- helper i where
---       -- helper : PathP (λ i → P (fst x i)) (snd w) (snd w')
---       -- helper i =
---       --   let u = λ j → λ where
---       --     (i = i0) → {!   !}
---       --     (i = i1) → {!   !}
---       --   -- let u = λ j → λ where
---       --   --   (i = i0) → transportRefl (snd w) j
---       --   --   (i = i1) → snd w'
---       --   in hcomp u {! snd x ? !}
-
-    
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem2-7-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+
+theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
+  → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
+theorem {P = P} {w = w} {w' = w'} =
+  isoToEquiv (iso f g fg gf) where
+    f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
+    f x = cong fst x , cong snd x
+
+    g : Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w')) → w ≡ w'
+    g x i = fst x i , snd x i
+
+    fg : section f g
+    fg b = refl
+
+    gf : retract f g
+    gf b = refl
+
+
+-- theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
+--   → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
+-- theorem {P = P} {w = w} {w' = w'} =
+--   isoToEquiv (iso f g {!   !} {!   !}) where
+--     f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
+--     f = J (λ y' p' → Σ (fst w ≡ fst y') (λ q → subst P q (snd w) ≡ snd y'))
+--       (refl , transportRefl (snd w))
+--       -- subst P (λ _ → fst w) (snd w) ≡ w .snd
+--     -- x = (λ i → fst (x i)) , J (λ y' p' → {!   !}) {!   !} x where
+--       -- subst P (λ i → fst (x i)) (snd w) ≡ snd w'
+--       -- P (fst w')
+--       -- ———— Boundary (wanted) —————————————————————————————————————
+--       -- i = i0 ⊢ transp (λ i₁ → P (fst (x i₁))) i0 (snd w)
+--       -- i = i1 ⊢ snd w'
+
+--     g : Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w') → w ≡ w'
+--     g x i = fst x i , {!   !}
+--     -- helper i where
+--       -- helper : PathP (λ i → P (fst x i)) (snd w) (snd w')
+--       -- helper i =
+--       --   let u = λ j → λ where
+--       --     (i = i0) → {!   !}
+--       --     (i = i1) → {!   !}
+--       --   -- let u = λ j → λ where
+--       --   --   (i = i0) → transportRefl (snd w) j
+--       --   --   (i = i1) → snd w'
+--       --   in hcomp u {! snd x ? !}
+
+    
diff --git a/src/CubicalHott/Theorem7-1-10.agda b/src/CubicalHott/Theorem7-1-10.agda
new file mode 100644
index 0000000..855d15b
--- /dev/null
+++ b/src/CubicalHott/Theorem7-1-10.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-1-10 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Data.Nat
+
+z = isContr
+
+theorem : {X : Type} → (n : ℕ) → isProp (isOfHLevel n X)
+theorem zero x y i = snd x (fst y) i , let z = snd x (fst y) i in λ y' j → {!   !}
+theorem (suc zero) x y = {!   !} 
+theorem (suc (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 131d45a..deffcc3 100644
--- a/src/CubicalHott/Theorem7-1-9.agda
+++ b/src/CubicalHott/Theorem7-1-9.agda
@@ -1,31 +1,31 @@
-{-# OPTIONS --cubical #-}
-
-module CubicalHott.Theorem7-1-9 where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Equiv
-open import Cubical.Functions.FunExtEquiv
-open import Data.Nat
-
-theorem : {A : Type} {B : A → Type}
-  → (n : ℕ)
-  → ((a : A) → isOfHLevel n (B a))
-  → isOfHLevel n ((x : A) → B x)
-theorem {A = A} {B = B} zero prf = (λ x → fst (prf x)) , helper where
-  helper : (f' : (x : A) → B x) → (λ x → fst (prf x)) ≡ f'
-  helper f' i x =
-    let given = snd (prf x) in
-    given (f' x) i
-theorem (suc zero) prf f1 f2 i x =
-  let result = prf x (f1 x) (f2 x) in
-  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)
-  -- goal1 = subst (λ x → isOfHLevel (suc n) x) funExtPath goal2
-
-  -- IH = theorem {A = A} {B = λ a → f1 a ≡ f2 a} (suc n) λ a → prf a (f1 a) (f2 a)
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-1-9 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Functions.FunExtEquiv
+open import Data.Nat
+
+theorem : {A : Type} {B : A → Type}
+  → (n : ℕ)
+  → ((a : A) → isOfHLevel n (B a))
+  → isOfHLevel n ((x : A) → B x)
+theorem {A = A} {B = B} zero prf = (λ x → fst (prf x)) , helper where
+  helper : (f' : (x : A) → B x) → (λ x → fst (prf x)) ≡ f'
+  helper f' i x =
+    let given = snd (prf x) in
+    given (f' x) i
+theorem (suc zero) prf f1 f2 i x =
+  let result = prf x (f1 x) (f2 x) in
+  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)
+  -- goal1 = subst (λ x → isOfHLevel (suc n) x) funExtPath goal2
+
+  -- IH = theorem {A = A} {B = λ a → f1 a ≡ f2 a} (suc n) λ a → prf a (f1 a) (f2 a)
   -- goal2 = IH
\ No newline at end of file
diff --git a/src/ThesisWork/Pi3S2/LES.agda b/src/ThesisWork/Pi3S2/LES.agda
index 4933405..ca6f57f 100644
--- a/src/ThesisWork/Pi3S2/LES.agda
+++ b/src/ThesisWork/Pi3S2/LES.agda
@@ -90,4 +90,10 @@ LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n ,
 --     -- 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
+-- LES-edge f n_ | (n , suc (suc zero)) = λ z → {!   !} 
+
+LES-is-exact : ∀ {l : Level} → {X∙ Y∙ : Pointed l}
+  → (f∙ : X∙ →∙ Y∙)
+  → (n : ℕ × Fin 3)
+  → {!   !}
+LES-is-exact f∙ (n , k) = {!   !} 
\ No newline at end of file
diff --git a/src/ThesisWork/Pi3S2/Lemma4-1-5.agda b/src/ThesisWork/Pi3S2/Lemma4-1-5.agda
index 28058a3..f6abf6f 100644
--- a/src/ThesisWork/Pi3S2/Lemma4-1-5.agda
+++ b/src/ThesisWork/Pi3S2/Lemma4-1-5.agda
@@ -89,4 +89,4 @@ lemma {A∙ = A∙ @ (A , a0)} {B∙ = B∙ @ (B , b0)} f∙ @ (f , f-eq) = eqv
           f-eq ∙ (sym f-eq ∙ a) ≡⟨ assoc f-eq (sym f-eq) a ⟩
           (f-eq ∙ sym f-eq) ∙ a ≡⟨ cong (_∙ a) (rCancel f-eq) ⟩
           refl ∙ a ≡⟨ sym (lUnit a) ⟩
-          a ∎
\ No newline at end of file
+          a ∎
diff --git a/src/ThesisWork/README.md b/src/ThesisWork/README.md
index 34c35f9..68da2a9 100644
--- a/src/ThesisWork/README.md
+++ b/src/ThesisWork/README.md
@@ -1,3 +1,3 @@
-# Notes
-
-- Already some existing work by Felix Cherubini (@felixwellen) about spectra here: https://github.com/agda/cubical/pull/723
+# Notes
+
+- Already some existing work by Felix Cherubini (@felixwellen) about spectra here: https://github.com/agda/cubical/pull/723
diff --git a/talks/2024-grads/Demo1.agda b/talks/2024-grads/Demo1.agda
new file mode 100644
index 0000000..8222437
--- /dev/null
+++ b/talks/2024-grads/Demo1.agda
@@ -0,0 +1,11 @@
+module 2024-grads.Demo1 where
+
+open import Data.Nat
+open import Data.Nat.Tactic.RingSolver
+open import Relation.Binary.PropositionalEquality as Eq
+
+_ : 1 + 1 ≡ 2
+_ = refl
+
+commutativity : (m n : ℕ) → m + n ≡ n + m
+commutativity = solve-∀
\ No newline at end of file
diff --git a/talks/2024-grads/main.tex b/talks/2024-grads/main.tex
index 7053cbe..7cb401a 100644
--- a/talks/2024-grads/main.tex
+++ b/talks/2024-grads/main.tex
@@ -47,6 +47,7 @@
     \note[item]{What: Program properties, compiler optimizations, correctness}
     \note[item]{Notably, can NOT prove some things, Rice's theorem}
 
+    \note[item]{Talk about proofs vs. testing}
     \item How to formalize proofs?
     \note[item]{How: lot of different techniques involving model checking / SMT approaches, etc}
     \note[item]{I'm going to focus here on proofs of mathematical statements, like $$ x + y = y + x $$}
@@ -78,10 +79,19 @@
   \end{itemize}
 \end{frame}
 
+
+
+\begin{frame}
+  \frametitle{Set theory}
+
+  Talk about set theory
+\end{frame}
+
 \begin{frame}
   \frametitle{Important features of Martin-L{\"o}f type theory}
 
   \begin{itemize}
+    \item Types instead of sets
     \item Predicative universes: $\mathsf{Type}_0, \mathsf{Type}_1, \mathsf{Type}_2, \dots$
     \item Inductive types: for example, $\mathbb{N}$ is defined with 2 possible constructors: $\mathsf{zero}$ and $\mathsf{suc}$.
 
diff --git a/talks/2024-grads/references.bib b/talks/2024-grads/references.bib
index 3ed0c13..8652659 100644
--- a/talks/2024-grads/references.bib
+++ b/talks/2024-grads/references.bib
@@ -1,16 +1,16 @@
-@Book{hottbook,
-  author =    {The {Univalent Foundations Program}},
-  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
-  publisher = {\url{https://homotopytypetheory.org/book}},
-  address =   {Institute for Advanced Study},
-  year =      2013}
-
-@article{
-  Cohen_Coquand_Huber_Mörtberg_2016,
-  title={Cubical Type Theory: a constructive interpretation of the univalence axiom},
-  url={http://arxiv.org/abs/1611.02108},
-  DOI={10.48550/arXiv.1611.02108},
-  abstractNote={This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky’s univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.}, note={arXiv:1611.02108 [cs, math]}, number={arXiv:1611.02108}, publisher={arXiv}, author={Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
-  year={2016},
-  month=nov
-}
+@Book{hottbook,
+  author =    {The {Univalent Foundations Program}},
+  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
+  publisher = {\url{https://homotopytypetheory.org/book}},
+  address =   {Institute for Advanced Study},
+  year =      2013}
+
+@article{
+  Cohen_Coquand_Huber_Mörtberg_2016,
+  title={Cubical Type Theory: a constructive interpretation of the univalence axiom},
+  url={http://arxiv.org/abs/1611.02108},
+  DOI={10.48550/arXiv.1611.02108},
+  abstractNote={This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky’s univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.}, note={arXiv:1611.02108 [cs, math]}, number={arXiv:1611.02108}, publisher={arXiv}, author={Cohen, Cyril and Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
+  year={2016},
+  month=nov
+}