progress
This commit is contained in:
parent
36e3186b0f
commit
bab1fe0d9f
|
@ -454,7 +454,7 @@ A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
|
||||||
|
|
||||||
```
|
```
|
||||||
module lemma2∙4∙12 where
|
module lemma2∙4∙12 where
|
||||||
id-equiv : (A : Set) → A ≃ A
|
id-equiv : {l : Level} → (A : Set l) → A ≃ A
|
||||||
id-equiv A = id , e
|
id-equiv A = id , e
|
||||||
where
|
where
|
||||||
e : isequiv id
|
e : isequiv id
|
||||||
|
@ -545,26 +545,46 @@ definition2∙6∙1 p = ap Σ.fst p , ap Σ.snd p
|
||||||
### Theorem 2.6.2
|
### Theorem 2.6.2
|
||||||
|
|
||||||
```
|
```
|
||||||
-- theorem2∙6∙2 : {A B : Set} (x y : A × B)
|
module theorem2∙6∙2 where
|
||||||
-- → isequiv (definition2∙6∙1 {A} {B} {x} {y})
|
pair-≡ : {A B : Set} {x y : A × B} → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) → x ≡ y
|
||||||
-- theorem2∙6∙2 {A} {B} x y = qinv-to-isequiv (mkQinv g {! !} {! !})
|
pair-≡ (refl , refl) = refl
|
||||||
-- 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
|
theorem2∙6∙2 : {A B : Set} {x y : A × B}
|
||||||
-- backward x = {! !}
|
→ isequiv (definition2∙6∙1 {A} {B} {x} {y})
|
||||||
|
theorem2∙6∙2 {A} {B} {x} {y} = qinv-to-isequiv (mkQinv pair-≡ backward forward)
|
||||||
|
where
|
||||||
|
backward : (definition2∙6∙1 ∘ pair-≡) ∼ id
|
||||||
|
backward (refl , refl) = refl
|
||||||
|
|
||||||
|
forward : (pair-≡ ∘ definition2∙6∙1) ∼ id
|
||||||
|
forward refl = refl
|
||||||
|
|
||||||
|
open theorem2∙6∙2 using (pair-≡)
|
||||||
|
```
|
||||||
|
|
||||||
|
### Theorem 2.6.4
|
||||||
|
|
||||||
|
```
|
||||||
|
theorem2∙6∙4 : {Z : Set} {A B : Z → Set} {z w : Z}
|
||||||
|
→ (p : z ≡ w)
|
||||||
|
→ (x : A z × B z)
|
||||||
|
→ transport (λ z → A z × B z) p x ≡ (transport A p (Σ.fst x) , transport B p (Σ.snd x))
|
||||||
|
theorem2∙6∙4 {Z} {A} {B} {z} {w} refl x = refl
|
||||||
```
|
```
|
||||||
|
|
||||||
### Theorem 2.6.5
|
### Theorem 2.6.5
|
||||||
|
|
||||||
```
|
```
|
||||||
|
theorem2∙6∙5 : {A A' B B' : Set} {g : A → A'} {h : B → B'}
|
||||||
|
→ (x y : A × B)
|
||||||
|
→ (p : Σ.fst x ≡ Σ.fst y)
|
||||||
|
→ (q : Σ.snd x ≡ Σ.snd y)
|
||||||
|
→ let
|
||||||
|
f : A × B → A' × B'
|
||||||
|
f z = (g (Σ.fst z) , h (Σ.snd z))
|
||||||
|
in
|
||||||
|
ap f (pair-≡ (p , q)) ≡ pair-≡ (ap g p , ap h q)
|
||||||
|
theorem2∙6∙5 x y refl refl = refl
|
||||||
```
|
```
|
||||||
|
|
||||||
## 2.7 Σ-types
|
## 2.7 Σ-types
|
||||||
|
@ -612,7 +632,7 @@ corollary2∙7∙3 z = refl
|
||||||
-- → {x y : A}
|
-- → {x y : A}
|
||||||
-- → (p : x ≡ y)
|
-- → (p : x ≡ y)
|
||||||
-- → (u z : Σ (P x) (λ u → Q (x , u)))
|
-- → (u z : Σ (P x) (λ u → Q (x , u)))
|
||||||
-- → {! !}
|
-- → transport {! P !} p (u , z) ≡ (transport {! P !} p u , transport {! !} (pair-≡ (p , refl)) z)
|
||||||
```
|
```
|
||||||
|
|
||||||
## 2.8 The unit type
|
## 2.8 The unit type
|
||||||
|
@ -700,18 +720,18 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where
|
||||||
hat B (fst , snd) = B fst snd
|
hat B (fst , snd) = B fst snd
|
||||||
|
|
||||||
--- I have no idea where this goes but this definitely needs to exist
|
--- I have no idea where this goes but this definitely needs to exist
|
||||||
pair-≡ : {A : Set} {B : A → Set} {a1 a2 : A} {b1 : B a1} {b2 : B a2}
|
pair-≡-d : {A : Set} {B : A → Set} {a1 a2 : A} {b1 : B a1} {b2 : B a2}
|
||||||
→ (p : a1 ≡ a2) → (transport B p b1 ≡ b2) → (a1 , b1) ≡ (a2 , b2)
|
→ (p : a1 ≡ a2) → (transport B p b1 ≡ b2) → (a1 , b1) ≡ (a2 , b2)
|
||||||
pair-≡ refl refl = refl
|
pair-≡-d refl refl = refl
|
||||||
|
|
||||||
equation2∙9∙5 : (A : X → Set)
|
equation2∙9∙5 : (A : X → Set)
|
||||||
→ (B : (x : X) → A x → Set)
|
→ (B : (x : X) → A x → Set)
|
||||||
→ (f : (a : A x1) → B x1 a)
|
→ (f : (a : A x1) → B x1 a)
|
||||||
→ (p : x1 ≡ x2)
|
→ (p : x1 ≡ x2)
|
||||||
→ (a : A x2)
|
→ (a : A x2)
|
||||||
→ transport (Π A B) p f a ≡ transport (hat B) (sym (pair-≡ (sym p) refl)) (f (transport A (sym p) a))
|
→ transport (Π A B) p f a ≡ transport (hat B) (sym (pair-≡-d (sym p) refl)) (f (transport A (sym p) a))
|
||||||
equation2∙9∙5 A B f p a =
|
equation2∙9∙5 A B f p a =
|
||||||
J (λ x1' x2' p' → (f' : (a : A x1') → B x1' a) → (a' : A x2') → transport (Π A B) p' f' a' ≡ transport (hat B) (sym (pair-≡ (sym p') refl)) (f' (transport A (sym p') a')))
|
J (λ x1' x2' p' → (f' : (a : A x1') → B x1' a) → (a' : A x2') → transport (Π A B) p' f' a' ≡ transport (hat B) (sym (pair-≡-d (sym p') refl)) (f' (transport A (sym p') a')))
|
||||||
(λ x' f' a' → refl) x1 x2 p f a
|
(λ x' f' a' → refl) x1 x2 p f a
|
||||||
```
|
```
|
||||||
|
|
||||||
|
@ -740,13 +760,14 @@ module equation2∙9∙5 {X : Set} {x1 x2 : X} where
|
||||||
idtoeqv : {l : Level} {A B : Set l}
|
idtoeqv : {l : Level} {A B : Set l}
|
||||||
→ (A ≡ B)
|
→ (A ≡ B)
|
||||||
→ (A ≃ B)
|
→ (A ≃ B)
|
||||||
idtoeqv {l} {A} {B} p = J C c A B p
|
idtoeqv {l} {A} {B} refl = lemma2∙4∙12.id-equiv A
|
||||||
where
|
-- idtoeqv {l} {A} {B} p = J C c A B p
|
||||||
C : (x y : Set l) (p : x ≡ y) → Set l
|
-- where
|
||||||
C x y p = x ≃ y
|
-- C : (x y : Set l) (p : x ≡ y) → Set l
|
||||||
|
-- C x y p = x ≃ y
|
||||||
|
|
||||||
c : (x : Set l) → C x x refl
|
-- c : (x : Set l) → C x x refl
|
||||||
c x = id , qinv-to-isequiv id-qinv
|
-- c x = id , qinv-to-isequiv id-qinv
|
||||||
```
|
```
|
||||||
|
|
||||||
### Axiom 2.10.3 (Univalence)
|
### Axiom 2.10.3 (Univalence)
|
||||||
|
@ -1019,3 +1040,19 @@ theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl)
|
||||||
g : (X → A) × (X → B) → (X → A × B)
|
g : (X → A) × (X → B) → (X → A × B)
|
||||||
g (f1 , f2) = λ x → (f1 x , f2 x)
|
g (f1 , f2) = λ x → (f1 x , f2 x)
|
||||||
```
|
```
|
||||||
|
|
||||||
|
### Equation 2.15.4
|
||||||
|
|
||||||
|
```
|
||||||
|
equation2∙15∙4 : {X : Set} {A B : X → Set}
|
||||||
|
→ ((x : X) → A x × B x)
|
||||||
|
→ ((x : X) → A x) × ((x : X) → B x)
|
||||||
|
equation2∙15∙4 f = ((λ x → Σ.fst (f x)) , λ x → Σ.snd (f x))
|
||||||
|
```
|
||||||
|
|
||||||
|
### Theorem 2.15.5
|
||||||
|
|
||||||
|
```
|
||||||
|
-- theorem2∙15∙5 : isequiv equation2∙15∙4
|
||||||
|
-- theorem2∙15∙5 = qinv-to-isequiv (mkQinv {! !} {! !} {! !})
|
||||||
|
```
|
|
@ -63,9 +63,9 @@ $A$, simultaneously with the type of boundaries for such paths._
|
||||||
[6]: https://git.mzhang.io/school/type-theory/issues/6
|
[6]: https://git.mzhang.io/school/type-theory/issues/6
|
||||||
|
|
||||||
```
|
```
|
||||||
data n-dimensional-path {A : Set} : (n : ℕ) → Set where
|
-- data n-dimensional-path {A : Set} : (n : ℕ) → Set where
|
||||||
z : (x y : A) → x ≡ y → n-dimensional-path zero
|
-- z : (x y : A) → x ≡ y → n-dimensional-path zero
|
||||||
s : (n : ℕ) → (d : n-dimensional-path {A} n) → n-dimensional-path (suc n)
|
-- s : (n : ℕ) → (d : n-dimensional-path {A} n) → n-dimensional-path (suc n)
|
||||||
-- n-dimensional-path {A} zero = (x y : A) → x ≡ y
|
-- n-dimensional-path {A} zero = (x y : A) → x ≡ y
|
||||||
-- n-dimensional-path {A} (suc n) = {! !}
|
-- n-dimensional-path {A} (suc n) = {! !}
|
||||||
```
|
```
|
||||||
|
@ -100,6 +100,38 @@ module exercise2∙5 {A B : Set} {x y : A} {p : x ≡ y} {f : A → B} where
|
||||||
in z3 ∙ z2 ∙ z4
|
in z3 ∙ z2 ∙ z4
|
||||||
```
|
```
|
||||||
|
|
||||||
|
## Exercise 2.6
|
||||||
|
|
||||||
|
```
|
||||||
|
exercise2∙6 : {l : Level} {A : Set l} {x y z : A}
|
||||||
|
→ (p : x ≡ y)
|
||||||
|
→ isequiv (λ (q : y ≡ z) → p ∙ q)
|
||||||
|
exercise2∙6 {l} {A} {x} {y} {z} p = qinv-to-isequiv (mkQinv g forward backward)
|
||||||
|
where
|
||||||
|
f : y ≡ z → x ≡ z
|
||||||
|
f q = p ∙ q
|
||||||
|
|
||||||
|
g : x ≡ z → y ≡ z
|
||||||
|
g q = sym p ∙ q
|
||||||
|
|
||||||
|
forward : (f ∘ g) ∼ id
|
||||||
|
forward q = let
|
||||||
|
z1 = lemma2∙1∙4.ii2 p
|
||||||
|
z2 = ap (λ r → r ∙ q) z1
|
||||||
|
z3 = lemma2∙1∙4.iv p (sym p) q
|
||||||
|
z4 = sym (lemma2∙1∙4.i2 q)
|
||||||
|
in z3 ∙ z2 ∙ z4
|
||||||
|
|
||||||
|
backward : (g ∘ f) ∼ id
|
||||||
|
backward q = let
|
||||||
|
z1 = lemma2∙1∙4.ii1 p
|
||||||
|
z2 = ap (λ r → r ∙ q) z1
|
||||||
|
z3 = lemma2∙1∙4.iv (sym p) p q
|
||||||
|
z4 = sym (lemma2∙1∙4.i2 q)
|
||||||
|
in z3 ∙ z2 ∙ z4
|
||||||
|
|
||||||
|
```
|
||||||
|
|
||||||
## Exercise 2.9
|
## Exercise 2.9
|
||||||
|
|
||||||
Prove that coproducts have the expected universal property,
|
Prove that coproducts have the expected universal property,
|
||||||
|
@ -134,6 +166,10 @@ TODO: Generalizing to dependent functions.
|
||||||
|
|
||||||
## Exercise 2.10
|
## Exercise 2.10
|
||||||
|
|
||||||
|
```
|
||||||
|
|
||||||
|
```
|
||||||
|
|
||||||
## Exercise 2.13
|
## Exercise 2.13
|
||||||
|
|
||||||
_Show that $(2 \simeq 2) \simeq 2$._
|
_Show that $(2 \simeq 2) \simeq 2$._
|
||||||
|
@ -227,3 +263,54 @@ exercise2∙13 = f , equiv
|
||||||
equiv : isequiv f
|
equiv : isequiv f
|
||||||
equiv = mkIsEquiv g f∘g∼id g g∘f∼id
|
equiv = mkIsEquiv g f∘g∼id g g∘f∼id
|
||||||
```
|
```
|
||||||
|
|
||||||
|
## Exercise 2.16
|
||||||
|
|
||||||
|
```
|
||||||
|
module exercise2∙16 where
|
||||||
|
postulate
|
||||||
|
notFunext : {l1 l2 : Level} (A : Set l1) → (B : A → Set l2) → (f g : (x : A) → B x) → (f ∼ g) → (f ≡ g)
|
||||||
|
|
||||||
|
realFunext : {l : Level} {A B : Set l} → {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
|
||||||
|
realFunext {l} {A} {B} {f} {g} p = notFunext A {! B !} {! !} {! !} {! !}
|
||||||
|
```
|
||||||
|
|
||||||
|
## Exercise 2.17
|
||||||
|
|
||||||
|
```
|
||||||
|
module exercise2∙17 where
|
||||||
|
open axiom2∙10∙3 hiding (forward; backward)
|
||||||
|
statement = {A A' B B' : Set} → A ≃ A' → B ≃ B' → (A × B) ≃ (A' × B')
|
||||||
|
|
||||||
|
--- I have no idea where this goes but this definitely needs to exist
|
||||||
|
pair-≡ : {l : Level} {A A' B B' : Set l}
|
||||||
|
→ (p : A ≡ A') → (B ≡ B') → (A × B) ≡ (A' × B')
|
||||||
|
pair-≡ refl refl = refl
|
||||||
|
|
||||||
|
-- Without univalence
|
||||||
|
i : statement
|
||||||
|
i {A} {A'} {B} {B'} (A-eqv @ (Af , A-isequiv)) (B-eqv @ (Bf , B-isequiv)) =
|
||||||
|
f , qinv-to-isequiv (mkQinv g {! !} {! !})
|
||||||
|
where
|
||||||
|
f : (A × B) → (A' × B')
|
||||||
|
f (a , b) = Af a , Bf b
|
||||||
|
|
||||||
|
g : (A' × B') → (A × B)
|
||||||
|
g (a' , b') = (isequiv.g A-isequiv) a' , (isequiv.g B-isequiv) b'
|
||||||
|
|
||||||
|
backward : (f ∘ g) ∼ id
|
||||||
|
backward x = {! !}
|
||||||
|
|
||||||
|
forward : (g ∘ f) ∼ id
|
||||||
|
forward x = {! !}
|
||||||
|
|
||||||
|
-- With univalence
|
||||||
|
ii : statement
|
||||||
|
ii {A} {A'} {B} {B'} A-eqv B-eqv =
|
||||||
|
let
|
||||||
|
A-id = ua A-eqv
|
||||||
|
B-id = ua B-eqv
|
||||||
|
|
||||||
|
combined-id = pair-≡ A-id B-id
|
||||||
|
in idtoeqv combined-id
|
||||||
|
```
|
Loading…
Reference in a new issue