From 282be4abed3d714aaa494c1019f8e932dd0bdfe3 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 30 May 2024 16:54:04 -0500
Subject: [PATCH] make it error-less

---
 Makefile                                      |   8 +-
 src/HottBook/Chapter2Exercises.lagda.md       |   6 +-
 src/HottBook/Chapter3.lagda.md                | 109 +++++++++---------
 src/HottBook/Chapter6.lagda.md                |  12 +-
 src/HottBook/Chapter7.lagda.md                |   2 +
 src/HottBook/Chapter8.lagda.md                |   5 +-
 src/HottBook/Chapter9.lagda.md                |  13 ++-
 src/HottBook/Primitives.agda                  |  21 ----
 src/VanDoornDissertation/HIT.lagda.md         |  15 ++-
 .../Preliminaries.lagda.md                    |   1 -
 10 files changed, 90 insertions(+), 102 deletions(-)
 delete mode 100644 src/HottBook/Primitives.agda

diff --git a/Makefile b/Makefile
index 94aec3c..8ffac85 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,11 @@
 GENDIR := html/src/generated
 
 build-to-html:
-	find src \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
+	find src \
+    -not \( -path src/Misc -prune \) \
+    -not \( -path src/CubicalHott -prune \) \
+    \( -name "*.agda" -o -name "*.lagda.md" \) \
+    -print0 \
 	  | rust-parallel -0 agda \
 	  	--html \
 		--html-dir=$(GENDIR) \
@@ -17,6 +21,6 @@ refresh-book: build-to-html
 	mdbook serve html
 
 deploy: build-book
-	rsync -azrP html/book/ root@veil:/home/blogDeploy/public/research
+	rsync -azr html/book/ root@veil:/home/blogDeploy/public/research
 
 .PHONY: build-book build-to-html deploy
\ No newline at end of file
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 9b31abe..79a2e41 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -133,10 +133,6 @@ exercise2∙13 = f , equiv
   where
     open WithAbstractionUtil
 
-    neg : 𝟚 → 𝟚
-    neg true = false
-    neg false = true
-
     f : 𝟚 ≃ 𝟚 → 𝟚
     f (fst , snd) = fst true
 
@@ -168,7 +164,7 @@ exercise2∙13 = f , equiv
           let p3 = trans (sym (h-id true)) p2 in
           remark2∙12∙6 p3
 
