school/type-theory
2
0
Fork 0
Code Issues 11 Pull requests Projects 1 Releases Packages Wiki Activity Actions

2.11.2 - 2.11.4

Browse source
This commit is contained in:
Michael Zhang 2024-05-30 14:10:28 -05:00
parent 9ea3e91e17
commit d89ed0c7a0
7 changed files with 151 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

128
src/HottBook/Chapter2.lagda.md
View file

@ -6,7 +6,7 @@ module HottBook.Chapter2 where
open import Agda.Primitive
open import HottBook.Chapter1
open import HottBook.Chapter2Lemma221
open import HottBook.Chapter2Lemma221 public
open import HottBook.Util
```
@ -738,45 +738,67 @@ open axiom2∙10∙3
### 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 , f-eqv) a a' =
let
open ≡-Reasoning
mkQinv g α β = isequiv-to-qinv f-eqv
inv : (f a ≡ f a') → a ≡ a'
inv p = (sym (β a)) ∙ (ap g p) ∙ (β a')
backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
backward q = begin
ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a') ⟩
ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩
ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩
id q ∎
forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
forward p = begin
(sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩
(sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {! !} ⟩
-- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {! !} ⟩
id p ∎
eqv = mkQinv inv backward forward
in
ap f , qinv-to-isequiv eqv
-- 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 g α β = isequiv-to-qinv f-eqv
-- inv : (f a ≡ f a') → a ≡ a'
-- inv p = (sym (β a)) ∙ (ap g p) ∙ (β a')
-- backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p
-- backward q = begin
-- ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a') ⟩
-- ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩
-- ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩
-- id q ∎
-- forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p
-- forward p = begin
-- (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩
-- (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {! !} ⟩
-- -- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {! !} ⟩
-- id p ∎
-- eqv = mkQinv inv backward forward
-- in
-- ap f , qinv-to-isequiv eqv
```
### Theorem 2.11.2
```
-- module theorem2∙11∙2 where
-- i : {A : Set} {a x1 x2 : A}
-- → (p : x1 ≡ x2)
-- → (q : a ≡ x1)
-- → transport (λ y → a ≡ y) p q ≡ q ∙ p
-- i {A} {a} {x1} {x2} p q =
-- J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1)
-- (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → {! refl !}) a x3 q1)
-- x1 x2 p q
module theorem2∙11∙2 where
open ≡-Reasoning
i : {A : Set} {a x1 x2 : A}
→ (p : x1 ≡ x2)
→ (q : a ≡ x1)
→ transport (λ y → a ≡ y) p q ≡ q ∙ p
i {A} {a} {x1} {x2} p q =
J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1)
(λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → lemma2∙1∙4.i1 q1) a x3 q1)
x1 x2 p q
ii : {A : Set} {a x1 x2 : A}
→ (p : x1 ≡ x2)
→ (q : x1 ≡ a)
→ transport (λ y → y ≡ a) p q ≡ sym p ∙ q
ii {A} {a} {x1} {x2} p q =
J (λ x y p → (q1 : x ≡ a) → transport (λ y → y ≡ a) p q1 ≡ sym p ∙ q1)
(λ x q1 → J (λ x y p → transport (λ y → y ≡ a) refl q1 ≡ sym refl ∙ q1) (λ x → lemma2∙1∙4.i2 q1) x a q1)
x1 x2 p q
iii : {A : Set} {a x1 x2 : A}
→ (p : x1 ≡ x2)
→ (q : x1 ≡ x1)
→ transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
iii {A} {a} {x1} {x2} p q =
J (λ x y p → (q1 : x ≡ x) → transport (λ y → y ≡ y) p q1 ≡ sym p ∙ q1 ∙ p)
(λ x q1 → J (λ x y p → transport (λ y → y ≡ y) refl q1 ≡ sym refl ∙ q1 ∙ refl)
(λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper)
x x q1)
x1 x2 p q
```
### Theorem 2.11.3
@ -786,7 +808,41 @@ theorem2∙11∙3 : {A B : Set} → {f g : A → B} → {a a' : A}
→ (p : a ≡ a')
→ (q : f a ≡ g a)
→ transport (λ x → f x ≡ g x) p q ≡ sym (ap f p) ∙ q ∙ (ap g p)
theorem2∙11∙3 p q = {! !}
theorem2∙11∙3 {A} {B} {f} {g} {a} {a'} p q =
J (λ x y p → (q1 : f x ≡ g x) → transport (λ x → f x ≡ g x) p q1 ≡ sym (ap f p) ∙ q1 ∙ (ap g p))
(λ x q1 →
J (λ x y p → transport (λ z → f z ≡ g z) refl q1 ≡ sym (ap f refl) ∙ q1 ∙ ap g refl)
(λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper)
(f a) (g a) q)
a a' p q
```
### Theorem 2.11.4
```
theorem2∙11∙4 : {A : Set} {B : A → Set} {f g : (x : A) → B x} {a a' : A}
→ (p : a ≡ a')
→ (q : f a ≡ g a)
→ transport (λ x → f x ≡ g x) p q ≡ sym (apd f p) ∙ ap (transport B p) q ∙ apd g p
theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} p q =
let open ≡-Reasoning in
J (λ x y p → (q1 : f x ≡ g x) → transport (λ x → f x ≡ g x) p q1 ≡ sym (apd f p) ∙ ap (transport B p) q1 ∙ apd g p)
(λ x q1 →
J (λ x y p → transport (λ z → f z ≡ g z) refl q1 ≡ sym (apd f refl) ∙ ap (transport B refl) q1 ∙ apd g refl)
(λ y →
let
q2 = ap id q1
q1≡q2 : q1 ≡ q2
q1≡q2 = J (λ a b p → p ≡ ap id p) (λ x → refl) (f x) (g x) q1
in
begin
transport (λ z → f z ≡ g z) refl q1 ≡⟨⟩
q1 ≡⟨ q1≡q2 ⟩
q2 ≡⟨ (let helper = ap (λ p → refl ∙ p) (lemma2∙1∙4.i1 q2) in lemma2∙1∙4.i2 q2 ∙ helper) ⟩
refl ∙ ap (transport B refl) q1 ∙ refl ∎
)
(f a) (g a) q)
a a' p q
```
## 2.12 Coproducts

BIN
src/HottBook/Chapter2.pdf Normal file
View file

Binary file not shown.

59
src/HottBook/Chapter2.typ Normal file
View file

@ -0,0 +1,59 @@
#import "@preview/cetz:0.2.2"
#set page(width: auto, height: auto, margin: .5cm)
#let data = (
([Belgium], 24),
([Germany], 31),
([Greece], 18),
([Spain], 21),
([France], 23),
([Hungary], 18),
([Netherlands], 27),
([Romania], 17),
([Finland], 26),
([Turkey], 13),
)
#cetz.canvas({
import cetz.chart
import cetz.draw: *
// let colors = gradient.linear(red, blue, green, yellow)
// chart.piechart(
// data,
// value-key: 1,
// label-key: 0,
// radius: 4,
// slice-style: colors,
// inner-radius: 1,
// outset: 3,
// inner-label: (content: (value, label) => [#text(white, str(value))], radius: 110%),
// outer-label: (content: "%", radius: 110%))
let point(p, name) = {
content((p.at(0)-0.1, p.at(1)+0.1), name)
circle(p, radius: 0.05, fill: black)
}
circle((2, 1), radius: (1, 1), fill: gray, stroke: none)
circle((2, 3), radius: (1, 0.75), fill: gray, stroke: none)
let a = (1.6, 3)
let b = (2.4, 3)
let fa = (1.6, 1.5)
let fb = (2.4, 1.5)
let ga = (1.3, 0.5)
let gb = (2.7, 0.5)
point(a, "a")
point(b, "b")
point(fa, "f(a)")
point(fb, "f(b)")
point(ga, "g(a)")
point(gb, "g(b)")
line(a, fa)
})

1
src/HottBook/Chapter2Exercises.lagda.md
View file

@ -4,7 +4,6 @@ module HottBook.Chapter2Exercises where
open import Agda.Primitive
open import HottBook.Chapter1
open import HottBook.Chapter2
open import HottBook.Chapter2Lemma221
open import HottBook.Util
```

1
src/HottBook/Chapter3.lagda.md
View file

@ -5,7 +5,6 @@ open import Agda.Primitive
open import HottBook.Chapter1
open import HottBook.Chapter1Util
open import HottBook.Chapter2
open import HottBook.Chapter2Lemma221
open import HottBook.Chapter3Definition331
open import HottBook.Chapter3Lemma333
open import HottBook.Util

1
src/HottBook/Chapter6.lagda.md
View file

@ -3,7 +3,6 @@ module HottBook.Chapter6 where
open import HottBook.Chapter1
open import HottBook.Chapter2
open import HottBook.Chapter2Lemma221
```
# 6 Higher inductive types

1
src/MayConcise/Chapter1.lagda.md
View file

@ -29,5 +29,4 @@ https://en.wikipedia.org/wiki/Homomorphism
## 4 Homotopy invariance
```
_⋆
```