diff --git a/.editorconfig b/.editorconfig index 3f999da..3de629d 100644 --- a/.editorconfig +++ b/.editorconfig @@ -1,3 +1,7 @@ [*] indent_size = 2 -indent_style = space \ No newline at end of file +indent_style = space + +[Makefile] +indent_size = 4 +indent_style = tab \ No newline at end of file diff --git a/Makefile b/Makefile index 044d83a..75bc087 100644 --- a/Makefile +++ b/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 diff --git a/html/src/front.md b/html/src/front.md index 47f8cde..f7ceba4 100644 --- a/html/src/front.md +++ b/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}} \ No newline at end of file diff --git a/scripts/build-table b/scripts/build-table new file mode 100755 index 0000000..12d6da5 --- /dev/null +++ b/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" } + + $"
+ ($k) / ($n) +
" | 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] } \ No newline at end of file diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 77081a8..24bd5bb 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/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 diff --git a/src/HottBook/Chapter3Exercises.lagda.md b/src/HottBook/Chapter3Exercises.lagda.md index 9694e87..40748a9 100644 --- a/src/HottBook/Chapter3Exercises.lagda.md +++ b/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 ``` \ No newline at end of file