-        ⊥-elim : {A : Set} → ⊥ → A
+        ⊥-elim : {l : Level} {A : Set l} → ⊥ {l} → A
         ⊥-elim ()
 
         opposite-prop : {a b : 𝟚} → (p : f' a ≡ b) → f' (neg a) ≡ neg b
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 6655036..f351988 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -48,28 +48,28 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 ### Example 3.1.9
 
 ```
-example3∙1∙9 : ∀ {l : Level} → ¬_ {lsuc l} (isSet (Set l))
-example3∙1∙9 p = remark2∙12∙6 lol
-  where
-    open axiom2∙10∙3
+-- example3∙1∙9 : ∀ {l : Level} → ¬_ {lsuc l} (isSet (Set l))
+-- example3∙1∙9 p = remark2∙12∙6 lol
+--   where
+--     open axiom2∙10∙3
 
-    f-path : 𝟚 ≡ 𝟚
-    f-path = ua neg-equiv
+--     f-path : 𝟚 ≡ 𝟚
+--     f-path = ua neg-equiv
 
-    bogus : id ≡ neg
-    bogus =
-      let
-        -- helper : f-path ≡ refl
-        -- helper = p 𝟚 𝟚 f-path refl
+--     bogus : id ≡ neg
+--     bogus =
+--       let
+--         -- helper : f-path ≡ refl
+--         -- helper = p 𝟚 𝟚 f-path refl
 
-        a = ap
+--         a = ap
 
-        -- wtf : idtoeqv f-path ≡ idtoeqv refl
-        -- wtf = ap idtoeqv helper
-      in {!   !}
+--         -- wtf : idtoeqv f-path ≡ idtoeqv refl
+--         -- wtf = ap idtoeqv helper
+--       in {!   !}
 
-    lol : true ≡ false
-    lol = ap (λ f → f true) bogus
+--     lol : true ≡ false
+--     lol = ap (λ f → f true) bogus
 ```
 
 ## 3.2 Propositions as types?
@@ -79,55 +79,56 @@ example3∙1∙9 p = remark2∙12∙6 lol
 TODO: Study this more
 
 ```
-theorem3∙2∙2 : ((A : Set) → ¬ ¬ A → A) → ⊥
-theorem3∙2∙2 f = let wtf = f 𝟚 in {!   !}
-  where
-    open axiom2∙10∙3
+postulate
+  theorem3∙2∙2 : {l : Level} → ((A : Set l) → ¬ ¬ A → A) → ⊥ {l}
+-- theorem3∙2∙2 f = let wtf = f 𝟚 in {!   !}
+--   where
+--     open axiom2∙10∙3
 
-    p : 𝟚 ≡ 𝟚
-    p = ua neg-equiv
+--     p : 𝟚 ≡ 𝟚
+--     p = ua neg-equiv
 
-    wtf : ¬ ¬ 𝟚 → 𝟚
-    wtf = f 𝟚
+--     wtf : ¬ ¬ 𝟚 → 𝟚
+--     wtf = f 𝟚
 
-    wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚
-    wtf2 = apd f p
+--     wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚
+--     wtf2 = apd f p
 
-    wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u
-    wtf3 u = happly wtf2 u
+--     wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u
+--     wtf3 u = happly wtf2 u
 
-    wtf4 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ transport (λ A → A) p (f 𝟚 (transport (λ A → ¬ ¬ A) (sym p) u))
-    wtf4 u = 
-      let
-        wtf5 : 
-          let A = λ A → ¬ ¬ A in
-          let B = id in
-          transport (λ x → A x → B x) p (f 𝟚) ≡ λ x → transport B p (f 𝟚 (transport A (sym p) x))
-        wtf5 = equation2∙9∙4 (f 𝟚) p
-      in
-      happly wtf5 u
+--     wtf4 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ transport (λ A → A) p (f 𝟚 (transport (λ A → ¬ ¬ A) (sym p) u))
+--     wtf4 u = 
+--       let
+--         wtf5 : 
+--           let A = λ A → ¬ ¬ A in
+--           let B = id in
+--           transport (λ x → A x → B x) p (f 𝟚) ≡ λ x → transport B p (f 𝟚 (transport A (sym p) x))
+--         wtf5 = equation2∙9∙4 (f 𝟚) p
+--       in
+--       happly wtf5 u
 
-    wtf6 : (u v : ¬ ¬ 𝟚) → u ≡ v
-    wtf6 u v = funext (λ x → rec-⊥ (u x))
+--     wtf6 : (u v : ¬ ¬ 𝟚) → u ≡ v
+--     wtf6 u v = funext (λ x → rec-⊥ (u x))
 
-    wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u
-    wtf7 u = {!   !}
+--     wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u
+--     wtf7 u = {!   !}
 
-    wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u
-    wtf8 u = {!  sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u
+--     wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u
+--     wtf8 u = {!  sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u
 
-    wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u
-    wtf9 = {!   !}
+--     wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u
+--     wtf9 = {!   !}
 
-    wtf10 : (x : 𝟚) → ¬ (neg x ≡ x)
-    wtf10 true p = remark2∙12∙6 (sym p)
-    wtf10 false p = remark2∙12∙6 p
+--     wtf10 : (x : 𝟚) → ¬ (neg x ≡ x)
+--     wtf10 true p = remark2∙12∙6 (sym p)
+--     wtf10 false p = remark2∙12∙6 p
 
-    wtf11 : (u : ¬ ¬ 𝟚) → ¬ (neg (f 𝟚 u) ≡ (f 𝟚 u))
-    wtf11 u = wtf10 (f 𝟚 u)
+--     wtf11 : (u : ¬ ¬ 𝟚) → ¬ (neg (f 𝟚 u) ≡ (f 𝟚 u))
+--     wtf11 u = wtf10 (f 𝟚 u)
 
-    wtf12 : (u : ¬ ¬ 𝟚) → ⊥
-    wtf12 u = wtf11 u (wtf9 u)
+--     wtf12 : (u : ¬ ¬ 𝟚) → ⊥
+--     wtf12 u = wtf11 u (wtf9 u)
 ```
 
 ### Corollary 3.2.7
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index 06a3e7d..74731f1 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -52,11 +52,13 @@ lemma6∙2∙5 {A} a p circ = S¹-elim P p-base p-loop circ
 ### Lemma 6.2.8
 
 ```
-lemma6∙2∙8 : {A : Set} {f g : S¹ → A}
-  → (p : f base ≡ g base)
-  → (q : (ap f loop) ≡[ (λ x → x ≡ x) , p ] (ap g loop))
-  → (x : S¹) → f x ≡ g x
-lemma6∙2∙8 {A} {f} {g} p q = S¹-elim (λ x → f x ≡ g x) p {!   !}
+-- TODO: Finish this
+postulate
+  lemma6∙2∙8 : {A : Set} {f g : S¹ → A}
+    → (p : f base ≡ g base)
+    → (q : (ap f loop) ≡[ (λ x → x ≡ x) , p ] (ap g loop))
+    → (x : S¹) → f x ≡ g x
+-- lemma6∙2∙8 {A} {f} {g} p q = S¹-elim (λ x → f x ≡ g x) p {!   !}
 ```
 
 ## 6.3 The interval
diff --git a/src/HottBook/Chapter7.lagda.md b/src/HottBook/Chapter7.lagda.md
index ab8b050..56b653e 100644
--- a/src/HottBook/Chapter7.lagda.md
+++ b/src/HottBook/Chapter7.lagda.md
@@ -13,4 +13,6 @@ open import HottBook.Chapter6
 
 ```
 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/Chapter8.lagda.md b/src/HottBook/Chapter8.lagda.md
index 3855299..177bb1d 100644
--- a/src/HottBook/Chapter8.lagda.md
+++ b/src/HottBook/Chapter8.lagda.md
@@ -10,8 +10,9 @@ open import HottBook.Chapter6
 ### Definition 8.0.1
 
 ```
-π : (n : ℕ) → (A : Set) → (a : A) → Set
-
+-- TODO: Finish
+postulate
+  π : (n : ℕ) → (A : Set) → (a : A) → Set
 ```
 
 ## 8.1 π₁(S¹)
diff --git a/src/HottBook/Chapter9.lagda.md b/src/HottBook/Chapter9.lagda.md
index 7bada01..5968ed2 100644
--- a/src/HottBook/Chapter9.lagda.md
+++ b/src/HottBook/Chapter9.lagda.md
@@ -11,19 +11,19 @@ open import HottBook.Chapter1
 record precat {l : Level} (A : Set l) : Set (lsuc l) where
   field
     hom : (a b : A) → Set
-    id : (a : A) → hom a a
+    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)
+    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
+-- 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
@@ -34,4 +34,5 @@ idtoiso : {A : Set}
   → (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
diff --git a/src/HottBook/Primitives.agda b/src/HottBook/Primitives.agda
deleted file mode 100644
index ea545c7..0000000
--- a/src/HottBook/Primitives.agda
+++ /dev/null
@@ -1,21 +0,0 @@
-module HottBook.Primitives where
-
-{-# BUILTIN TYPE Type  #-}
-{-# BUILTIN SETOMEGA Typeω #-}
-{-# BUILTIN PROP Prop  #-}
-{-# BUILTIN PROPOMEGA Propω #-}
-{-# BUILTIN STRICTSET SType  #-}
-{-# BUILTIN STRICTSETOMEGA STypeω #-}
-
-postulate
-  Level : Type
-  lzero : Level
-  lsuc  : Level → Level
-  _⊔_   : Level → Level → Level
-infixl 6 _⊔_
-
-{-# BUILTIN LEVELUNIV LevelUniv #-}
-{-# BUILTIN LEVEL Level #-}
-{-# BUILTIN LEVELZERO lzero #-}
-{-# BUILTIN LEVELSUC lsuc #-}
-{-# BUILTIN LEVELMAX _⊔_ #-}
\ No newline at end of file
diff --git a/src/VanDoornDissertation/HIT.lagda.md b/src/VanDoornDissertation/HIT.lagda.md
index 790c903..c65b905 100644
--- a/src/VanDoornDissertation/HIT.lagda.md
+++ b/src/VanDoornDissertation/HIT.lagda.md
@@ -1,9 +1,8 @@
 ```
-{-# OPTIONS --cubical #-}
 module VanDoornDissertation.HIT where
 
-open import Data.Nat
-open import VanDoornDissertation.Preliminaries
+open import HottBook.Chapter1
+-- open import VanDoornDissertation.Preliminaries
 ```
 
 # 3 Higher Inductive Types
@@ -11,9 +10,13 @@ open import VanDoornDissertation.Preliminaries
 ## 3.1 Propositional Truncation
 
 ```
-data one-step-truncation (A : Set) : Set where
-  f : A → one-step-truncation A
-  e : (x y : A) → f x ≡ f y
+postulate
+  one-step-truncation : Set → Set
+  f : {A : Set} → A → one-step-truncation A
+  e : {A : Set} → (x y : A) → f x ≡ f y
+-- data one-step-truncation (A : Set) : Set where
+--   f : A → one-step-truncation A
+--   e : (x y : A) → f x ≡ f y
 
 weakly-constant : {A B : Set} → (g : A → B) → Set
 weakly-constant {A} g = {x y : A} → g x ≡ g y
diff --git a/src/VanDoornDissertation/Preliminaries.lagda.md b/src/VanDoornDissertation/Preliminaries.lagda.md
index 7ac242f..b4a2926 100644
--- a/src/VanDoornDissertation/Preliminaries.lagda.md
+++ b/src/VanDoornDissertation/Preliminaries.lagda.md
@@ -1,5 +1,4 @@
 ```
-{-# OPTIONS --cubical #-}
 module VanDoornDissertation.Preliminaries where
 
 open import Agda.Primitive