From ce894147d4b36d4e89bbac22faf05b77e39d9f82 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 20 May 2024 02:40:03 -0500 Subject: [PATCH] progress --- Makefile | 10 +- html/book.toml | 2 +- html/macros.txt | 1 + src/HottBook/Chapter1.lagda.md | 9 +- src/HottBook/Chapter2.lagda.md | 156 ++++++++++++++++++++---- src/HottBook/Chapter2Exercises.lagda.md | 57 ++++++--- src/HottBook/Chapter2Lemma221.lagda.md | 4 +- src/HottBook/Chapter3.lagda.md | 43 +++++++ src/HottBook/Util.agda | 9 ++ 9 files changed, 241 insertions(+), 50 deletions(-) create mode 100644 html/macros.txt diff --git a/Makefile b/Makefile index 5c4affa..7429825 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,5 @@ GENDIR := html/src/generated + build-to-html: find src/HottBook \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \ | rust-parallel -0 agda \ @@ -9,8 +10,13 @@ build-to-html: || true fd --no-ignore "html$$" $(GENDIR) -x rm -deploy: build-to-html +build-book: build-to-html mdbook build html + +refresh-book: build-to-html + mdbook serve html + +deploy: build-book rsync -azrP html/book/ root@veil:/home/blogDeploy/public/hott-book -.PHONY: build-to-html deploy \ No newline at end of file +.PHONY: build-book build-to-html deploy \ No newline at end of file diff --git a/html/book.toml b/html/book.toml index 69bb4db..f8c4374 100644 --- a/html/book.toml +++ b/html/book.toml @@ -6,7 +6,7 @@ src = "src" title = "HoTT Book" [preprocessor.katex] -command = "mdbook-katex" +macros = "./macros.txt" # [preprocessor.pagetoc] diff --git a/html/macros.txt b/html/macros.txt new file mode 100644 index 0000000..99fc636 --- /dev/null +++ b/html/macros.txt @@ -0,0 +1 @@ +\refl:{\textrm{refl}} \ No newline at end of file diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md index 8c14b1f..d29c97b 100644 --- a/src/HottBook/Chapter1.lagda.md +++ b/src/HottBook/Chapter1.lagda.md @@ -46,13 +46,15 @@ data πŸ™ : Set where ## 1.6 Dependent pair types (Ξ£-types) ``` +infixr 4 _,_ +infixr 2 _Γ—_ + record Ξ£ {l₁ lβ‚‚} (A : Set l₁) (B : A β†’ Set lβ‚‚) : Set (l₁ βŠ” lβ‚‚) where constructor _,_ field fst : A snd : B fst open Ξ£ -infixr 4 _,_ {-# BUILTIN SIGMA Ξ£ #-} syntax Ξ£ A (Ξ» x β†’ B) = Ξ£[ x ∈ A ] B @@ -115,7 +117,7 @@ rec-β„• C z s (suc n) = s n (rec-β„• C z s n) ## 1.11 Propositions as types ``` -Β¬_ : (A : Set) β†’ Set +Β¬_ : {l : Level} (A : Set l) β†’ Set l Β¬ A = A β†’ βŠ₯ ``` @@ -179,8 +181,7 @@ composite-assoc f g h = refl ## Exercise 1.14 Why do the induction principles for identity types not allow us to construct a -function f : ∏(x:A) ∏(p:x=x)(p = refl_x) with the defining equation f (x, -refl_x) :≑ refl_(refl_x) ? +function $f : \prod_{x:A} \prod_{p:x \equiv x}(p \equiv \refl_x)$ with the defining equation $f (x, \refl_x) :≑ \refl_{\refl_x}$ ? Under non-UIP systems, there are identity types that are different from refl, and this ability gives us higher dimensional paths. Otherwise, we would be diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 89e05c3..edd8c0c 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -46,19 +46,19 @@ _βˆ™_ = trans ``` module ≑-Reasoning where infix 1 begin_ - begin_ : {A : Set} {x y : A} β†’ (x ≑ y) β†’ (x ≑ y) + begin_ : {l : Level} {A : Set l} {x y : A} β†’ (x ≑ y) β†’ (x ≑ y) begin x = x - _β‰‘βŸ¨βŸ©_ : {A : Set} (x {y} : A) β†’ x ≑ y β†’ x ≑ y + _β‰‘βŸ¨βŸ©_ : {l : Level} {A : Set l} (x {y} : A) β†’ x ≑ y β†’ x ≑ y _ β‰‘βŸ¨βŸ© x≑y = x≑y infixr 2 _β‰‘βŸ¨βŸ©_ step-≑ - step-≑ : {A : Set} (x {y z} : A) β†’ y ≑ z β†’ x ≑ y β†’ x ≑ z + step-≑ : {l : Level} {A : Set l} (x {y z} : A) β†’ y ≑ z β†’ x ≑ y β†’ x ≑ z step-≑ _ y≑z x≑y = trans x≑y y≑z syntax step-≑ x y≑z x≑y = x β‰‘βŸ¨ x≑y ⟩ y≑z infix 3 _∎ - _∎ : {A : Set} (x : A) β†’ (x ≑ x) + _∎ : {l : Level} {A : Set l} (x : A) β†’ (x ≑ x) _ ∎ = refl ``` @@ -254,27 +254,28 @@ lemma2βˆ™3βˆ™9 {A} {x} {y} {z} P p q u = ### Lemma 2.3.10 ``` --- lemma2310 : {A B : Set} (f : A β†’ B) β†’ (P : B β†’ Set) --- β†’ {x y : A} (p : x ≑ y) β†’ (u : P (f x)) --- β†’ transport (P ∘ f) p u ≑ transport P (ap f p) u --- lemma2310 f P p u = --- let --- inner : transport (Ξ» y β†’ P (f y)) refl u ≑ u --- inner = refl --- in --- J (Ξ» _ what β†’ transport (P ∘ f) what u ≑ transport P (ap f what) u) p inner +lemma2βˆ™3βˆ™10 : {l : Level} {A B : Set (lsuc l)} + β†’ (f : A β†’ B) + β†’ (P : B β†’ Set l) + β†’ {x y : A} + β†’ (p : x ≑ y) + β†’ (u : P (f x)) + β†’ transport (P ∘ f) p u ≑ transport P (ap f p) u +lemma2βˆ™3βˆ™10 {l} {A} {B} f P {x} {y} p u = + J (Ξ» x1 y1 p1 β†’ (u1 : P (f x1)) β†’ transport (P ∘ f) p1 u1 ≑ transport P (ap f p1) u1) + (Ξ» x1 u1 β†’ refl) x y p u ``` ### Lemma 2.3.11 ``` --- lemma2βˆ™3βˆ™11 : {A : Set} {P Q : A β†’ Set} --- β†’ (f : (x : A) β†’ P x β†’ Q x) --- β†’ {x y : A} (p : x ≑ y) β†’ (u : P x) --- β†’ transport Q p (f x u) ≑ f y (transport P p u) --- lemma2βˆ™3βˆ™11 {A} {P} {Q} f {x} {y} p u = --- J (Ξ» a b p β†’ transport Q p (f a {! !}) ≑ f b (transport P p {! !})) (Ξ» a β†’ {! !}) x y p - -- J (Ξ» the what β†’ transport Q what (f x u) ≑ f the (transport P what u)) p refl +lemma2βˆ™3βˆ™11 : {A : Set} {P Q : A β†’ Set} + β†’ (f : (x : A) β†’ P x β†’ Q x) + β†’ {x y : A} (p : x ≑ y) β†’ (u : P x) + β†’ transport Q p (f x u) ≑ f y (transport P p u) +lemma2βˆ™3βˆ™11 {A} {P} {Q} f {x} {y} p u = + J (Ξ» x1 y1 p1 β†’ (u1 : P x1) β†’ transport Q p1 (f x1 u1) ≑ f y1 (transport P p1 u1)) + (Ξ» x1 u1 β†’ refl) x y p u ``` ## 2.4 Homotopies and equivalences @@ -471,6 +472,79 @@ module lemma2βˆ™4βˆ™12 where in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward) ``` +## 2.5 The higher groupoid structure of type formers + +### Definition 2.5.1 + +``` +-- definition2βˆ™5βˆ™1 : {B C : Set} {b b' : B} {c c' : C} +-- β†’ ((b , c) ≑ (b' , c')) ≃ ((b ≑ b') Γ— (c ≑ c')) +-- definition2βˆ™5βˆ™1 {B} {C} {b} {b'} {c} {c'} = +-- let +-- open Ξ£ + +-- f : ((b , c) ≑ (b' , c')) β†’ ((b ≑ b') Γ— (c ≑ c')) +-- f p = ap fst p , ap snd p + +-- g : ((b ≑ b') Γ— (c ≑ c')) β†’ ((b , c) ≑ (b' , c')) +-- g p = +-- let (p1 , p2) = p in +-- J (Ξ» x1 y1 p1 β†’ (x1 , c) ≑ (y1 , c')) +-- (Ξ» x1 β†’ ap (Ξ» p β†’ (x1 , p)) p2) b b' p1 + +-- open ≑-Reasoning + +-- forward : (g ∘ f) ∼ id +-- forward x = +-- J (Ξ» x1 y1 p1 β†’ (g ∘ f) {! !} ≑ id {! !}) +-- (Ξ» x1 β†’ {! !}) (b , c) (b' , c') x + +-- backward : (f ∘ g) ∼ id +-- backward x = +-- let (p1 , p2) = x in +-- begin +-- f (g (p1 , p2)) β‰‘βŸ¨ {! !} ⟩ +-- f (J (Ξ» x1 y1 p1 β†’ (x1 , c) ≑ (y1 , c')) (Ξ» x1 β†’ ap (Ξ» p β†’ (x1 , p)) p2) b b' p1) β‰‘βŸ¨ {! !} ⟩ +-- id x ∎ +-- in f , qinv-to-isequiv (mkQinv g backward forward) +``` + +## 2.6 Cartesian product types + +### Definition 2.6.1 + +``` +definition2βˆ™6βˆ™1 : {A B : Set} {x y : A Γ— B} + β†’ (p : x ≑ y) + β†’ (Ξ£.fst x ≑ Ξ£.fst y) Γ— (Ξ£.snd x ≑ Ξ£.snd y) +definition2βˆ™6βˆ™1 p = ap Ξ£.fst p , ap Ξ£.snd p +``` + +### Theorem 2.6.2 + +``` +-- theorem2βˆ™6βˆ™2 : {A B : Set} (x y : A Γ— B) +-- β†’ isequiv (definition2βˆ™6βˆ™1 {A} {B} {x} {y}) +-- theorem2βˆ™6βˆ™2 {A} {B} x y = qinv-to-isequiv (mkQinv g {! !} {! !}) +-- where +-- g : (Ξ£.fst x ≑ Ξ£.fst y) Γ— (Ξ£.snd x ≑ Ξ£.snd y) β†’ x ≑ y +-- g p = +-- let (p1 , p2) = p in +-- J +-- (Ξ» x3 y3 p3 β†’ (x4 y4 : B) β†’ (p2 : x4 ≑ y4) β†’ (x3 , x4) ≑ (y3 , y4)) +-- (Ξ» x1 x4 y4 p2 β†’ J (Ξ» x4 y4 p2 β†’ (x1 , x4) ≑ (x1 , y4)) (Ξ» _ β†’ refl) x4 y4 p2) +-- (Ξ£.fst x) (Ξ£.fst y) p1 (Ξ£.snd x) (Ξ£.snd y) p2 + +-- backward : (definition2βˆ™6βˆ™1 ∘ g) ∼ id +-- backward x = {! !} +``` + +### Theorem 2.6.5 + +``` + +``` + ## 2.7 Ξ£-types ### Theorem 2.7.2 @@ -508,6 +582,17 @@ corollary2βˆ™7βˆ™3 : {A : Set} {P : A β†’ Set} corollary2βˆ™7βˆ™3 z = refl ``` +### Theorem 2.7.4 + +``` +-- theorem2βˆ™7βˆ™4 : {A : Set} {P : A β†’ Set} +-- β†’ (Q : Ξ£ A (Ξ» x β†’ P x) β†’ Set) +-- β†’ {x y : A} +-- β†’ (p : x ≑ y) +-- β†’ (u z : Ξ£ (P x) (Ξ» u β†’ Q (x , u))) +-- β†’ {! !} +``` + ## 2.8 The unit type ### Theorem 2.8.1 @@ -610,8 +695,19 @@ idtoeqv {l} {A} {B} p = J C c A B p ### Axiom 2.10.3 (Univalence) ``` -postulate - ua : {A B : Set} (eqv : A ≃ B) β†’ (A ≑ B) +module axiom2βˆ™10βˆ™3 where + postulate + -- ua-eqv : {l : Level} {A B : Set l} β†’ (A ≃ B) ≃ (A ≑ B) + + ua : {l : Level} {A B : Set l} β†’ (A ≃ B) β†’ (A ≑ B) + + -- forward : {A B : Set} β†’ (eqv @ (f , f-eqv) : A ≃ B) β†’ (x : A) β†’ transport id (ua eqv) x ≑ f x + -- forward eqv x = {! !} + + -- ua-refl : {A : Set} β†’ refl ≑ ua (lemma2βˆ™4βˆ™12.id-equiv A) + -- ua-refl = {! !} + +open axiom2βˆ™10βˆ™3 ``` ### Lemma 2.10.5 @@ -656,6 +752,22 @@ postulate -- ap f , qinv-to-isequiv eqv ``` +## 2.12 Coproducts + +### Remark 2.12.6 + +``` +remark2βˆ™12βˆ™6 : true β‰’ false +remark2βˆ™12βˆ™6 p = genBot tt + where + Bmap : 𝟚 β†’ Set + Bmap true = πŸ™ + Bmap false = βŠ₯ + + genBot : πŸ™ β†’ βŠ₯ + genBot = transport Bmap p +``` + ## 2.13 Natural numbers ``` diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index bf8618b..341d88e 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/src/HottBook/Chapter2Exercises.lagda.md @@ -5,6 +5,7 @@ open import Agda.Primitive open import HottBook.Chapter1 open import HottBook.Chapter2 open import HottBook.Chapter2Lemma221 +open import HottBook.Util ``` ## Exercise 2.1 @@ -73,6 +74,40 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences. [2.3.6]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.6 [2.3.7]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.7 +## Exercise 2.9 + +Prove that coproducts have the expected universal property, + +$ (A + B β†’ X) ≃ (A β†’ X) Γ— (B β†’ X) $ + +``` +exercise2βˆ™9 : {A B X : Set} β†’ (A + B β†’ X) ≃ ((A β†’ X) Γ— (B β†’ X)) +exercise2βˆ™9 {A} {B} {X} = + f , qinv-to-isequiv (mkQinv g f∘g∼id g∘f∼id) + where + f : (A + B β†’ X) β†’ (A β†’ X) Γ— (B β†’ X) + f func = (Ξ» a β†’ func (inl a)) , (Ξ» b β†’ func (inr b)) + + g : ((A β†’ X) Γ— (B β†’ X)) β†’ (A + B β†’ X) + g p = let (f1 , f2) = p in Ξ» pr β†’ rec-+ X f1 f2 pr + + f∘g∼id : (f ∘ g) ∼ id + f∘g∼id x = refl + + open ≑-Reasoning + + g∘f∼id' : (func : A + B β†’ X) β†’ (pr : A + B) β†’ (g ∘ f) func pr ≑ id func pr + g∘f∼id' func (inl a) = refl + g∘f∼id' func (inr b) = refl + + g∘f∼id : (g ∘ f) ∼ id + g∘f∼id func = funext (g∘f∼id' func) +``` + +TODO: Generalizing to dependent functions. + +## Exercise 2.10 + ## Exercise 2.13 _Show that $(2 \simeq 2) \simeq 2$._ @@ -89,15 +124,6 @@ postulate β†’ (e1 e2 : A ≃ B) β†’ (Ξ£.fst e1 ≑ Ξ£.fst e2) β†’ e1 ≑ e2 - --- What the hell --- https://agda.readthedocs.io/en/v2.6.1/language/with-abstraction.html#the-inspect-idiom -module Wtf {a b} {A : Set a} {B : A β†’ Set b} where - data Graph (f : βˆ€ x β†’ B x) (x : A) (y : B x) : Set b where - ingraph : f x ≑ y β†’ Graph f x y - inspect : (f : βˆ€ x β†’ B x) (x : A) β†’ Graph f x (f x) - inspect _ _ = ingraph refl -open Wtf ``` main proof: @@ -106,6 +132,8 @@ main proof: exercise2βˆ™13 : (𝟚 ≃ 𝟚) ≃ 𝟚 exercise2βˆ™13 = f , equiv where + open WithAbstractionUtil + neg : 𝟚 β†’ 𝟚 neg true = false neg false = true @@ -134,21 +162,12 @@ exercise2βˆ™13 = f , equiv g∘f∼id : (g ∘ f) ∼ id g∘f∼id e' @ (f' , ie' @ (mkIsEquiv g' g-id h' h-id)) = attempt where - Bmap : 𝟚 β†’ Set - Bmap true = πŸ™ - Bmap false = βŠ₯ - - trueβ‰’false : true β‰’ false - trueβ‰’false p = - let genBot = transport Bmap p in - genBot tt - f-codomain-is-2 : f' true β‰’ f' false f-codomain-is-2 p = let p1 = ap h' p in let p2 = trans p1 (h-id false) in let p3 = trans (sym (h-id true)) p2 in - trueβ‰’false p3 + remark2βˆ™12βˆ™6 p3 βŠ₯-elim : {A : Set} β†’ βŠ₯ β†’ A βŠ₯-elim () diff --git a/src/HottBook/Chapter2Lemma221.lagda.md b/src/HottBook/Chapter2Lemma221.lagda.md index cb9d840..cb59032 100644 --- a/src/HottBook/Chapter2Lemma221.lagda.md +++ b/src/HottBook/Chapter2Lemma221.lagda.md @@ -8,11 +8,11 @@ open import HottBook.Chapter1 []: ANCHOR: ap ``` -ap : {l : Level} {A B : Set l} {x y : A} +ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A} β†’ (f : A β†’ B) β†’ (p : x ≑ y) β†’ f x ≑ f y -ap {l} {A} {B} {x} {y} f p = +ap {l1} {l2} {A} {B} {x} {y} f p = J (Ξ» x y p β†’ f x ≑ f y) (Ξ» x β†’ refl) x y p ``` diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index cba8dc2..188dc95 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -5,6 +5,7 @@ open import Agda.Primitive open import HottBook.Chapter1 open import HottBook.Chapter1Util open import HottBook.Chapter2 +open import HottBook.Chapter2Lemma221 open import HottBook.Util ``` @@ -39,8 +40,50 @@ isSet A = (x y : A) β†’ (p q : x ≑ y) β†’ p ≑ q -- β„•-is-Set = ``` +### Example 3.1.9 + +``` +example3βˆ™1βˆ™9 : Β¬ (isSet Set) +example3βˆ™1βˆ™9 p = {! !} + where + open axiom2βˆ™10βˆ™3 + + f : 𝟚 β†’ 𝟚 + f true = false + f false = true + + f-homotopy : (f ∘ f) ∼ id + f-homotopy true = refl + f-homotopy false = refl + + f-equiv : 𝟚 ≃ 𝟚 + f-equiv = f , qinv-to-isequiv (mkQinv f f-homotopy f-homotopy) + + f-path : 𝟚 ≑ 𝟚 + f-path = ua f-equiv + + bogus : f ≑ id + bogus = + let + helper : f-path ≑ refl + helper = p 𝟚 𝟚 f-path refl + + a = ap + + wtf : idtoeqv f-path ≑ idtoeqv refl + wtf = ap idtoeqv helper + in {! !} +``` + ## 3.2 Propositions as types? +### Theorem 3.2.2 + +``` +-- theorem3βˆ™2βˆ™2 : (A : Set) β†’ (Β¬ (Β¬ A) β†’ A) β†’ βŠ₯ +-- theorem3βˆ™2βˆ™2 A p = {! !} +``` + ## 3.3 Mere propositions ### Definition 3.3.1 diff --git a/src/HottBook/Util.agda b/src/HottBook/Util.agda index fa7ab3e..d24339d 100644 --- a/src/HottBook/Util.agda +++ b/src/HottBook/Util.agda @@ -1,3 +1,12 @@ module HottBook.Util where open import Agda.Primitive +open import HottBook.Chapter1 + +-- What the hell +-- https://agda.readthedocs.io/en/v2.6.1/language/with-abstraction.html#the-inspect-idiom +module WithAbstractionUtil {a b} {A : Set a} {B : A β†’ Set b} where + data Graph (f : βˆ€ x β†’ B x) (x : A) (y : B x) : Set b where + ingraph : f x ≑ y β†’ Graph f x y + inspect : (f : βˆ€ x β†’ B x) (x : A) β†’ Graph f x (f x) + inspect _ _ = ingraph refl \ No newline at end of file