school/type-theory
2
0
Fork 0
Code Issues 11 Pull requests Projects 1 Releases Packages Wiki Activity Actions

updates

Browse source
This commit is contained in:
Michael Zhang 2024-07-11 02:07:11 -05:00
parent 176e908ac8
commit 56394e55aa
2 changed files with 24 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/CubicalHott/Chapter3.lagda.md
View file

@ -72,8 +72,11 @@ postulate
``` ```
lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥ lemma3∙9∙1 : {P : Type} → isProp P → P ≃ ∥ P ∥
lemma3∙9∙1 {P} prop = ∣_∣ , qinv-to-isequiv (mkQinv inv {! !} {! !}) lemma3∙9∙1 {P} Pprop = ∣_∣ , qinv-to-isequiv (mkQinv inv {! !} {! !})
where where
inv : ∥ P ∥ → P inv : ∥ P ∥ → P
inv = {! rec-∥ P ∥ !} inv ∣ a ∣ = a
inv (witness p q i) =
let what = ap ∥_∥ {! !}
in {! !}
``` ```

31
src/HottBook/Chapter3.lagda.md
View file

@ -319,7 +319,9 @@ module section3∙7 where
∣_∣ : {A : Set l} → (a : A) → ∥ A ∥ ∣_∣ : {A : Set l} → (a : A) → ∥ A ∥
witness : {A : Set l} → (x y : ∥ A ∥) → x ≡ y → Set l witness : {A : Set l} → (x y : ∥ A ∥) → x ≡ y → Set l
rec-∥_∥ : (A : Set l) → {B : Set l} → isProp B → (f : A → B) rec-∥_∥ : (A : Set l) → {B : Set l}
→ isProp B
→ (f : A → B)
→ Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a) → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
open section3∙7 public open section3∙7 public
``` ```
@ -365,9 +367,9 @@ open definition3∙8∙1 public
### Lemma 3.8.2 ### Lemma 3.8.2
``` ```
module lemma3∙8∙2 where -- module lemma3∙8∙2 where
definition3∙8∙3 : {X : Set} → (Y : X → Set) → ((x : X) → isSet (Y x)) → ((x : X) → ∥ (Y x) ∥) → ∥ ((x : X) → Y x) ∥ -- definition3∙8∙3 : {X : Set} → (Y : X → Set) → ((x : X) → isSet (Y x)) → ((x : X) → ∥ (Y x) ∥) → ∥ ((x : X) → Y x) ∥
definition3∙8∙3 {X} Y allYSet = {! !} -- definition3∙8∙3 {X} Y allYSet = {! !}
``` ```
## 3.9 The principle of unique choice ## 3.9 The principle of unique choice
@ -376,11 +378,14 @@ module lemma3∙8∙2 where
``` ```
lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥ lemma3∙9∙1 : {P : Set} → isProp P → P ≃ ∥ P ∥
lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g lemma3∙9∙1 {P} Pprop = lemma3∙3∙3 Pprop prop2 ∣_∣ g
where where
thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ a) open Σ
thing = rec-∥ P ∥ prop id
thing : Σ (∥ P ∥ → P) (λ g → (a : P) → g ∣ a ∣ ≡ a)
thing = rec-∥ P ∥ Pprop id
g : ∥ P ∥ → P
g = Σ.fst thing g = Σ.fst thing
g-prop : (a : P) → g ∣ a ∣ ≡ a g-prop : (a : P) → g ∣ a ∣ ≡ a
@ -390,12 +395,14 @@ lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
-- x y : ∥ P ∥ -- x y : ∥ P ∥
prop2 x y = prop2 x y =
let let
gx = g x gx = g x -- : g x
gy = g y gy = g y -- : g y
eqP = prop gx gy eqP = Pprop gx gy -- : gx ≡ gy
gpx = g-prop gx gpx = g-prop gx -- : g (∣ gx ∣) ≡ gx
what = gpx ∙ eqP
prevResult = (lemma3∙9∙1 {P} Pprop) .snd .isequiv.g-id
in in
admit {! !}
where where
postulate postulate
-- TODO: Finish this -- TODO: Finish this