3.3.4 and 3.3.5

This commit is contained in:
Michael Zhang 2024-07-11 11:03:21 -05:00
parent 41c18cdd32
commit c470464a1e
4 changed files with 69 additions and 8 deletions

View file

@ -2,7 +2,6 @@ GENDIR := html/src/generated
AGDA_SOURCES := $(shell find src -not \( -path src/Misc -prune \) \( -name "*.agda" -o -name "*.lagda.md" \) )
build-to-html:
nu scripts/build-table
find src \
-not \( -path src/Misc -prune \) \
\( -name "*.agda" -o -name "*.lagda.md" \) \
@ -14,7 +13,7 @@ build-to-html:
--html-highlight=auto \
--no-load-primitives \
|| true
fd --no-ignore "html$$" $(GENDIR) -x rm
# fd --no-ignore "html$$" $(GENDIR) -x rm
.PHONY: html/src/generated/Progress.md
@ -25,8 +24,8 @@ html/book/Progress.html: html/src/generated/Progress.md
pandoc \
-f markdown-markdown_in_html_blocks+raw_html \
-t html \
-i html/src/generated/Progress.md \
> html/book/Progress.html
-i $^ \
> $@
html/book/progress/index.html: html/book/Progress.html
cat html/ProgressHeader.html $^ > $@
@ -38,7 +37,7 @@ build-book: build-to-html
refresh-book: build-to-html
mdbook serve html
deploy: build-book html/book/Progress.html
deploy: build-book html/book/progress/index.html
rsync -azr html/book/ root@veil:/home/blogDeploy/public/research
.PHONY: build-book build-to-html deploy

View file

@ -83,8 +83,6 @@ let vizChapter = { |n|
| each { $in | update column1 { do $viz ($in | where completed == "x" | length) ($in | length) } }
| sort-by -n column0
print ($table2 | table)
let newColumn1 = { column0: "Ch", column1: (do $vizCh $n $table) }
let newColumn2 = { column0: "Chnum", column1: $n }

View file

@ -784,7 +784,7 @@ open axiom2∙10∙3
-- ap f , qinv-to-isequiv eqv
```
### Theorem 2.11.2
### Lemma 2.11.2
```
module lemma2∙11∙2 where

View file

@ -270,6 +270,47 @@ lemma3∙3∙2 {P} pp x0 =
{{#include HottBook.Chapter3Lemma333.md:lemma333}}
### Lemma 3.3.4
```
lemma3∙3∙4 : {A : Set} → isProp A → isSet A
lemma3∙3∙4 {A} f x y p q =
let
g : (y : A) → x ≡ y
g y = f x y
step : (y z : A) → (p : y ≡ z) → transport (λ w → x ≡ w) p (g y) ≡ g z
step y z p = apd g p
step2 : (y z : A) → (p : y ≡ z) → (g y) ∙ p ≡ g z
step2 y z p = sym (lemma2∙11∙2.i p (g y)) ∙ step y z p
step3 : (y z : A) → (p : y ≡ z) → p ≡ sym (g y) ∙ (g z)
step3 y z p =
lemma2∙1∙4.i2 p
∙ ap (λ q → q ∙ p) (sym (lemma2∙1∙4.ii1 (g y)))
∙ sym (lemma2∙1∙4.iv (sym (g y)) (g y) p)
∙ ap (λ q → sym (g y) ∙ q) (step2 y z p)
step4 = step3 x y p
step5 = step3 x y q
in step4 ∙ sym step5
```
### Lemma 3.3.5
```
module lemma3∙3∙5 where
open axiom2∙9∙3
i : {A : Set} → isProp (isProp (A))
i f g = funext λ x → funext λ y → (lemma3∙3∙4 f) x y (f x y) (g x y)
ii : {A : Set} → isProp (isSet (A))
ii f g = funext λ x → funext λ y → funext λ p → funext λ q →
(lemma3∙1∙8 f) x y p q (f x y p q) (g x y p q)
```
## 3.4 Classical vs. intuitionistic logic
### Definition 3.4.3
@ -409,6 +450,18 @@ lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop prop2 _ g
admit : x ≡ y
```
### Corollary 3.9.2
Principle of unique choice
```
-- corollary3∙9∙2 : {A : Set} {P : A → Set}
-- → ((x : A) → isProp (P x))
-- → ((x : A) → ∥ P x ∥)
-- → (x : A) → P x
-- corollary3∙9∙2 assump1 assump2 x = {! !}
```
## 3.11 Contractibility
### Definition 3.11.1
@ -564,4 +617,15 @@ module lemma3∙11∙9 where
where
y : (q : a ≡ x) → transport P q (transport P (sym q) p) ≡ p
y refl = refl
```
### Lemma 3.11.10
```
module lemma3∙11∙10 where
i : {A : Set} → ((x y : A) → isContr (x ≡ y)) → isProp A
i f x y = Σ.fst (f x y)
ii : {A : Set} → isProp A → ((x y : A) → isContr (x ≡ y))
ii f x y = f x y , λ z → {! !}
```