make it compile again

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]

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)]

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

src/HottBook/Chapter7.lagda.md

@@ -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)
-```

src/HottBook/Chapter9.lagda.md

@@ -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
-```