build table

.editorconfig

@@ -1,3 +1,7 @@
 [*]
 indent_size = 2
-indent_style = space
+indent_style = space
+
+[Makefile]
+indent_size = 4
+indent_style = tab

Makefile

@@ -1,17 +1,18 @@
 GENDIR := html/src/generated
 
 build-to-html:
+	nu scripts/build-table
 	find src \
-    -not \( -path src/Misc -prune \) \
-    \( -name "*.agda" -o -name "*.lagda.md" \) \
-    -print0 \
-	  | rust-parallel -0 agda \
-	  	--html \
+		-not \( -path src/Misc -prune \) \
+		\( -name "*.agda" -o -name "*.lagda.md" \) \
+		-print0 \
+		| rust-parallel -0 agda \
+			--html \
 		--html-dir=$(GENDIR) \
 		--allow-unsolved-metas \
 		--html-highlight=auto \
-    --no-load-primitives \
-	  || true
+		--no-load-primitives \
+		|| true
 	fd --no-ignore "html$$" $(GENDIR) -x rm
 
 build-book: build-to-html

html/src/front.md

@@ -25,3 +25,7 @@ I have scaled down some of these materials to eBook size, for easier reading on
   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)]
+
+## HottBook Progress:
+
+{{#include generated/Progress.md}}

scripts/build-table

@@ -0,0 +1,80 @@
+#!/usr/bin/env nu
+
+let chapters = {
+  2: 7,
+  3: 9,
+  4: 19,
+}
+
+let gradients = [
+  [0, [90, 0, 0]],
+  [0.5, [90, 90, 0]],
+  [1, [0, 90, 0]],
+]
+
+let formatColor = {|color| $"rgb\(($color.0), ($color.1), ($color.2)\)" }
+
+let interpColor = {|p| 
+  let next = ($gradients
+    | enumerate
+    | skip until { $p <= $in.item.0 }
+    | get index).0
+  if $next == 0 { return (do $formatColor ($gradients.0.1)) }
+  let prev = ($gradients | get ($next - 1))
+  let next = ($gradients | get $next)
+  let pp = ($p - $prev.0) / ($next.0 - $prev.0)
+
+  let color = ($prev.1 | zip $next.1 | each {|a| $a.0 * (1 - $pp) + $a.1 * $pp})
+  do $formatColor $color
+}
+
+let viz = { |k, n| 
+  let ratio = ($k / $n) | math round --precision 1
+  # let color = if n == 0 { "gray" } else if $ratio < 0.25 { "red" } else if $ratio < 0.5 { "orange"} else if $ratio < 0.75 { "yellow"} else { "green" }
+  let color = if $n == 0 { "gray" } else { do $interpColor ($k / $n) }
+  let textColor = if $k == $n { "gold" } else { "white" }
+
+  $"<div style=\"
+      display: flex;
+      align-items: center;
+      justify-content: center;
+      aspect-ratio: 1;
+      min-height: 80px;
+      background-color: ($color);
+      color: ($textColor);
+    \">
+    ($k)&nbsp;/&nbsp;($n)
+  </div>" | str replace -a "\n" ""
+  # $n | math round --precision 1 
+}
+
+let vizChapter = { |n| 
+  let nStr = $n | into string
+  let url = $"https://git.mzhang.io/api/v1/repos/school/type-theory/issues/($chapters | get $nStr)"
+
+  curl -s $url
+    | jq -r .body
+    | lines
+    | rg -o $"\\[\(x| \)\\] \(.*\) \(\\d+\(\\.\\d+\)*\)" -r "$1,$2,$3"
+    | from csv --noheaders
+    | rename completed type number
+    | insert section { if $in.type == "Exercise" { "Exercise" } else { $in.number | split row "." | get 1 } }
+    | group-by section
+    | transpose
+    | each { $in | update column1 { do $viz ($in | where completed == "x" | length) ($in | length) } }
+    | sort-by -n column0
+    | prepend { column0: "Ch", column1: $n }
+    | transpose -r
+}
+
+$chapters
+  | columns
+  | each { do $vizChapter $in }
+  | reduce {|it, acc| $acc | append $it }
+  | sort-by Ch
+  | tee { save -f html/src/generated/Progress.md }
+
+
+# open breakdown.json
+#   | transpose
+#   | each {|row| [$row.column0, $row.column1.ratioCompleted] }

src/HottBook/Chapter3.lagda.md

@@ -57,18 +57,18 @@ TODO: DO this without path induction
 
 ```
 ×-Set : {A B : Set} → isSet A → isSet B → isSet (A × B)
-×-Set {A} {B} A-set B-set (xa , xb) (ya , yb) refl refl =
-  let
-    open theorem2∙6∙2
+×-Set {A} {B} A-set B-set (xa , xb) (ya , yb) refl refl = refl
+```
 
-    -- p-pair = definition2∙6∙1 p
-    -- q-pair = definition2∙6∙1 q
+### Example 3.1.6
 
-    -- a-eq = A-set xa ya (Σ.fst p-pair) (Σ.fst q-pair)
-    -- b-eq = B-set xb yb (Σ.snd p-pair) (Σ.snd q-pair)
-
-    -- overall = pair-≡ {xa ≡ ya} {xb ≡ yb} {p-pair} {q-pair} (a-eq , b-eq)
-  in refl
+```
+-- example3∙1∙6 : {A : Set} {B : A → Set} → ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
+-- example3∙1∙6 func f g p q =
+--   let
+--     wtf : p ≡ funext (λ x → happly p x)
+--     wtf = refl
+--   in {!   !}
 ```
 
 ### Definition 3.1.7
@@ -80,6 +80,8 @@ is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s
 
 ### Lemma 3.1.8
 
+"levels are upward-closed"
+
 ```
 lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
 lemma3∙1∙8 {A} A-set x y p q r s =
@@ -109,7 +111,7 @@ lemma3∙1∙8 {A} A-set x y p q r s =
 ### Example 3.1.9
 
 ```
-example3∙1∙9 : ¬  (isSet Set)
+example3∙1∙9 : ¬ (isSet Set)
 example3∙1∙9 p = remark2∙12∙6.true≢false lol
   where
     open axiom2∙10∙3
@@ -262,8 +264,8 @@ module definition3∙4∙3 where
   data decidable (A : Set) : Set where
     proof : A + (¬ A) → decidable A
 
-  data decidable2 {A : Set} (B : A → Set) : Set where
-    proof : (a : A) → (B a + (¬ (B a))) → decidable2 B
+  data decidable-family {A : Set} (B : A → Set) : Set where
+    proof : (a : A) → (B a + (¬ (B a))) → decidable-family B
 
   data decidable-equality (A : Set) : Set where
     proof : (a b : A) → ((a ≡ b) + (¬ a ≡ b)) → decidable-equality A
@@ -283,9 +285,10 @@ module section3∙7 where
     ∥_∥ : Set → Set
     ∣_∣ : {A : Set} → (a : A) → ∥ A ∥
     witness : {A : Set} → (x y : ∥ A ∥) → x ≡ y → Set
+
     rec-∥_∥ : (A : Set) → {B : Set} → isProp B → (f : A → B)
       → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
-open section3∙7
+open section3∙7 public
 ```
 
 ### Definition 3.7.1
@@ -298,22 +301,27 @@ open section3∙7
 lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
 lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
   where
-    thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ id a)
+    thing2 : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ (∣ a ∣) ∣ ≡ ∣ a ∣)
+    thing2 = rec-∥ P ∥ prop ∣_∣
+
+    thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ a)
     thing = rec-∥ P ∥ prop id
 
     g = Σ.fst thing
+
+    g-prop : (a : P) → g ∣ a ∣ ≡ a
     g-prop = Σ.snd thing
 
     prop2 : isProp ∥ P ∥
+    -- x y : ∥ P ∥
     prop2 x y = 
-      let a = g-prop (g x) in
-      let b = g-prop (g y) in
-      let eqProp = prop (g x) (g y) in
-      let 
-        concat : g (∣ g x ∣) ≡ g (∣ g y ∣)
-        concat = a ∙ eqProp ∙ (sym b)
+      let
+        gx = g x
+        gy = g y
+        eqP = prop gx gy
+        gpx = g-prop gx
       in
-      admit
+      {!   !}
       where
         postulate
           -- TODO: Finish this 

src/HottBook/Chapter3Exercises.lagda.md

@@ -12,9 +12,47 @@ ProvethatifA≃BandAisaset,thensoisB.
 
 ```
 exercise3∙1 : {A B : Set}
-  → isSet (A ≃ B)
+  → A ≃ B
   → isSet A
   → isSet B
-exercise3∙1 {A} {B} isSetAB isSetA xB yB pB qB =
-  {!   !}
+exercise3∙1 {A} {B} equiv@(f , mkIsEquiv g g* h h*) isSetA xB yB pB qB =
+  let
+    xA = g xB
+    yA = g yB
+    pA : xA ≡ yA
+    pA = ap g pB
+    qA : xA ≡ yA
+    qA = ap g qB
+    eq = isSetA xA yA pA qA
+    idAB = axiom2∙10∙3.ua equiv
+    eqB = transport (λ S → {!   !}) idAB eq
+  in {!   !}
+```
+
+### Exercise 3.5
+
+```
+exercise3∙5 : ∀ {A} → isProp A ≃ ((x : A) → isContr A)
+exercise3∙5 {A} = {!  f , ? !}
+  where
+    f : isProp A → ((x : A) → isContr A)
+    f AisProp x = x , λ y → AisProp x y
+
+    g : ((x : A) → isContr A) → isProp A
+    g func x y = {!   !}
+```
+
+### Exercise 3.19
+
+```
+exercise3∙19 : (P : ℕ → Set)
+  → definition3∙4∙3.decidable-family P
+  → ∥ Σ ℕ P ∥ → Σ ℕ P
+exercise3∙19 P Pdecidable trunc = {!   !}
+```
+
+### Exercise 3.20
+
+```
+exercise3∙20 = lemma3∙11∙9.ii
 ```