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

2.7

Browse source
This commit is contained in:
Michael Zhang 2024-05-08 19:00:28 -05:00
parent 044e7382ee
commit 4d7ab55b19
2 changed files with 45 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/HottBook/Chapter1.lagda.md
View file

@ -114,7 +114,7 @@ composite : {A B C : Set}
→ A → C
composite f g x = g (f x)
_∘_ : {A B C : Set}
_∘_ : {l : Level} {A B C : Set l}
→ (g : B → C)
→ (f : A → B)
→ A → C

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

@ -205,7 +205,8 @@ Homotopy forms an equivalence relation:
### Definition 2.4.6
```
record qinv {A B : Set} (f : A → B) : Set where
record qinv {l : Level} {A B : Set l} (f : A → B) : Set l where
constructor mkQinv
field
g : B → A
α : f ∘ g ∼ id
@ -215,7 +216,7 @@ record qinv {A B : Set} (f : A → B) : Set where
### Example 2.4.7
```
id-qinv : {A : Set} → qinv {A} id
id-qinv : {l : Level} {A : Set l} → qinv {l} {A} id
id-qinv = record
{ g = id
; α = λ _ → refl
@ -226,7 +227,7 @@ id-qinv = record
### Definition 2.4.10
```
record isequiv {A B : Set} (f : A → B) : Set where
record isequiv {l : Level} {A B : Set l} (f : A → B) : Set l where
constructor mkIsEquiv
field
g : B → A
@ -236,7 +237,7 @@ record isequiv {A B : Set} (f : A → B) : Set where
```
```
qinv-to-isequiv : {A B : Set}
qinv-to-isequiv : {l : Level} {A B : Set l}
→ {f : A → B}
→ qinv f
→ isequiv f
@ -251,8 +252,45 @@ qinv-to-isequiv q = record
### Definition 2.4.11
```
_≃_ : (A B : Set) → Set
A ≃ B = Σ[ f ∈ (A → B) ] isequiv f
_≃_ : {l : Level} → (A B : Set l) → Set l
A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
```
## 2.8 Σ-types
### Theorem 2.7.2
_Suppose that P : A → U is a type family over a type A and let w, w′ : ∑(x:A) P(x). Then there is an equivalence_
```
theorem2∙7∙2 : {l : Level} {A : Set l} {P : A → Set l}
→ ((w @ (w1 , w2)) (w' @ (w'1 , w'2)) : Σ A P)
→ (w ≡ w') ≃ Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2)
theorem2∙7∙2 {l} {A} {P} (w @ (w1 , w2)) (w' @ (w'1 , w'2)) =
f , qinv-to-isequiv (mkQinv g forwards backwards)
where
f : (w ≡ w') → Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2)
f refl = refl , refl
g : Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2) → (w ≡ w')
g (refl , refl) = refl
forwards : f ∘ g ∼ id
forwards (refl , refl) = refl
backwards : g ∘ f ∼ id
backwards refl = refl
```
### Corollary 2.7.3
_For z : ∑(x:A) P(x), we have z = (pr1(z), pr2(z))._
```
corollary2∙7∙3 : {A : Set} {P : A → Set}
→ (z @ (a , b) : Σ A P)
→ z ≡ (a , b)
corollary2∙7∙3 z = refl
```
## 2.8 The unit type