wip
This commit is contained in:
parent
3ffdaf1fcb
commit
491b1b87b0
7 changed files with 164 additions and 98 deletions
|
|
@ -83,4 +83,13 @@ lemma6∙4∙2 : Σ ((x : S¹) → x ≡ x) (λ y → y ≢ (λ x → refl))
|
|||
-- z2 = z base
|
||||
-- z3 = lemma6∙4∙1 z2
|
||||
-- in z3
|
||||
```
|
||||
|
||||
```
|
||||
circle-is-contractible : isContr S¹
|
||||
circle-is-contractible = base , f
|
||||
where
|
||||
f : (x : S¹) → base ≡ x
|
||||
f base = refl
|
||||
f (loop i) j = {! !}
|
||||
```
|
||||
|
|
@ -120,6 +120,12 @@ neg true = false
|
|||
neg false = true
|
||||
```
|
||||
|
||||
```
|
||||
if_then_else_ : {A : Set} → 𝟚 → A → A → A
|
||||
if true then x else y = x
|
||||
if false then x else y = y
|
||||
```
|
||||
|
||||
## 1.9 The natural numbers
|
||||
|
||||
```
|
||||
|
|
|
|||
|
|
@ -39,9 +39,7 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
|
|||
𝟙-is-Set tt tt refl refl = refl
|
||||
|
||||
𝟙-isProp : isProp 𝟙
|
||||
𝟙-isProp x y =
|
||||
let (_ , equiv) = theorem2∙8∙1 x y in
|
||||
isequiv.g equiv tt
|
||||
𝟙-isProp tt tt = refl
|
||||
```
|
||||
|
||||
### Example 3.1.3
|
||||
|
|
@ -374,8 +372,8 @@ module definition3∙4∙3 where
|
|||
data decidable-family {A : Set} (B : A → Set) : Set where
|
||||
proof : (a : A) → (B a + (¬ (B a))) → decidable-family B
|
||||
|
||||
data decidable-equality (A : Set) : Set where
|
||||
proof : ((a b : A) → (a ≡ b) + (¬ a ≡ b)) → decidable-equality A
|
||||
decidable-equality : (A : Set) → Set
|
||||
decidable-equality A = (a b : A) → (a ≡ b) + (¬ a ≡ b)
|
||||
```
|
||||
|
||||
## 3.5 Subsets and propositional resizing
|
||||
|
|
|
|||
|
|
@ -83,7 +83,6 @@ module Interval where
|
|||
{-# REWRITE rec-Interval-1I #-}
|
||||
|
||||
rec-Interval-3 : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → apd (rec-Interval b₀ b₁ s) seg ≡ s
|
||||
{-# 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-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₀
|
||||
|
|
@ -92,7 +91,6 @@ module Interval where
|
|||
{-# REWRITE rec-Interval-d-1I #-}
|
||||
|
||||
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 #-}
|
||||
open Interval public
|
||||
```
|
||||
|
||||
|
|
@ -194,38 +192,19 @@ lemma6∙4∙2 = f , g
|
|||
### Corollary 6.4.3
|
||||
|
||||
```
|
||||
corollary6∙4∙3 : (l : Level) → ¬ (is-1-type (Set l))
|
||||
corollary6∙4∙3 l p = {! !}
|
||||
where
|
||||
open lemma2∙4∙12
|
||||
corollary6∙4∙3 : ¬ (is-1-type Set)
|
||||
corollary6∙4∙3 = {! !} where
|
||||
open ≃-Reasoning
|
||||
open lemma2∙4∙12
|
||||
open axiom2∙9∙3
|
||||
open axiom2∙10∙3
|
||||
open S¹
|
||||
|
||||
Circle : Set l
|
||||
Circle = Lift S¹
|
||||
goal : ¬ is-1-type Set
|
||||
|
||||
goal2 : ¬ isSet (S¹ ≡ S¹)
|
||||
goal prf = goal2 (prf S¹ S¹)
|
||||
|
||||
self : Set (lsuc l)
|
||||
self = Circle ≡ Circle
|
||||
|
||||
self-equiv : Set l
|
||||
self-equiv = Circle ≃ Circle
|
||||
|
||||
goal1 : ¬ isSet self-equiv
|
||||
|
||||
goal2 : ¬ isProp (id-equiv Circle ≡ id-equiv Circle)
|
||||
goal1 p = goal2 λ p' q' → p (id-equiv Circle) (id-equiv Circle) p' q'
|
||||
|
||||
goal2 = {! !}
|
||||
|
||||
-- postulate
|
||||
-- equivalence-isProp : isProp self-equiv
|
||||
|
||||
-- goal3 : ¬ isProp (id {A = Circle} ≡ id)
|
||||
-- goal2 prop = goal3 λ x y → {! !}
|
||||
|
||||
-- goal4 : (id {A = Circle} ≡ id) ≃ (id-equiv Circle ≡ id-equiv Circle)
|
||||
-- goal4 = f , {! !}
|
||||
-- where
|
||||
-- f : (id {A = Circle} ≡ id) → (id-equiv Circle ≡ id-equiv Circle)
|
||||
-- f p = ap (λ z → z , {! mkIsEquiv id (λ _ → refl) id (λ _ → refl) !}) p
|
||||
```
|
||||
|
||||
### Lemma 6.4.4
|
||||
|
|
@ -328,36 +307,71 @@ open Suspension public
|
|||
|
||||
```
|
||||
lemma6∙5∙1 : Susp 𝟚 ≃ S¹
|
||||
lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
|
||||
where
|
||||
open S¹
|
||||
lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward) where
|
||||
open S¹
|
||||
open ≡-Reasoning
|
||||
|
||||
m : 𝟚 → base ≡ base
|
||||
m true = refl
|
||||
m false = loop
|
||||
m : 𝟚 → base ≡ base
|
||||
m = λ b → if b then refl else loop
|
||||
|
||||
f : Susp 𝟚 → S¹
|
||||
f s = rec-Susp base base m s
|
||||
f : Susp 𝟚 → S¹
|
||||
f = rec-Susp base base m
|
||||
-- f N = base
|
||||
-- f S = base
|
||||
-- f (merid b) = if b then refl else loop
|
||||
|
||||
g : S¹ → Susp 𝟚
|
||||
g s = rec-S¹ N (merid false ∙ sym (merid true)) s
|
||||
-- g : S¹ → Susp 𝟚
|
||||
-- g base = N
|
||||
-- g loop = (merid false ∙ sym (merid true))
|
||||
g : S¹ → Susp 𝟚
|
||||
g = rec-S¹ N (merid false ∙ sym (merid true))
|
||||
-- g base = N
|
||||
-- g loop = merid false ∙ sym (merid true)
|
||||
|
||||
forward : (f ∘ g) ∼ id
|
||||
forward x = rec-S¹ refl {! !} x
|
||||
|
||||
backward : (x : Susp 𝟚) → g (f x) ≡ x
|
||||
backward x = ind-Susp {P = λ z → g (f z) ≡ z} refl (merid true) goal x where
|
||||
goal : (a : 𝟚) → transport (λ z → g (f z) ≡ z) (merid a) refl ≡ (merid true)
|
||||
|
||||
forward : (f ∘ g) ∼ id
|
||||
forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl p x
|
||||
where
|
||||
p : refl ≡[ (λ x → f (g x) ≡ x) , loop ] refl
|
||||
p = {! merid true !}
|
||||
|
||||
backward : (g ∘ f) ∼ id
|
||||
backward x = ind-Susp {P = λ y → g (f y) ≡ y} refl (merid true) goal x
|
||||
where
|
||||
goal : (y : 𝟚) → transport (λ z → g (f z) ≡ z) (merid y) refl ≡ merid true
|
||||
goal2 : (a : 𝟚) → sym (ap g (ap f (merid a))) ∙ refl ∙ merid a ≡ merid true
|
||||
goal a = {! !}
|
||||
|
||||
goal2 : (y : 𝟚) → {! !} ∙ refl ∙ {! !} ≡ merid true
|
||||
goal y = {! !}
|
||||
goal3 : (a : 𝟚) → sym (ap g (ap f (merid a))) ∙ merid a ≡ merid true
|
||||
goal2 a = ap (sym (ap g (ap f (merid a))) ∙_) (sym (lemma2∙1∙4.i2 (merid a))) ∙ goal3 a
|
||||
|
||||
goal3 true =
|
||||
sym (ap g (ap f (merid true))) ∙ merid true ≡⟨ ap (_∙ merid true) (ap (λ z → sym (ap g z)) (rec-Susp-merid base base m true)) ⟩
|
||||
sym (ap g refl) ∙ merid true ≡⟨ sym (lemma2∙1∙4.i2 (merid true)) ⟩
|
||||
merid true ∎
|
||||
goal3 false = {! !}
|
||||
|
||||
-- lemma6∙5∙1 : Susp 𝟚 ≃ S¹
|
||||
-- lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
|
||||
-- where
|
||||
-- open S¹
|
||||
|
||||
-- m : 𝟚 → base ≡ base
|
||||
-- m true = refl
|
||||
-- m false = loop
|
||||
|
||||
-- f : Susp 𝟚 → S¹
|
||||
-- f s = rec-Susp base base m s
|
||||
|
||||
-- g : S¹ → Susp 𝟚
|
||||
-- g s = rec-S¹ N (merid false ∙ sym (merid true)) s
|
||||
|
||||
-- forward : (f ∘ g) ∼ id
|
||||
-- forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl p x
|
||||
-- where
|
||||
-- p : refl ≡[ (λ x → f (g x) ≡ x) , loop ] refl
|
||||
-- p = {! merid true !}
|
||||
|
||||
-- backward : (g ∘ f) ∼ id
|
||||
-- backward x = ind-Susp {P = λ y → g (f y) ≡ y} refl (merid true) goal x
|
||||
-- where
|
||||
-- goal : (y : 𝟚) → transport (λ z → g (f z) ≡ z) (merid y) refl ≡ merid true
|
||||
|
||||
-- goal2 : (y : 𝟚) → {! !} ∙ refl ∙ {! !} ≡ merid true
|
||||
-- goal y = {! !}
|
||||
```
|
||||
|
||||
### Definition 6.5.2
|
||||
|
|
@ -466,4 +480,6 @@ module Pushout where
|
|||
Pushout : {A B C : Set} → (f : C → A) → (g : C → B) → Set
|
||||
|
||||
syntax Pushout A B C = A ⊔[ C ] B
|
||||
```
|
||||
```
|
||||
|
||||
## asdf
|
||||
|
|
@ -25,13 +25,11 @@ module S¹ where
|
|||
base : S¹
|
||||
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¹-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 #-}
|
||||
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
|
||||
|
||||
-- TODO: Uncommenting this leads to a bug in the definition of z2 in lemma 6.4.1
|
||||
-- {-# REWRITE rec-S¹-loop #-}
|
||||
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
|
||||
open S¹ hiding (base) public
|
||||
```
|
||||
|
||||
|
|
|
|||
|
|
@ -41,6 +41,20 @@ theorem7∙1∙4 {X} {Y} f negtwo q = f (fst q) , λ y → {! !}
|
|||
theorem7∙1∙4 {X} {Y} f (suc n) q = {! !}
|
||||
```
|
||||
|
||||
### Corollary 7.1.5
|
||||
|
||||
```
|
||||
corollary7∙1∙5 : {X Y : Set} → X ≃ Y → (n : ℕ') → is n type X → is n type Y
|
||||
corollary7∙1∙5 eqv n X-ntype = theorem7∙1∙4 (fst eqv) n X-ntype
|
||||
```
|
||||
|
||||
## 7.2 Uniqueness of identity proofs and Hedberg’s theorem
|
||||
|
||||
### Theorem 7.2.1
|
||||
|
||||
```
|
||||
```
|
||||
|
||||
### Theorem 7.2.2
|
||||
|
||||
```
|
||||
|
|
@ -63,27 +77,27 @@ module lemma2∙9∙6 where
|
|||
Prop : {l : Level} → Set (lsuc l)
|
||||
Prop {l} = Σ (Set l) isProp
|
||||
|
||||
theorem7∙2∙2 : {l : Level} {X : Set l} → {R : X → X → Prop {l = l}}
|
||||
→ (ρ : (x : X) → R x x)
|
||||
→ (f : (x y : X) → R x y → x ≡ y) → isSet X
|
||||
theorem7∙2∙2 {X} {R} ρ f = {! !}
|
||||
where
|
||||
variable
|
||||
x : X
|
||||
p : x ≡ x
|
||||
r : R x x
|
||||
-- theorem7∙2∙2 : {l : Level} {X : Set l} → {R : X → X → Prop {l = l}}
|
||||
-- → (ρ : (x : X) → R x x)
|
||||
-- → (f : (x y : X) → R x y → x ≡ y) → isSet X
|
||||
-- theorem7∙2∙2 {X} {R} ρ f = {! !}
|
||||
-- where
|
||||
-- variable
|
||||
-- x : X
|
||||
-- p : x ≡ x
|
||||
-- r : R x x
|
||||
|
||||
apdfp : transport (λ x → x ≡ x) p (f x x (ρ x)) ≡ f x x (ρ x)
|
||||
apdfp {p = p} = apd (λ x → f x x (ρ x)) p
|
||||
-- apdfp : transport (λ x → x ≡ x) p (f x x (ρ x)) ≡ f x x (ρ x)
|
||||
-- apdfp {p = p} = apd (λ x → f x x (ρ x)) p
|
||||
|
||||
step2 : {x : X} {p : x ≡ x}
|
||||
→ (r : R x x)
|
||||
→ transport (λ z → z ≡ z) p (f x x r) ≡ f x x (transport (λ z → R z z) p r)
|
||||
step2 {x} {p} r =
|
||||
let
|
||||
f' = f x x
|
||||
helper = lemma2∙9∙6.stmt {A = λ z → R z z} p f' f'
|
||||
in (fst helper) refl (ρ x)
|
||||
-- step2 : {x : X} {p : x ≡ x}
|
||||
-- → (r : R x x)
|
||||
-- → transport (λ z → z ≡ z) p (f x x r) ≡ f x x (transport (λ z → R z z) p r)
|
||||
-- step2 {x} {p} r =
|
||||
-- let
|
||||
-- f' = f x x
|
||||
-- helper = lemma2∙9∙6.stmt {A = λ z → R z z} p f' f'
|
||||
-- in (fst helper) refl (ρ x)
|
||||
```
|
||||
|
||||
### Lemma 7.2.4
|
||||
|
|
@ -107,14 +121,14 @@ theorem7∙2∙3 x y u =
|
|||
|
||||
```
|
||||
theorem7∙2∙5 : {X : Set} → definition3∙4∙3.decidable-equality X → isSet X
|
||||
theorem7∙2∙5 {X} (definition3∙4∙3.proof f) x y p q with prf ← f x y in eq = helper prf eq
|
||||
where
|
||||
helper : (prf : (x ≡ y) + (x ≡ y → ⊥)) → (f x y ≡ prf) → p ≡ q
|
||||
helper (inl z) eq = theorem7∙2∙3 x y (λ n → n p) x y p q
|
||||
helper (inr g) eq = rec-⊥ (g p)
|
||||
-- theorem7∙2∙5 {X} d x y p q with prf ← d x y in eq = helper prf eq
|
||||
-- where
|
||||
-- helper : (prf : (x ≡ y) + (x ≡ y → ⊥)) → (f x y ≡ prf) → p ≡ q
|
||||
-- helper (inl z) eq = theorem7∙2∙3 x y (λ n → n p) x y p q
|
||||
-- helper (inr g) eq = rec-⊥ (g p)
|
||||
|
||||
hedberg : {X : Set} → definition3∙4∙3.decidable-equality X → isSet X
|
||||
hedberg {X} (definition3∙4∙3.proof d) x y p q = {! !}
|
||||
hedberg {X} d x y p q = {! !}
|
||||
where
|
||||
open ≡-Reasoning
|
||||
-- d : (a b : X) → (a ≡ b) + (¬ a ≡ b)
|
||||
|
|
@ -130,6 +144,7 @@ hedberg {X} (definition3∙4∙3.proof d) x y p q = {! !}
|
|||
helper (inr x) = rec-⊥ (x p)
|
||||
|
||||
r-constant : (x y : X) → (p q : x ≡ y) → r x y p ≡ r x y q
|
||||
r-constant x y p q = {! !}
|
||||
|
||||
s : (x y : X) → x ≡ y → x ≡ y
|
||||
s x y p = sym (r x x refl) ∙ r x y p
|
||||
|
|
@ -152,4 +167,27 @@ hedberg {X} (definition3∙4∙3.proof d) x y p q = {! !}
|
|||
-- helper : (prf : (x ≡ y) + (x ≡ y → ⊥)) → (f x y ≡ prf) → p ≡ q
|
||||
-- helper (inl z) eq = {! !}
|
||||
-- helper (inr g) eq = rec-⊥ (g p)
|
||||
```
|
||||
|
||||
### Theorem 7.2.6
|
||||
|
||||
```
|
||||
open theorem2∙13∙1
|
||||
theorem7∙2∙6 : definition3∙4∙3.decidable-equality ℕ
|
||||
theorem7∙2∙6 zero zero = inl refl
|
||||
theorem7∙2∙6 zero (suc y) = inr (encode zero (suc y))
|
||||
theorem7∙2∙6 (suc x) zero = inr (encode (suc x) zero)
|
||||
theorem7∙2∙6 (suc x) (suc y) with IH ← theorem7∙2∙6 x y = helper IH where
|
||||
helper : (x ≡ y) + (x ≡ y → ⊥) → (suc x ≡ suc y) + (suc x ≡ suc y → ⊥)
|
||||
helper (inl p) = inl (ap suc p)
|
||||
helper (inr f) = inr λ p → f (decode x y (encode (suc x) (suc y) p))
|
||||
```
|
||||
|
||||
### Theorem 7.2.8
|
||||
|
||||
## 7.3 Truncations
|
||||
|
||||
### Lemma 7.3.1
|
||||
|
||||
```
|
||||
```
|
||||
|
|
@ -18,7 +18,7 @@ open import HottBook.CoreUtil
|
|||
### Definition 8.0.1
|
||||
|
||||
```
|
||||
π : (n : ℕ) → (A : Set) → (a : A) → Set
|
||||
-- π : (n : ℕ) → (A : Set) → (a : A) → Set
|
||||
-- π n A a = ∥ ? ∥₀
|
||||
```
|
||||
|
||||
|
|
@ -75,8 +75,9 @@ module definition8∙1∙1 where
|
|||
backward (lift (negsuc zero)) = refl
|
||||
backward (lift (negsuc (suc x))) = refl
|
||||
|
||||
code : {l : Level} → S¹ → Set l
|
||||
code = rec-S¹ Int (ua zsuc-equiv)
|
||||
code : {l : Level} → Lift S¹ → Set l
|
||||
-- code = rec-S¹ Int (ua zsuc-equiv)
|
||||
code (lift s) = rec-S¹ Int (ua zsuc-equiv) s
|
||||
```
|
||||
|
||||
### Lemma 8.1.2
|
||||
|
|
@ -91,10 +92,10 @@ module lemma8∙1∙2 where
|
|||
lifted-loop : {l : Level} → lift base ≡ lift base
|
||||
lifted-loop {l} = ap (lift {l = l}) loop
|
||||
|
||||
i : {l : Level} → (x : Int {l}) → (transport code loop x) ≡ int-suc x
|
||||
i : {l : Level} → (x : Int {l}) → (transport code lifted-loop x) ≡ int-suc x
|
||||
i x = begin
|
||||
(transport code loop x) ≡⟨ lemma2∙3∙10 id code {! lifted-loop !} x ⟩
|
||||
(transport id (ap code loop) x) ≡⟨ {! !} ⟩
|
||||
(transport code lifted-loop x) ≡⟨ lemma2∙3∙10 id code {! lifted-loop !} x ⟩
|
||||
(transport id (ap code lifted-loop) x) ≡⟨ {! !} ⟩
|
||||
-- (transport id (ua int-suc) x) ≡⟨ {! !} ⟩
|
||||
int-suc x ∎
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue