6.4.1
This commit is contained in:
parent
c16fcb2217
commit
00f02ba1ca
4 changed files with 98 additions and 121 deletions
|
@ -488,26 +488,30 @@ module lemma2∙4∙12 where
|
||||||
```
|
```
|
||||||
definition2∙6∙1 : {A B : Set l} {x y : A × B}
|
definition2∙6∙1 : {A B : Set l} {x y : A × B}
|
||||||
→ (p : x ≡ y)
|
→ (p : x ≡ y)
|
||||||
→ (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y)
|
→ (fst x ≡ fst y) × (snd x ≡ snd y)
|
||||||
definition2∙6∙1 p = ap Σ.fst p , ap Σ.snd p
|
definition2∙6∙1 p = ap fst p , ap snd p
|
||||||
```
|
```
|
||||||
|
|
||||||
### Theorem 2.6.2
|
### Theorem 2.6.2
|
||||||
|
|
||||||
```
|
```
|
||||||
module theorem2∙6∙2 where
|
module theorem2∙6∙2 where
|
||||||
pair-≡ : {A B : Set l} {x y : A × B} → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) → x ≡ y
|
private
|
||||||
|
variable
|
||||||
|
A B : Set l
|
||||||
|
x y : A × B
|
||||||
|
|
||||||
|
pair-≡ : (fst x ≡ fst y) × (snd x ≡ snd y) → x ≡ y
|
||||||
pair-≡ (refl , refl) = refl
|
pair-≡ (refl , refl) = refl
|
||||||
|
|
||||||
theorem2∙6∙2 : {A B : Set l} {x y : A × B}
|
backward : ((definition2∙6∙1 {A = A} {B = B} {x = x} {y = y}) ∘ pair-≡) ∼ id
|
||||||
→ isequiv (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y})
|
backward (refl , refl) = refl
|
||||||
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 : (pair-≡ ∘ (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y})) ∼ id
|
||||||
forward refl = refl
|
forward refl = refl
|
||||||
|
|
||||||
|
theorem2∙6∙2 : isequiv (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y})
|
||||||
|
theorem2∙6∙2 = qinv-to-isequiv (mkQinv pair-≡ backward forward)
|
||||||
|
|
||||||
pair-≃ : {A B : Set l} {x y : A × B} → (x ≡ y) ≃ ((fst x ≡ fst y) × (snd x ≡ snd y))
|
pair-≃ : {A B : Set l} {x y : A × B} → (x ≡ y) ≃ ((fst x ≡ fst y) × (snd x ≡ snd y))
|
||||||
pair-≃ = definition2∙6∙1 , theorem2∙6∙2
|
pair-≃ = definition2∙6∙1 , theorem2∙6∙2
|
||||||
|
|
|
@ -84,24 +84,17 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
|
||||||
where
|
where
|
||||||
open theorem2∙6∙2
|
open theorem2∙6∙2
|
||||||
open axiom2∙10∙3
|
open axiom2∙10∙3
|
||||||
|
open isequiv
|
||||||
|
|
||||||
p' : (xa ≡ ya) × (xb ≡ yb)
|
p' = theorem2∙6∙2 .h-id p
|
||||||
p' = definition2∙6∙1 p
|
q' = theorem2∙6∙2 .h-id q
|
||||||
|
|
||||||
q' : (xa ≡ ya) × (xb ≡ yb)
|
pr1 : ap fst p ≡ ap fst q
|
||||||
q' = definition2∙6∙1 q
|
pr1 = A-set xa ya (ap fst p) (ap fst q)
|
||||||
|
pr2 : ap snd p ≡ ap snd q
|
||||||
|
pr2 = B-set xb yb (ap snd p) (ap snd q)
|
||||||
|
|
||||||
lol : {A B : Set l} {x y : A × B} → (x ≡ y) ≡ ((fst x ≡ fst y) × (snd x ≡ snd y))
|
goal = sym p' ∙ ap pair-≡ (pair-≡ (pr1 , pr2)) ∙ q'
|
||||||
lol = ua pair-≃
|
|
||||||
|
|
||||||
convert : (p : (xa , xb) ≡ (ya , yb)) → (xa ≡ ya) × (xb ≡ yb)
|
|
||||||
convert p = definition2∙6∙1 p
|
|
||||||
|
|
||||||
goal : p ≡ q -- (p : (xa, xb)≡(ya, yb)) (q : (xa, xb)≡(ya, yb))
|
|
||||||
-- (p': xa≡ya × xb≡yb)
|
|
||||||
|
|
||||||
goal2 = p' ≡ q'
|
|
||||||
goal = {! ap (λ z → ?) goal2 !}
|
|
||||||
```
|
```
|
||||||
|
|
||||||
### Example 3.1.6
|
### Example 3.1.6
|
||||||
|
@ -432,20 +425,13 @@ module section3∙7 where
|
||||||
∥_∥ : Set l → Set l
|
∥_∥ : Set l → Set l
|
||||||
∣_∣ : {A : Set l} → A → ∥ A ∥
|
∣_∣ : {A : Set l} → A → ∥ A ∥
|
||||||
trunc-witness : {A : Set l} → isProp (∥ A ∥)
|
trunc-witness : {A : Set l} → isProp (∥ A ∥)
|
||||||
|
|
||||||
rec-∥_∥ : (A : Set l) → {B : Set l}
|
|
||||||
→ isProp B
|
|
||||||
→ (f : A → B)
|
|
||||||
→ Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
|
|
||||||
|
|
||||||
trunc-rec : (A : Set) → {B : Set} → isProp B → (f : A → B)
|
rec-trunc : (A : Set) → {B : Set} → isProp B → (f : A → B) → ∥ A ∥ → B
|
||||||
→ ∥ A ∥ → B
|
|
||||||
|
|
||||||
trunc-rec-1 : {A : Set} → {B : Set} → (Bprop : isProp B) → (f : A → B)
|
rec-trunc-1 : {A : Set} → {B : Set} → (Bprop : isProp B) → (f : A → B) → (a : A) → rec-trunc A Bprop f (∣ a ∣) ≡ f a
|
||||||
→ (a : A) → trunc-rec A Bprop f (∣ a ∣) ≡ f a
|
{-# REWRITE rec-trunc-1 #-}
|
||||||
|
|
||||||
open section3∙7 public
|
open section3∙7 public
|
||||||
{-# REWRITE trunc-rec-1 #-}
|
|
||||||
```
|
```
|
||||||
|
|
||||||
### Definition 3.7.1
|
### Definition 3.7.1
|
||||||
|
@ -503,7 +489,7 @@ lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
|
||||||
lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop witness ∣_∣ rec-func
|
lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop witness ∣_∣ rec-func
|
||||||
where
|
where
|
||||||
rec-func : ∥ P ∥ → P
|
rec-func : ∥ P ∥ → P
|
||||||
rec-func = trunc-rec P Pprop id
|
rec-func = rec-trunc P Pprop id
|
||||||
|
|
||||||
witness : isProp ∥ P ∥
|
witness : isProp ∥ P ∥
|
||||||
witness = trunc-witness
|
witness = trunc-witness
|
||||||
|
@ -673,11 +659,11 @@ module lemma3∙11∙9 where
|
||||||
g p = a , p
|
g p = a , p
|
||||||
|
|
||||||
forward : (p : P a) → transport P (sym (aContr a)) p ≡ p
|
forward : (p : P a) → transport P (sym (aContr a)) p ≡ p
|
||||||
forward p = y (sym (aContr a))
|
forward p = admit
|
||||||
where
|
where
|
||||||
y : (q : a ≡ a) → transport P q p ≡ p
|
postulate
|
||||||
y q = {! !}
|
-- TODO
|
||||||
|
admit : transport P (sym (aContr a)) p ≡ p
|
||||||
|
|
||||||
backward : (g ∘ f) ∼ id
|
backward : (g ∘ f) ∼ id
|
||||||
backward (x , p) =
|
backward (x , p) =
|
||||||
|
|
|
@ -95,16 +95,19 @@ lemma4∙1∙1 {A} {B} f e @ (mkQinv g _ _) = goal
|
||||||
### Lemma 4.1.2
|
### Lemma 4.1.2
|
||||||
|
|
||||||
```
|
```
|
||||||
open section3∙7
|
|
||||||
lemma4∙1∙2 : {A : Set} {a : A} (q : a ≡ a)
|
lemma4∙1∙2 : {A : Set} {a : A} (q : a ≡ a)
|
||||||
→ isSet (a ≡ a)
|
→ isSet (a ≡ a)
|
||||||
→ ((x : A) → ∥ a ≡ x ∥)
|
→ (g : (x : A) → ∥ a ≡ x ∥)
|
||||||
→ ((p : a ≡ a) → p ∙ q ≡ q ∙ p)
|
→ ((p : a ≡ a) → p ∙ q ≡ q ∙ p)
|
||||||
→ Σ ((x : A) → x ≡ x) (λ f → f a ≡ q)
|
→ Σ ((x : A) → x ≡ x) (λ f → f a ≡ q)
|
||||||
lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {! !}) , {! !}
|
lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {! !}) , {! !}
|
||||||
where
|
where
|
||||||
allsets : (x y : A) → isSet (x ≡ y)
|
allsets : (x y : A) → isSet (x ≡ y)
|
||||||
allsets x .x refl refl refl refl = refl
|
allsets x y p q r s = {! trunc-witness ? ? !}
|
||||||
|
|
||||||
|
ctx = let
|
||||||
|
f = rec-trunc A {! !} {! g !}
|
||||||
|
in {! !}
|
||||||
|
|
||||||
B : (x : A) → Set
|
B : (x : A) → Set
|
||||||
B x = Σ (x ≡ x) (λ r → (s : a ≡ x) → r ≡ (sym s) ∙ q ∙ s)
|
B x = Σ (x ≡ x) (λ r → (s : a ≡ x) → r ≡ (sym s) ∙ q ∙ s)
|
||||||
|
@ -188,6 +191,20 @@ fib : ∀ {A B} → (f : A → B) → (y : B) → Set
|
||||||
fib {A = A} f y = Σ A (λ x → f x ≡ y)
|
fib {A = A} f y = Σ A (λ x → f x ≡ y)
|
||||||
```
|
```
|
||||||
|
|
||||||
|
### Lemma 4.2.5
|
||||||
|
|
||||||
|
```
|
||||||
|
lemma4∙2∙5 : {A B : Set}
|
||||||
|
→ (f : A → B)
|
||||||
|
→ (y : B)
|
||||||
|
→ ((x , p) (x' , p') : fib f y)
|
||||||
|
→ ((x , p) ≡ (x' , p')) ≃ Σ (x ≡ x') (λ γ → ap f γ ∙ p' ≡ p)
|
||||||
|
lemma4∙2∙5 f y (x , p) (x' , p') = {! !} , {! !}
|
||||||
|
where
|
||||||
|
ff : (x , p) ≡ (x' , p') → Σ (x ≡ x') (λ γ → ap f γ ∙ p' ≡ p)
|
||||||
|
ff q = ap fst q , {! !} -- (_ : f x ≡ f x') ∙ p' ≡ p
|
||||||
|
```
|
||||||
|
|
||||||
### Definition 4.2.7
|
### Definition 4.2.7
|
||||||
|
|
||||||
```
|
```
|
||||||
|
|
|
@ -33,35 +33,28 @@ syntax dep-path P p u v = u ≡[ P , p ] v
|
||||||
|
|
||||||
```
|
```
|
||||||
module Interval where
|
module Interval where
|
||||||
data #I : Set where
|
|
||||||
#0 : #I
|
|
||||||
#1 : #I
|
|
||||||
|
|
||||||
I : Set
|
|
||||||
I = #I
|
|
||||||
|
|
||||||
0I 1I : I
|
|
||||||
0I = #0
|
|
||||||
1I = #1
|
|
||||||
|
|
||||||
postulate
|
postulate
|
||||||
|
I : Set
|
||||||
|
0I 1I : I
|
||||||
seg : 0I ≡ 1I
|
seg : 0I ≡ 1I
|
||||||
|
|
||||||
rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B
|
rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B
|
||||||
rec-Interval b₀ b₁ s #0 = b₀
|
rec-Interval-0I : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 0I ≡ b₀
|
||||||
rec-Interval b₀ b₁ s #1 = b₁
|
rec-Interval-1I : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 1I ≡ b₁
|
||||||
|
{-# REWRITE rec-Interval-0I #-}
|
||||||
|
{-# REWRITE rec-Interval-1I #-}
|
||||||
|
|
||||||
postulate
|
|
||||||
rec-Interval-3 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → apd (rec-Interval b₀ b₁ s) seg ≡ s
|
rec-Interval-3 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → apd (rec-Interval b₀ b₁ s) seg ≡ s
|
||||||
{-# REWRITE rec-Interval-3 #-}
|
{-# REWRITE rec-Interval-3 #-}
|
||||||
|
|
||||||
rec-Interval-d : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → (x : I) → B x
|
rec-Interval-d : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → (x : I) → B x
|
||||||
rec-Interval-d b₀ b₁ s #0 = b₀
|
rec-Interval-d-0I : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → rec-Interval-d {B = B} b₀ b₁ s 0I ≡ b₀
|
||||||
rec-Interval-d b₀ b₁ s #1 = b₁
|
rec-Interval-d-1I : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → rec-Interval-d {B = B} b₀ b₁ s 1I ≡ b₁
|
||||||
|
{-# REWRITE rec-Interval-d-0I #-}
|
||||||
|
{-# REWRITE rec-Interval-d-1I #-}
|
||||||
|
|
||||||
postulate
|
|
||||||
rec-Interval-d-3 : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → apd (rec-Interval-d {B} b₀ b₁ s) seg ≡ s
|
rec-Interval-d-3 : {B : I → Set} → (b₀ : B 0I) → (b₁ : B 1I) → (s : b₀ ≡[ B , seg ] b₁) → apd (rec-Interval-d {B} b₀ b₁ s) seg ≡ s
|
||||||
{-# REWRITE rec-Interval-d-3 #-}
|
{-# REWRITE rec-Interval-d-3 #-}
|
||||||
open Interval public
|
open Interval public
|
||||||
```
|
```
|
||||||
|
|
||||||
|
@ -101,25 +94,18 @@ lemma6∙3∙2 {A = A} {B = B} {f = f} {g = g} p = apd q seg
|
||||||
## 6.4 Circles and sphere
|
## 6.4 Circles and sphere
|
||||||
|
|
||||||
```
|
```
|
||||||
private
|
|
||||||
data #S¹ : Set where
|
|
||||||
#base : #S¹
|
|
||||||
|
|
||||||
S¹ : Set
|
|
||||||
S¹ = #S¹
|
|
||||||
|
|
||||||
base : S¹
|
|
||||||
base = #base
|
|
||||||
|
|
||||||
postulate
|
postulate
|
||||||
|
S¹ : Set
|
||||||
|
base : S¹
|
||||||
loop : base ≡ base
|
loop : base ≡ base
|
||||||
|
|
||||||
rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
|
rec-S¹ : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → ((x : S¹) → P x)
|
||||||
rec-S¹ b l #base = b
|
rec-S¹-base : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → rec-S¹ {P = P} b l base ≡ b
|
||||||
|
{-# REWRITE rec-S¹-base #-}
|
||||||
postulate
|
|
||||||
rec-S¹-loop : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (rec-S¹ b l) loop ≡ l
|
rec-S¹-loop : {l : Level} {P : S¹ → Set l} → (b : P base) → (l : b ≡[ P , loop ] b) → apd {P = P} (rec-S¹ b l) loop ≡ l
|
||||||
{-# REWRITE rec-S¹-loop #-}
|
|
||||||
|
-- TODO: Uncommenting this leads to a bug in the definition of z2 in lemma 6.4.1
|
||||||
|
-- {-# REWRITE rec-S¹-loop #-}
|
||||||
```
|
```
|
||||||
|
|
||||||
### Lemma 6.4.1
|
### Lemma 6.4.1
|
||||||
|
@ -128,54 +114,38 @@ postulate
|
||||||
lemma6∙4∙1 : loop ≢ refl
|
lemma6∙4∙1 : loop ≢ refl
|
||||||
lemma6∙4∙1 loop≡refl = goal3
|
lemma6∙4∙1 loop≡refl = goal3
|
||||||
where
|
where
|
||||||
-- goal : (s : S¹) (p : s ≡ s) → p ≡ refl
|
f : ∀ {l} {A : Set l} {x : A} {p : x ≡ x} → S¹ → A
|
||||||
-- goal s p = z1 ∙ z2 ∙ z3
|
f {A = A} {x = x} {p = p} = rec-S¹ {P = λ _ → A} x p
|
||||||
-- where
|
|
||||||
-- f : {A : Set} {x : A} {p : x ≡ x} → S¹ → A
|
|
||||||
-- f {x = x} {p = p} = rec-S¹ x p
|
|
||||||
|
|
||||||
-- z1 : p ≡ apd f loop
|
|
||||||
-- z1 = refl
|
|
||||||
|
|
||||||
-- z2 : apd f loop ≡ apd f refl
|
|
||||||
-- z2 = ap (apd f) loop≡refl
|
|
||||||
|
|
||||||
-- z3 : apd f refl ≡ refl
|
|
||||||
-- z3 = refl
|
|
||||||
|
|
||||||
goal2 : ∀ {l} {A : Set l} → isSet A
|
goal2 : ∀ {l} {A : Set l} → isSet A
|
||||||
goal2 x .x refl refl = refl
|
goal2 {l = l} {A = A} x .x p refl = z1 ∙ z2 ∙ z3
|
||||||
|
where
|
||||||
|
f' : S¹ → A
|
||||||
|
f' = f {l = l} {A = A} {x = x} {p = p}
|
||||||
|
|
||||||
|
z1 : p ≡ apd f' loop
|
||||||
|
z1 = sym (rec-S¹-loop x p)
|
||||||
|
|
||||||
|
z2 : apd f' loop ≡ apd {x = base} f' refl
|
||||||
|
z2 = ap {A = base ≡ base} (apd f') loop≡refl
|
||||||
|
|
||||||
|
z3 : apd {x = base} f' refl ≡ refl
|
||||||
|
z3 = refl
|
||||||
|
|
||||||
goal3 : ⊥
|
goal3 : ⊥
|
||||||
goal3 = example3∙1∙9 (goal2 {A = Set})
|
goal3 = example3∙1∙9 (goal2 {A = Set})
|
||||||
|
```
|
||||||
|
|
||||||
-- where
|
### Lemma 6.4.2
|
||||||
-- f : {l : Level} {A : Set l} {x : A} {p : x ≡ x} → (S¹ → A)
|
|
||||||
-- f {A = A} {x = x} {p = p} s =
|
|
||||||
-- let p' = transportconst A loop x
|
|
||||||
-- in (rec-S¹ x (p' ∙ p)) s
|
|
||||||
-- -- f-loop : {A : Set} {x : A} {p : x ≡ x} → apd f loop ≡ p
|
|
||||||
-- -- f-loop {x = x} = S¹-rec-loop x ?
|
|
||||||
|
|
||||||
-- goal : ⊥
|
```
|
||||||
|
lemma6∙4∙2 : Σ ((x : S¹) → x ≡ x) (λ y → y ≢ (λ x → refl))
|
||||||
|
lemma6∙4∙2 = f , g
|
||||||
|
where
|
||||||
|
open axiom2∙9∙3
|
||||||
|
|
||||||
-- goal2 : ∀ {l} → (A : Set l) (a : A) (p : a ≡ a) → isSet A
|
f = rec-S¹ loop {! !}
|
||||||
-- goal = example3∙1∙9 (goal2 Set 𝟙 refl)
|
|
||||||
|
|
||||||
-- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl
|
g : f ≡ (λ x → refl) → ⊥
|
||||||
-- goal2 {l} A a p x y r s = {! !}
|
g p = {! !}
|
||||||
-- where
|
|
||||||
-- f' = f {A = A} {x = a} {p = p}
|
|
||||||
-- test = apd f' loop ∙ sym (apd f' loop)
|
|
||||||
|
|
||||||
-- z1 : p ≡ apd f' loop
|
|
||||||
-- z1 = {! !}
|
|
||||||
|
|
||||||
-- z2 : apd f' loop ≡ apd f' refl
|
|
||||||
-- z2 = {! !}
|
|
||||||
|
|
||||||
-- z3 : apd f' refl ≡ refl
|
|
||||||
-- z3 = refl
|
|
||||||
|
|
||||||
-- wtf = let wtf = z1 ∙ z2 ∙ z3 in {! !}
|
|
||||||
```
|
```
|
Loading…
Reference in a new issue