From a44ff3cd4f27f327dafac886fe0cd839a92014c0 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sun, 30 Jun 2024 21:22:14 -0500 Subject: [PATCH] update ch3+4 --- src/CubicalHott/Chapter2.lagda.md | 34 +++--- src/CubicalHott/Chapter3.lagda.md | 13 ++- src/HottBook/Chapter3.lagda.md | 67 ++++++++--- src/HottBook/Chapter3Definition331.lagda.md | 6 +- src/HottBook/Chapter4.lagda.md | 116 ++++++++++++++++++-- 5 files changed, 191 insertions(+), 45 deletions(-) diff --git a/src/CubicalHott/Chapter2.lagda.md b/src/CubicalHott/Chapter2.lagda.md index ae42b9b..72dc340 100644 --- a/src/CubicalHott/Chapter2.lagda.md +++ b/src/CubicalHott/Chapter2.lagda.md @@ -253,26 +253,26 @@ open axiom2∙10∙3 ### Theorem 2.11.2 ``` -module lemma2∙11∙2 where - open ≡-Reasoning +-- module lemma2∙11∙2 where +-- open ≡-Reasoning - i : {l : Level} {A : Type l} {a x1 x2 : A} - → (p : x1 ≡ x2) - → (q : a ≡ x1) - → transport (λ y → a ≡ y) p q ≡ q ∙ p - i {l} {A} {a} {x1} {x2} p q j = {! !} +-- i : {l : Level} {A : Type l} {a x1 x2 : A} +-- → (p : x1 ≡ x2) +-- → (q : a ≡ x1) +-- → transport (λ y → a ≡ y) p q ≡ q ∙ p +-- i {l} {A} {a} {x1} {x2} p q j = {! !} - ii : {l : Level} {A : Type l} {a x1 x2 : A} - → (p : x1 ≡ x2) - → (q : x1 ≡ a) - → transport (λ y → y ≡ a) p q ≡ sym p ∙ q - ii {l} {A} {a} {x1} {x2} p q = {! !} +-- ii : {l : Level} {A : Type l} {a x1 x2 : A} +-- → (p : x1 ≡ x2) +-- → (q : x1 ≡ a) +-- → transport (λ y → y ≡ a) p q ≡ sym p ∙ q +-- ii {l} {A} {a} {x1} {x2} p q = {! !} - iii : {l : Level} {A : Type l} {a x1 x2 : A} - → (p : x1 ≡ x2) - → (q : x1 ≡ x1) - → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p - iii {l} {A} {a} {x1} {x2} p q = {! !} +-- iii : {l : Level} {A : Type l} {a x1 x2 : A} +-- → (p : x1 ≡ x2) +-- → (q : x1 ≡ x1) +-- → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p +-- iii {l} {A} {a} {x1} {x2} p q = {! !} ``` ### Remark 2.12.6 diff --git a/src/CubicalHott/Chapter3.lagda.md b/src/CubicalHott/Chapter3.lagda.md index 91c6441..5a0e344 100644 --- a/src/CubicalHott/Chapter3.lagda.md +++ b/src/CubicalHott/Chapter3.lagda.md @@ -39,6 +39,14 @@ module section3∙7 where data ∥_∥ (A : Type) : Type where ∣_∣ : (a : A) → ∥ A ∥ witness : (x y : ∥ A ∥) → x ≡ y + + rec-∥_∥ : (A : Type) → {B : Type} → isProp B → (f : A → B) + → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a) + rec-∥ A ∥ {B} BisProp f = g , λ _ → refl + where + g : ∥ A ∥ → B + g ∣ a ∣ = f a + g (witness x y i) = BisProp (g x) (g y) i open section3∙7 ``` @@ -64,5 +72,8 @@ postulate ``` lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥ -lemma3∙9∙1 prop = ∣_∣ , {! !} +lemma3∙9∙1 {P} prop = ∣_∣ , qinv-to-isequiv (mkQinv inv {! !} {! !}) + where + inv : ∥ P ∥ → P + inv = {! rec-∥ P ∥ !} ``` \ No newline at end of file diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 1cfc2e5..159f91a 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -81,19 +81,19 @@ is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s ### Lemma 3.1.8 ``` -lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A -lemma3∙1∙8 {A} A-set x y p q r s = - let g = λ q → A-set x y p q in - let - what : {q' : x ≡ y} (r : q ≡ q') → g q ∙ r ≡ g q' - what r = - let what3 = apd g r in - let what4 = lemma2∙11∙2.i r (g q) in - let what5 = {! !} in - sym what4 ∙ what3 - in - -- let what2 = what r in - {! !} +-- lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A +-- lemma3∙1∙8 {A} A-set x y p q r s = +-- let g = λ q → A-set x y p q in +-- let +-- what : {q' : x ≡ y} (r : q ≡ q') → g q ∙ r ≡ g q' +-- what r = +-- let what3 = apd g r in +-- let what4 = lemma2∙11∙2.i r (g q) in +-- let what5 = {! !} in +-- sym what4 ∙ what3 +-- in +-- -- let what2 = what r in +-- {! !} ``` ### Example 3.1.9 @@ -184,6 +184,7 @@ theorem3∙2∙2 double-neg = conclusion let y = what ∙ x in sym y ∙ foranyu + -- postulate huhh : (Σ.fst e) (fbool u) ≡ fbool u huhh = let @@ -193,7 +194,8 @@ theorem3∙2∙2 double-neg = conclusion x e a = {! axiom2∙10∙3.forward ? !} in - sym (x e (fbool u)) ∙ nextStep + {! !} + -- sym (x e (fbool u)) ∙ nextStep finalStep : (x : bool) → ¬ ((Σ.fst e) x ≡ x) finalStep (lift true) p = @@ -274,6 +276,39 @@ module definition3∙4∙3 where ``` module section3∙7 where - data ∥_∥ (A : Set) : Set where - ∣_∣ : (a : A) → ∥ A ∥ + postulate + ∥_∥ : Set → Set + ∣_∣ : {A : Set} → (a : A) → ∥ A ∥ + witness : {A : Set} → (x y : ∥ A ∥) → x ≡ y → Set + rec-∥_∥ : (A : Set) → {B : Set} → isProp B → (f : A → B) + → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a) +open section3∙7 +``` + +### Definition 3.7.1 + +## 3.9 The principle of unique choice + +### Lemma 3.9.1 + +``` +lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥ +lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g + where + thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ id a) + thing = rec-∥ P ∥ prop id + + g = Σ.fst thing + g-prop = Σ.snd thing + + prop2 : isProp ∥ P ∥ + prop2 x y = + let a = g-prop (g x) in + let b = g-prop (g y) in + let eqProp = prop (g x) (g y) in + let + concat : g (∣ g x ∣) ≡ g (∣ g y ∣) + concat = a ∙ eqProp ∙ (sym b) + in + {! prop ? !} ``` \ No newline at end of file diff --git a/src/HottBook/Chapter3Definition331.lagda.md b/src/HottBook/Chapter3Definition331.lagda.md index c97bd0d..c915271 100644 --- a/src/HottBook/Chapter3Definition331.lagda.md +++ b/src/HottBook/Chapter3Definition331.lagda.md @@ -3,6 +3,10 @@ module HottBook.Chapter3Definition331 where open import Agda.Primitive open import HottBook.Chapter1 + +private + variable + l : Level ``` ## Definition 3.3.1 @@ -10,7 +14,7 @@ open import HottBook.Chapter1 [//]: <> (ANCHOR: isProp) ``` -isProp : (P : Set) → Set +isProp : (P : Set l) → Set l isProp P = (x y : P) → x ≡ y ``` diff --git a/src/HottBook/Chapter4.lagda.md b/src/HottBook/Chapter4.lagda.md index 17525f8..6011e70 100644 --- a/src/HottBook/Chapter4.lagda.md +++ b/src/HottBook/Chapter4.lagda.md @@ -4,6 +4,20 @@ module HottBook.Chapter4 where open import HottBook.Chapter1 open import HottBook.Chapter2 open import HottBook.Chapter3 + +private + variable + l : Level +``` + +# Chapter 4 Equivalences + +``` +record satisfies-equivalence-properties {A B : Set} {f : A → B} (isequiv : (A → B) → Set) : Set where + field + qinv→isequiv : qinv f → isequiv f + isequiv→qinv : isequiv f → qinv f + isequiv-isProp : isProp (isequiv f) ``` ## 4.1 Quasi-inverses @@ -11,14 +25,32 @@ open import HottBook.Chapter3 ### Lemma 4.1.1 ``` -lemma4∙1∙1 : {A B : Set} - → (f : A → B) - → qinv f - → qinv f ≃ ((x : A) → x ≡ x) -lemma4∙1∙1 f q = {! !} +lemma4∙1∙1 : {A B : Set} → (f : A → B) → qinv f → qinv f ≃ ((x : A) → x ≡ x) +lemma4∙1∙1 {A} f q = {! !} where ff : qinv f → (x : A) → x ≡ x - ff + ff = {! !} +``` + +### Lemma 4.1.2 + +``` +open section3∙7 +lemma4∙1∙2 : {A : Set} {a : A} (q : a ≡ a) + → isSet (a ≡ a) + → ((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 + + B : (x : A) → Set + B x = Σ (x ≡ x) (λ r → (s : a ≡ x) → r ≡ (sym s) ∙ q ∙ s) + + BisProp : (a : A) → isProp (B a) + BisProp a x y = {! !} ``` ### Theorem 4.1.3 @@ -26,8 +58,72 @@ lemma4∙1∙1 f q = {! !} There exist types A and B and a function f : A → B such that qinv( f ) is not a mere proposition. ``` -theorem4∙1∙3 : {A B : Set} - → (f : A → B) - → isProp (qinv f) → ⊥ -theorem4∙1∙3 f p = {! !} +theorem4∙1∙3 : ∀ {l} {A B : Set l} + → Σ (A → B) (λ f → isProp (qinv f) → ⊥) +theorem4∙1∙3 = {! !} , {! !} + where + goal : Σ (Set (lsuc l)) (λ X → isProp ((x : X) → x ≡ x) → ⊥) + +``` + +## 4.2 Half adjoint equivalences + +### Definition 4.2.1 + +``` +record ishae {A B : Set} (f : A → B) : Set where + constructor mkIshae + field + g : B → A + η : (g ∘ f) ∼ id + ε : (f ∘ g) ∼ id + τ : (x : A) → ap f (η x) ≡ ε (f x) +``` + +### Lemma 4.2.2 + +### Theorem 4.2.3 + +``` +theorem4∙2∙3 : {A B : Set} (f : A → B) → qinv f → ishae f +theorem4∙2∙3 {A} {B} f (mkQinv g ε η) = mkIshae g' η' ε' τ + where + g' : B → A + g' = g + + η' : (g' ∘ f) ∼ id + η' = η + + ε' : (f ∘ g') ∼ id + ε' x = {! !} + + τ : (x : A) → ap f (η' x) ≡ ε' (f x) + τ x = {! !} +``` + +### Definition 4.2.7 + +``` +module definition4∙2∙7 where + linv : ∀ {A B} (f : A → B) → Set + linv {A} {B} f = Σ (B → A) (λ g → (g ∘ f) ∼ id) + + rinv : ∀ {A B} (f : A → B) → Set + rinv {A} {B} f = Σ (B → A) (λ g → (f ∘ g) ∼ id) +``` + +### Definition 4.2.10 + +``` +module definition4∙2∙10 where + open definition4∙2∙7 + + lcoh : ∀ {A} {B} → (f : A → B) → linv f → rinv f → Set + -- lcoh f (g , η) (g , ε) = ? +``` + +### Theorem 4.2.13 + +``` +theorem4∙2∙13 : {A B : Set} (f : A → B) → isProp (ishae f) ``` \ No newline at end of file