diff --git a/resources/VanDoornDissertation/dissertation.pdf b/resources/VanDoornDissertation/dissertation.pdf
index e730c6e..9aa4b07 100644
Binary files a/resources/VanDoornDissertation/dissertation.pdf and b/resources/VanDoornDissertation/dissertation.pdf differ
diff --git a/resources/VanDoornDissertation/dissertation.tex b/resources/VanDoornDissertation/dissertation.tex
index fce8139..05e9ace 100644
--- a/resources/VanDoornDissertation/dissertation.tex
+++ b/resources/VanDoornDissertation/dissertation.tex
@@ -1,5 +1,5 @@
 \RequirePackage{fix-cm}
-\def\OPTpagesize{4.8in,7.9in}   % Page size
+\def\OPTpagesize{6in,9in}   % Page size
 \documentclass[12pt]{report}
 \usepackage[hyphens]{url}
 \usepackage[
diff --git a/src/CubicalHottBook/Chapter2.lagda.md b/src/CubicalHottBook/Chapter2.lagda.md
index caf94c5..f9b0c0d 100644
--- a/src/CubicalHottBook/Chapter2.lagda.md
+++ b/src/CubicalHottBook/Chapter2.lagda.md
@@ -16,8 +16,8 @@ transportconst : {A : Type l} {x y : A}
   → (B : Type l2)
   → (p : x ≡ y)
   → (b : B)
-  → subst ? p ? ≡ ?
-transportconst B p b = ?
+  → subst (λ _ → B) p b ≡ b
+transportconst B p b i = {!   !}
 ```
 
 ### Definition 2.4.1
@@ -58,7 +58,6 @@ mkIsEquiv : {A B : Type} {f : A → B}
 mkIsEquiv {B = B} {f = f} g forward backward = record { equiv-proof = eqv-prf } where
   postulate
     helper : (y : B) → (z : fiber f y) → (g y , forward y) ≡ z
-  -- helper y (x , p) = Σ-≡,≡→≡ (ap g (sym p) ∙ backward x , {!  !})
 
   eqv-prf : (y : B) → isContr (fiber f y) 
   eqv-prf y = (g y , forward y) , helper y
@@ -67,22 +66,22 @@ mkIsEquiv {B = B} {f = f} g forward backward = record { equiv-proof = eqv-prf }
 ### Theorem 2.11.3
 
 ```
-theorem2∙11∙3 : {A B : Type} {f g : A → B} {a a' : A}
-  → (p : a ≡ a')
-  → (q : f a ≡ g a)
-  → subst (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ ap g p
-theorem2∙11∙3 refl q = sym (unitR q)
+-- theorem2∙11∙3 : {A B : Type} {f g : A → B} {a a' : A}
+--   → (p : a ≡ a')
+--   → (q : f a ≡ g a)
+--   → subst (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ ap g p
+-- theorem2∙11∙3 refl q = sym (unitR q)
 ```
 
 ### Theorem 2.11.5
 
 ```
-postulate
-  theorem2∙11∙5 : {A : Type} {a a' : A}
-    → (p : a ≡ a')
-    → (q : a ≡ a)
-    → (r : a' ≡ a')
-    → (transport (λ x → x ≡ x) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r)
+-- postulate
+--   theorem2∙11∙5 : {A : Type} {a a' : A}
+--     → (p : a ≡ a')
+--     → (q : a ≡ a)
+--     → (r : a' ≡ a')
+--     → (transport (λ x → x ≡ x) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r)
 -- theorem2∙11∙5 {a = a} refl q r = f , mkIsEquiv g {!   !} {!   !} where
 --   f : (q ≡ r) → (q ∙ refl ≡ r)
 --   f refl = unitR q
diff --git a/src/CubicalHottBook/Prelude.agda b/src/CubicalHottBook/Prelude.agda
index 53e7450..60845ab 100644
--- a/src/CubicalHottBook/Prelude.agda
+++ b/src/CubicalHottBook/Prelude.agda
@@ -4,6 +4,9 @@ module CubicalHottBook.Prelude where
 open import Cubical.Foundations.Function public
 open import Data.Product.Properties public
 open import Cubical.Foundations.Prelude public
-open import Cubical.Data.Equality public using (id)
 open import Cubical.Foundations.Equiv public
 
+module Inductive where
+  open import Cubical.Data.Equality public
+
+open Inductive public using (id)
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index d8b59e5..4e6f455 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -480,6 +480,4 @@ module Pushout where
     Pushout : {A B C : Set} → (f : C → A) → (g : C → B) → Set
 
   syntax Pushout A B C = A ⊔[ C ] B
-```
-  
-## asdf
\ No newline at end of file
+```
\ No newline at end of file
diff --git a/src/VanDoornDissertation/HoTT/LongExactSequence.agda b/src/VanDoornDissertation/HoTT/LongExactSequence.agda
new file mode 100644
index 0000000..b5c0d2a
--- /dev/null
+++ b/src/VanDoornDissertation/HoTT/LongExactSequence.agda
@@ -0,0 +1,4 @@
+{-# OPTIONS --cubical --safe #-}
+
+module VanDoornDissertation.HoTT.LongExactSequence where
+