update

2024-05-17 17:37:20 -05:00 · 2024-05-17 17:37:20 -05:00 · 447bd52025
commit 447bd52025
parent 87ab99506c
8 changed files with 186 additions and 125 deletions
--- a/html/Agda.css
+++ b/html/Agda.css
@ -0,0 +1,41 @@
+/* Aspects. */
+.content .Agda .Comment       { color: #B22222 }
+.content .Agda .Background    {}
+.content .Agda .Markup        { color: #000000 }
+.content .Agda .Keyword       { color: #CD6600 }
+.content .Agda .String        { color: #B22222 }
+.content .Agda .Number        { color: #A020F0 }
+.content .Agda .Symbol        { color: #404040 }
+.content .Agda .PrimitiveType { color: #0000CD }
+.content .Agda .Pragma        { color: black   }
+.content .Agda .Operator      {}
+.content .Agda .Hole          { background: #B4EEB4 }
+
+/* NameKinds. */
+.content .Agda .Bound                  { color: black   }
+.content .Agda .Generalizable          { color: black   }
+.content .Agda .InductiveConstructor   { color: #008B00 }
+.content .Agda .CoinductiveConstructor { color: #8B7500 }
+.content .Agda .Datatype               { color: #0000CD }
+.content .Agda .Field                  { color: #EE1289 }
+.content .Agda .Function               { color: #0000CD }
+.content .Agda .Module                 { color: #A020F0 }
+.content .Agda .Postulate              { color: #0000CD }
+.content .Agda .Primitive              { color: #0000CD }
+.content .Agda .Record                 { color: #0000CD }
+
+/* OtherAspects. */
+.content .Agda .DottedPattern        {}
+.content .Agda .UnsolvedMeta         { color: black; background: yellow         }
+.content .Agda .UnsolvedConstraint   { color: black; background: yellow         }
+.content .Agda .TerminationProblem   { color: black; background: #FFA07A        }
+.content .Agda .IncompletePattern    { color: black; background: #F5DEB3        }
+.content .Agda .Error                { color: red;   text-decoration: underline }
+.content .Agda .TypeChecks           { color: black; background: #ADD8E6        }
+.content .Agda .Deadcode             { color: black; background: #808080        }
+.content .Agda .ShadowingInTelescope { color: black; background: #808080        }
+
+/* Standard attributes. */
+.Agda a { text-decoration: none }
+.Agda a[href]:hover { background-color: #B4EEB4 }
+.Agda [href].hover-highlight { background-color: #B4EEB4; }
--- a/html/book.toml
+++ b/html/book.toml
@ -5,8 +5,17 @@ multilingual = false
 src = "src"
 title = "HoTT Book"

-[preprocessor.pagetoc]
+[preprocessor.katex]
+command = "mdbook-katex"
+
+# [preprocessor.pagetoc]

 [output.html]
-additional-js = ["theme/pagetoc.js"]
-additional-css = ["src/generated/Agda.css", "style.css", "theme/pagetoc.css"]
+additional-js = [
+    # "theme/pagetoc.js"
+]
+additional-css = [
+    "Agda.css",
+    "style.css",
+    # "theme/pagetoc.css"
+]
--- a/html/src/SUMMARY.md
+++ b/html/src/SUMMARY.md
@ -1,7 +1,10 @@
 # Summary

 - [Chapter 1](./generated/HottBook.Chapter1.md)
+  - [Exercises](./generated/HottBook.Chapter1Exercises.md)
 - [Chapter 2](./generated/HottBook.Chapter2.md)
+  - [Exercises](./generated/HottBook.Chapter2Exercises.md)
 - [Chapter 3](./generated/HottBook.Chapter3.md)
 - [Chapter 4](./generated/HottBook.Chapter4.md)
- [Chapter 5](./generated/HottBook.Chapter5.md)
+- [Chapter 5](./generated/HottBook.Chapter5.md)
+- [Chapter 6](./generated/HottBook.Chapter6.md)
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@ -6,11 +6,14 @@ module HottBook.Chapter2 where

 open import Agda.Primitive
 open import HottBook.Chapter1
+open import HottBook.Chapter2Lemma221
 open import HottBook.Util
 ```

 </details>

+# 2 Homotopy type theory
+
 ## 2.1 Types are higher groupoids

 ### Lemma 2.1.1
@ -33,6 +36,8 @@ trans {l} {A} {x} {y} {z} p q =
    func1 x y p = J (λ a b p → a ≡ b) (λ x → refl) x y p
    func2 = J (λ a b p → (z : A) → (q : b ≡ z) → a ≡ z) func1 x y p
  in func2 z q
+
+infixr 30 _∙_
 _∙_ = trans
 ```

@ -60,25 +65,37 @@ module ≡-Reasoning where
 ### Lemma 2.1.4

 ```
-record lemma2∙1∙4-statement {A : Set} {x y z w : A}
-    (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) : Set where
-  field
-    i1 : p ≡ p ∙ refl
-    i2 : p ≡ refl ∙ p
-    ii1 : (sym p) ∙ p ≡ refl
-    ii2 : p ∙ (sym p) ≡ refl
-    iii : sym (sym p) ≡ p
-    iv : p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+module lemma2∙1∙4 {A : Set} where
+  i1 : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
+  i1 {x} {y} p = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p

-lemma2∙1∙4 : {A : Set} {x y z w : A}
-  → (p : x ≡ y) 
-  → (q : y ≡ z) 
-  → (r : z ≡ w) 
-  → lemma2∙1∙4-statement p q r
+  i2 : {x y : A} (p : x ≡ y) → p ≡ refl ∙ p
+  i2 {x} {y} p = J (λ x y p → p ≡ refl ∙ p) (λ _ → refl) x y p
+
+  ii1 : {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
+  ii1 {x} {y} p = J (λ x y p → (sym p) ∙ p ≡ refl) (λ _ → refl) x y p
+
+  ii2 : {x y : A} (p : x ≡ y) → p ∙ (sym p) ≡ refl
+  ii2 {x} {y} p = J (λ x y p → p ∙ (sym p) ≡ refl) (λ _ → refl) x y p
+
+  iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
+  iii {x} {y} p = J (λ x y p → sym (sym p) ≡ p) (λ _ → refl) x y p
+
+  iv : {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+  iv {x} {y} {z} {w} p q r = let
+      open ≡-Reasoning
+
+      C : (x y : A) → (p : x ≡ y) → Set
+      C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+
+      c : (x : A) → C x x refl
+      c x q1 = begin
+        refl ∙ (q1 ∙ r) ≡⟨ sym (i2 (q1 ∙ r)) ⟩
+        (q1 ∙ r) ≡⟨ ap (λ p → p ∙ r) (i2 q1) ⟩
+        (refl ∙ q1) ∙ r ∎
+    in J C c x y p q
 ```

-(Proof appears below ap)
-
 ### Definition 2.1.7 (pointed type)

 This comes first, since it is needed to define Theorem 2.1.6.
@ -112,51 +129,18 @@ TODO

 ### Lemma 2.2.1

-```
-ap : {l : Level} {A B : Set l} {x y : A}
-  → (f : A → B)
-  → (p : x ≡ y)
-  → f x ≡ f y
-ap {l} {A} {B} {x} {y} f p = J (λ x y p → f x ≡ f y) (λ x → refl) x y p
-```
+{{#include HottBook.Chapter2Lemma221.md:ap}}

-<details>
-  <summary>Proof of Lemma 2.1.4</summary>
+### Lemma 2.2.2
+
+Ap rules

 ```
-
-lemma2∙1∙4 {A} {x} {y} {z} {w} p q r =
-  let
-    i2 : (x y : A) (p : x ≡ y) → p ≡ refl ∙ p
-    i2 x y p = J (λ x y p → p ≡ refl ∙ p) (λ _ → refl) x y p
-  in record 
-  { i1 = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p
-  ; i2 = i2 x y p
-  ; ii1 = J (λ x y p → (sym p) ∙ p ≡ refl) (λ _ → refl) x y p
-  ; ii2 = J (λ x y p → p ∙ (sym p) ≡ refl) (λ _ → refl) x y p
-  ; iii = J (λ x y p → sym (sym p) ≡ p) (λ _ → refl) x y p
-  ; iv = 
-      let
-        C : (x y : A) → (p : x ≡ y) → Set
-        C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
-
-        wtf : (x : A) (q1 : x ≡ z) → (q1 ∙ r) ≡ (refl ∙ (q1 ∙ r))
-        wtf x q1 = i2 x w (q1 ∙ r)
-
-        wtf2 : (x : A) (q1 : x ≡ z) → q1 ≡ (refl ∙ q1)
-        wtf2 x q1 = i2 x z q1
-
-        wtf3 : (x : A) (q1 : x ≡ z) → (q1 ∙ r) ≡ ((refl ∙ q1) ∙ r)
-        wtf3 x q1 = ap (λ x → x ∙ r) (wtf2 x q1)
-
-        c : (x : A) → C x x refl
-        c x q1 = trans (sym (wtf x q1)) (wtf3 x q1)
-      in J C c x y p q
-  }
+-- module lemma2∙2∙2 {A B : Set} {f : A → B} {x y z : A} {p : x ≡ y} {q : y ≡ z} where
+--   i : ap f (p ∙ q) ≡ ap f p ∙ ap f q
+--   i = J ((λ x1 y1 p1 → (q1 : y1 ≡ z) → ap f (p1 ∙ q1) ≡ ap f p1 ∙ ap f q1)) (λ x1 q1 → {!   !}) x y p q
 ```

-</details>
-
 ## 2.3 Type families are fibrations

 ### Lemma 2.3.1 (Transport)
@ -240,11 +224,7 @@ lemma2∙3∙9 {A} {x} {y} {z} P p q u =
  let 
    f2 : (x1 : A) → (q1 : x1 ≡ z) (u1 : P x1) → transport P q1 u1 ≡ transport P (refl ∙ q1) u1
    f2 x1 q1 u1 =
-      let
-        properties = lemma2∙1∙4 q1 refl refl
-        property = lemma2∙1∙4-statement.i2 properties
-      in
-      ap (λ x → transport P x u1) property
+      ap (λ x → transport P x u1) (lemma2∙1∙4.i2 q1)
    f1 = J (λ x1 y1 p1 → (q1 : y1 ≡ z) → (u1 : P x1) → transport P q1 (transport P p1 u1) ≡ transport P (p1 ∙ q1) u1) f2 x y p
  in f1 q u
 ```
@ -354,14 +334,10 @@ transport-qinv : {A : Set}
 transport-qinv P p = mkQinv (transport P (sym p))
  (λ py → 
    let wtf = lemma2∙3∙9 P (sym p) p py in
-    let properties = lemma2∙1∙4 p refl refl in
-    let property = lemma2∙1∙4-statement.ii1 properties in
-    trans wtf (ap (λ x → transport P x py) property)) 
+    trans wtf (ap (λ x → transport P x py) (lemma2∙1∙4.ii1 p))) 
  (λ px → 
    let wtf = lemma2∙3∙9 P p (sym p) px in
-    let properties = lemma2∙1∙4 p refl refl in
-    let property = lemma2∙1∙4-statement.ii2 properties in
-    trans wtf (ap (λ x → transport P x px) property)) 
+    trans wtf (ap (λ x → transport P x px) (lemma2∙1∙4.ii2 p))) 
 ```

 ### Definition 2.4.10
@ -413,44 +389,45 @@ A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
 ### Lemma 2.4.12

 ```
-id-equiv : (A : Set) → A ≃ A
-id-equiv A = id , e
-  where
-    e : isequiv id
-    e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)
+module lemma2∙4∙12 where
+  id-equiv : (A : Set) → A ≃ A
+  id-equiv A = id , e
+    where
+      e : isequiv id
+      e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)

-sym-equiv : {A B : Set} → (f : A ≃ B) → B ≃ A
-sym-equiv {A} {B} (f , eqv) =
-  let (mkQinv g α β) = isequiv-to-qinv eqv
-  in g , qinv-to-isequiv (mkQinv f β α)
+  sym-equiv : {A B : Set} → (f : A ≃ B) → B ≃ A
+  sym-equiv {A} {B} (f , eqv) =
+    let (mkQinv g α β) = isequiv-to-qinv eqv
+    in g , qinv-to-isequiv (mkQinv f β α)

-trans-equiv : {A B C : Set} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
-trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
-  let
-    (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
-    (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv
+  trans-equiv : {A B C : Set} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
+  trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) =
+    let
+      (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv
+      (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv

-    open ≡-Reasoning
+      open ≡-Reasoning

-    forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
-    forward c =
-      begin
-        ((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
-        (g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
-        (g ∘ id ∘ g-inv) c ≡⟨⟩
-        (g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
-        id c ∎
+      forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id
+      forward c =
+        begin
+          ((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩
+          (g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩
+          (g ∘ id ∘ g-inv) c ≡⟨⟩
+          (g ∘ g-inv) c ≡⟨ g-inv-left c ⟩
+          id c ∎

-    backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
-    backward a =
-      begin
-        ((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
-        (f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
-        (f-inv ∘ (id ∘ f)) a ≡⟨⟩
-        (f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
-        id a ∎
-    
-  in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)
+      backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id
+      backward a =
+        begin
+          ((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩
+          (f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩
+          (f-inv ∘ (id ∘ f)) a ≡⟨⟩
+          (f-inv ∘ f) a ≡⟨ f-inv-right a ⟩
+          id a ∎
+      
+    in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)
 ```

 ## 2.7 Σ-types
@ -578,15 +555,25 @@ postulate
 ### Theorem 2.11.1

 ```
-theorem2∙11∙1 : {A B : Set}
-  → (eqv @ (f , f-eqv) : A ≃ B)
-  → (a a' : A)
-  → (a ≡ a') ≃ (f a ≡ f a')
-theorem2∙11∙1 (f , mkIsEquiv g g-id h h-id) a a' = ap f , qinv-to-isequiv eqv
-  where
-    inv : f a ≡ f a' → a ≡ a'
-    inv p = trans {!   !} (trans (ap g p) {!   !})
-    eqv = mkQinv {! !} {!   !} {!   !}
+-- theorem2∙11∙1 : {A B : Set}
+--   → (eqv @ (f , f-eqv) : A ≃ B)
+--   → (a a' : A)
+--   → (a ≡ a') ≃ (f a ≡ f a')
+-- theorem2∙11∙1 (f , f-eqv) a a' =
+--   let
+--     open ≡-Reasoning
+--     mkQinv f⁻¹ α β = isequiv-to-qinv f-eqv
+--     inv : (f a ≡ f a') → a ≡ a'
+--     inv p = (sym (β a)) ∙ (ap f⁻¹ p) ∙ (β a')
+--     backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
+--     backward q = begin
+--       ap f ((sym (β a)) ∙ (ap f⁻¹ q) ∙ (β a')) ≡⟨ {!   !} ⟩
+--       id q ∎
+--     forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
+--     forward p = {!   !}
+--     eqv = mkQinv inv backward forward
+--   in
+--   ap f , qinv-to-isequiv eqv
 ```

 ## 2.13 Natural numbers
@ -686,4 +673,4 @@ theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl)
  where
    g : (X → A) × (X → B) → (X → A × B)
    g (f1 , f2) = λ x → (f1 x , f2 x)
-```   
+```    
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@ -27,7 +27,7 @@ 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.13
+## Exercise 2.13

 _Show that $(2 \simeq 2) \simeq 2$._

@ -81,11 +81,11 @@ exercise2∙13 = f , equiv
    g true = id , id-equiv
    g false = neg , neg-equiv

-    f∘g∼id : f ∘ g ∼ id
+    f∘g∼id : (f ∘ g) ∼ id
    f∘g∼id true = refl
    f∘g∼id false = refl

-    g∘f∼id : g ∘ f ∼ id
+    g∘f∼id : (g ∘ f) ∼ id
    g∘f∼id e' @ (f' , ie' @ (mkIsEquiv g' g-id h' h-id)) = attempt
      where
        Bmap : 𝟚 → Set
--- a/src/HottBook/Chapter2Lemma221.lagda.md
+++ b/src/HottBook/Chapter2Lemma221.lagda.md
@ -0,0 +1,19 @@
+```
+module HottBook.Chapter2Lemma221 where
+
+open import Agda.Primitive
+open import HottBook.Chapter1
+```
+
+[]: ANCHOR: ap
+
+```
+ap : {l : Level} {A B : Set l} {x y : A}
+  → (f : A → B)
+  → (p : x ≡ y)
+  → f x ≡ f y
+ap {l} {A} {B} {x} {y} f p =
+  J (λ x y p → f x ≡ f y) (λ x → refl) x y p
+```
+
+[]: ANCHOR_END: ap
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@ -5,6 +5,8 @@ open import HottBook.Chapter1
 open import HottBook.Chapter2
 ```

+# 6 Higher inductive types
+
 ### Definition 6.2.2 (Dependent paths)

 ```
@ -31,7 +33,7 @@ postulate

 ### Lemma 6.2.5

-```text
+```
 lemma6∙2∙5 : {A : Set}
  → (a : A)
  → (p : a ≡ a)
@ -45,7 +47,7 @@ lemma6∙2∙5 {A} a p circ = S¹-elim P p-base p-loop circ

    p-loop : transport P loop a ≡ a
    p-loop =
-      let wtf = {! lemma2∙3∙8   !} in
+      let wtf = lemma2∙3∙8 loop in
      {!   !}
 ```

@ -62,8 +64,8 @@ postulate
 ## 6.10 Quotients

 ```
-module Quotient (A : Set) (R : A × A → Prop) where
-  postulate
-    _/_ : Set → Set → Set
-    q : (A : Set) → A / A
+-- module Quotient (A : Set) (R : A × A → Prop) where
+--   postulate
+--     _/_ : Set → Set → Set
+--     q : (A : Set) → A / A
 ```
--- a/src/HottBook/Chapter8.lagda.md
+++ b/src/HottBook/Chapter8.lagda.md
@ -16,6 +16,6 @@ data ℤ : Set where
 ```

 ```
-code : {l : Level} → S¹ → Set (lsuc l)
-code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)
+-- code : {l : Level} → S¹ → Set (lsuc l)
+-- code {l} = S¹-elim (λ _ → Set l) ℤ (ua suc)
 ```