diff --git a/html/book.toml b/html/book.toml
index 8920053..e9c0af1 100644
--- a/html/book.toml
+++ b/html/book.toml
@@ -8,8 +8,8 @@ title = "Research"
[preprocessor.katex]
macros = "./macros.txt"
-[preprocessor.graph]
-command = "bun aux/preprocessGraph.ts"
+# [preprocessor.graph]
+# command = "bun aux/preprocessGraph.ts"
[preprocessor.chapter-zero]
levels = [0]
diff --git a/html/src/front.md b/html/src/front.md
index 438be5d..47f8cde 100644
--- a/html/src/front.md
+++ b/html/src/front.md
@@ -22,5 +22,6 @@ I have scaled down some of these materials to eBook size, for easier reading on
[[ebook-sized pdf](https://git.mzhang.io/school/type-theory/src/branch/master/resources/MayConcise/ConciseRevised.pdf)]
[[original pdf](https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf)]
-
+ Cubical Type Theory: a constructive interpretation of the univalence axiom (CCHM) (2015)
[[ebook-sized pdf](https://git.mzhang.io/school/type-theory/raw/branch/master/resources/CCHM/main.pdf)]
[[original pdf](https://arxiv.org/pdf/1611.02108)]
diff --git a/src/CubicalHott/Chapter2.lagda.md b/src/CubicalHott/Chapter2.lagda.md
index 5d11425..1ecb81b 100644
--- a/src/CubicalHott/Chapter2.lagda.md
+++ b/src/CubicalHott/Chapter2.lagda.md
@@ -201,20 +201,14 @@ module lemma2∙4∙12 where
```
module axiom2∙10∙3 where
- Glue : ∀ {l l2} (A : Type l)
- → {φ : I}
- → (Te : Partial φ (Σ (Type l2) (λ T → T ≃ A)))
- → Type l2
+ -- Glue : ∀ {l l2} (A : Type l)
+ -- → {φ : I}
+ -- → (Te : Partial φ (Σ (Type l2) (λ T → T ≃ A)))
+ -- → Type l2
- id-equiv : isequiv id
-
- ua : ∀ {l} {A B : Type l} → A ≃ B → A ≡ B
- ua {A = A} {B} eqv i = Glue B λ
- { (i = i0) → A , eqv
- ; (i = i1) → B , _ , id-equiv
- }
- -- postulate
- -- ua : {l : Level} {A B : Type l} → (A ≃ B) → (A ≡ B)
+ postulate
+ -- TODO: Provide the definition for this after reading CCHM
+ ua : {l : Level} {A B : Type l} → (A ≃ B) → (A ≡ B)
-- forward : {l : Level} {A B : Type l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
-- -- forward eqv = {! !}
@@ -225,7 +219,7 @@ module axiom2∙10∙3 where
-- ua-eqv : {l : Level} {A : Type l} {B : Type l} → (A ≃ B) ≃ (A ≡ B)
-- ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
-open axiom2∙10∙3 hiding (forward; backward)
+open axiom2∙10∙3
```
### Remark 2.12.6
diff --git a/src/HottBook/Chapter7.lagda.md b/src/HottBook/Chapter7.lagda.md
deleted file mode 100644
index 56b653e..0000000
--- a/src/HottBook/Chapter7.lagda.md
+++ /dev/null
@@ -1,18 +0,0 @@
-```
-module HottBook.Chapter7 where
-
-open import Agda.Primitive
-open import HottBook.Chapter1
-open import HottBook.Chapter2
-open import HottBook.Chapter6
-```
-
-## 7.1 Definition of $n$-types
-
-### Definition 7.1.1
-
-```
-is-_-type : ℕ → Set → Set
-is- zero -type X = 𝟙
-is- suc n -type X = (x y : X) → is- n -type (x ≡ y)
-```
\ No newline at end of file
diff --git a/src/HottBook/Chapter9.lagda.md b/src/HottBook/Chapter9.lagda.md
deleted file mode 100644
index 5968ed2..0000000
--- a/src/HottBook/Chapter9.lagda.md
+++ /dev/null
@@ -1,38 +0,0 @@
-```
-module HottBook.Chapter9 where
-
-open import Agda.Primitive
-open import HottBook.Chapter1
-```
-
-## 9.1 Categories and precategories
-
-```
-record precat {l : Level} (A : Set l) : Set (lsuc l) where
- field
- hom : (a b : A) → Set
- id' : (a : A) → hom a a
- comp : {a b c : A} → hom a b → hom b c → hom a c
- lol : (a b : A) → (f : hom a b) → (f ≡ comp f (id' b)) × (f ≡ comp (id' a) f)
-
-```
-
-### Definition 9.1.2
-
-```
--- record isIso {l : Level} {A : Set l} {PC : precat A} {a b : A} (f : precat.hom PC a b) : Set (lsuc l) where
--- field
--- g : precat.hom PC b a
--- g-f : precat.comp f g ≡ precat.id' a
-```
-
-### Lemma 9.1.4
-
-```
-idtoiso : {A : Set}
- → (PC : precat A)
- → (a b : A)
- → a ≡ b
- → precat.hom PC a b
-idtoiso {A} PC a b refl = precat.id' PC a
-```
\ No newline at end of file