From 00f02ba1ca890e8d753eceaf594e34ab2ed67b75 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 16 Jul 2024 16:41:37 -0400 Subject: [PATCH] 6.4.1 --- src/HottBook/Chapter2.lagda.md | 26 ++++--- src/HottBook/Chapter3.lagda.md | 46 +++++------- src/HottBook/Chapter4.lagda.md | 23 +++++- src/HottBook/Chapter6.lagda.md | 124 +++++++++++++-------------------- 4 files changed, 98 insertions(+), 121 deletions(-) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 92cb64f..27aa8c5 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -488,26 +488,30 @@ module lemma2∙4∙12 where ``` definition2∙6∙1 : {A B : Set l} {x y : A × B} → (p : x ≡ y) - → (Σ.fst x ≡ Σ.fst y) × (Σ.snd x ≡ Σ.snd y) -definition2∙6∙1 p = ap Σ.fst p , ap Σ.snd p + → (fst x ≡ fst y) × (snd x ≡ snd y) +definition2∙6∙1 p = ap fst p , ap snd p ``` ### Theorem 2.6.2 ``` 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 - theorem2∙6∙2 : {A B : Set l} {x y : A × B} - → isequiv (definition2∙6∙1 {A = A} {B = B} {x = x} {y = 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 + backward : ((definition2∙6∙1 {A = A} {B = B} {x = x} {y = y}) ∘ pair-≡) ∼ id + backward (refl , refl) = refl - forward : (pair-≡ ∘ definition2∙6∙1) ∼ id - forward refl = refl + forward : (pair-≡ ∘ (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y})) ∼ id + 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-≃ = definition2∙6∙1 , theorem2∙6∙2 diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 1532194..99de3f8 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -84,24 +84,17 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q where open theorem2∙6∙2 open axiom2∙10∙3 + open isequiv - p' : (xa ≡ ya) × (xb ≡ yb) - p' = definition2∙6∙1 p + p' = theorem2∙6∙2 .h-id p + q' = theorem2∙6∙2 .h-id q - q' : (xa ≡ ya) × (xb ≡ yb) - q' = definition2∙6∙1 q + pr1 : ap fst p ≡ ap fst 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)) - 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 !} + goal = sym p' ∙ ap pair-≡ (pair-≡ (pr1 , pr2)) ∙ q' ``` ### Example 3.1.6 @@ -432,20 +425,13 @@ module section3∙7 where ∥_∥ : Set l → Set l ∣_∣ : {A : Set l} → A → ∥ 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) - → ∥ A ∥ → B + rec-trunc : (A : Set) → {B : Set} → isProp B → (f : A → B) → ∥ A ∥ → B - trunc-rec-1 : {A : Set} → {B : Set} → (Bprop : isProp B) → (f : A → B) - → (a : A) → trunc-rec A Bprop f (∣ a ∣) ≡ f a + rec-trunc-1 : {A : Set} → {B : Set} → (Bprop : isProp B) → (f : A → B) → (a : A) → rec-trunc A Bprop f (∣ a ∣) ≡ f a + {-# REWRITE rec-trunc-1 #-} open section3∙7 public -{-# REWRITE trunc-rec-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 where rec-func : ∥ P ∥ → P - rec-func = trunc-rec P Pprop id + rec-func = rec-trunc P Pprop id witness : isProp ∥ P ∥ witness = trunc-witness @@ -673,11 +659,11 @@ module lemma3∙11∙9 where g p = a , p forward : (p : P a) → transport P (sym (aContr a)) p ≡ p - forward p = y (sym (aContr a)) + forward p = admit where - y : (q : a ≡ a) → transport P q p ≡ p - y q = {! !} - + postulate + -- TODO + admit : transport P (sym (aContr a)) p ≡ p backward : (g ∘ f) ∼ id backward (x , p) = diff --git a/src/HottBook/Chapter4.lagda.md b/src/HottBook/Chapter4.lagda.md index 7b08bd2..16b598c 100644 --- a/src/HottBook/Chapter4.lagda.md +++ b/src/HottBook/Chapter4.lagda.md @@ -95,16 +95,19 @@ lemma4∙1∙1 {A} {B} f e @ (mkQinv g _ _) = goal ### Lemma 4.1.2 ``` -open section3∙7 lemma4∙1∙2 : {A : Set} {a : A} (q : a ≡ a) → isSet (a ≡ a) - → ((x : A) → ∥ a ≡ x ∥) + → (g : (x : A) → ∥ a ≡ x ∥) → ((p : a ≡ a) → p ∙ q ≡ q ∙ p) → Σ ((x : A) → x ≡ x) (λ f → f a ≡ q) lemma4∙1∙2 {A} {a} q prop1 g prop3 = (λ x → {! !}) , {! !} where 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 = Σ (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) ``` +### 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 ``` diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md index 71a0011..c890a58 100644 --- a/src/HottBook/Chapter6.lagda.md +++ b/src/HottBook/Chapter6.lagda.md @@ -33,35 +33,28 @@ syntax dep-path P p u v = u ≡[ P , p ] v ``` module Interval where - data #I : Set where - #0 : #I - #1 : #I - - I : Set - I = #I - - 0I 1I : I - 0I = #0 - 1I = #1 - postulate + I : Set + 0I 1I : I seg : 0I ≡ 1I - rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B - rec-Interval b₀ b₁ s #0 = b₀ - rec-Interval b₀ b₁ s #1 = b₁ + rec-Interval : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → I → B + rec-Interval-0I : {B : Set} → (b₀ b₁ : B) → (s : b₀ ≡ b₁) → rec-Interval b₀ b₁ s 0I ≡ 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 - {-# 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₀ b₁ s #0 = b₀ - rec-Interval-d b₀ b₁ s #1 = b₁ + 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₀ + 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 - {-# REWRITE rec-Interval-d-3 #-} + {-# REWRITE rec-Interval-d-3 #-} 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 ``` -private - data #S¹ : Set where - #base : #S¹ - -S¹ : Set -S¹ = #S¹ - -base : S¹ -base = #base - postulate + S¹ : Set + 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¹ b l #base = b - -postulate + 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 -{-# 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 @@ -128,54 +114,38 @@ postulate lemma6∙4∙1 : loop ≢ refl lemma6∙4∙1 loop≡refl = goal3 where - -- goal : (s : S¹) (p : s ≡ s) → p ≡ refl - -- goal s p = z1 ∙ z2 ∙ z3 - -- 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 + f : ∀ {l} {A : Set l} {x : A} {p : x ≡ x} → S¹ → A + f {A = A} {x = x} {p = p} = rec-S¹ {P = λ _ → A} x p 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 = example3∙1∙9 (goal2 {A = Set}) +``` - -- where - -- 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 ? +### Lemma 6.4.2 - -- 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 - -- goal = example3∙1∙9 (goal2 Set 𝟙 refl) + f = rec-S¹ loop {! !} - -- goal3 : ∀ (s : S¹) (p : s ≡ s) → p ≡ refl - -- goal2 {l} A a p x y r s = {! !} - -- 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 {! !} + g : f ≡ (λ x → refl) → ⊥ + g p = {! !} ``` \ No newline at end of file