progress

2024-05-20 02:40:03 -05:00 · 2024-05-20 02:40:03 -05:00 · ce894147d4
commit ce894147d4
parent 8658b6a2f5
9 changed files with 241 additions and 50 deletions
--- a/10
+++ b/10
@ -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
+.PHONY: build-book build-to-html deploy
--- 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]

--- a/html/macros.txt
+++ b/html/macros.txt
@ -0,0 +1 @@
+\refl:{\textrm{refl}}
--- 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
--- 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

 ```
--- 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 ()
--- 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
 ```

--- 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
--- 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