From c2217a27d1bd126a5710f2f1bf99bebb0c4a9ec7 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 1 Nov 2018 01:17:12 +0200 Subject: [PATCH 1/7] preliminary and misc proofs --- library/cool/logic.red | 65 ++++++++++++++++++++++++++++++++++++++++ library/paths/bool.red | 18 +++++++++++ library/paths/hlevel.red | 5 ++++ library/paths/sigma.red | 22 ++++++++++++++ 4 files changed, 110 insertions(+) diff --git a/library/cool/logic.red b/library/cool/logic.red index de9086d5b..b6fcd6c90 100644 --- a/library/cool/logic.red +++ b/library/cool/logic.red @@ -4,6 +4,11 @@ import data.bool import paths.bool import basics.hedberg +import basics.retract +import data.susp +import data.unit +import paths.hlevel + def no-double-neg-elim (f : (A : type) → stable A) : void = let f2 = f bool in @@ -34,3 +39,63 @@ def no-double-neg-elim (f : (A : type) → stable A) : void = def no-excluded-middle (g : (A : type) → dec A) : void = no-double-neg-elim (λ A → dec→stable A (g A)) + +-- 7.2.2 +def mere-relation/set-equiv + (A : type) (R : A → A → type) + (R/prop : (x y : A) → is-prop (R x y)) + (R/refl : (x : A) → R x x) + (R/id : (x y : A) → R x y → path A x y) + : (is-set A) × ((x y : A) → equiv (R x y) (path A x y)) + = + let eq = path-retract/equiv A R (λ a b → + ( R/id a b + , λ p → coe 0 1 (R/refl a) in λ j → R a (p j) + , λ rab → R/prop a b (coe 0 1 (R/refl a) in λ j → R a (R/id a b rab j)) rab + )) in + ( λ x y → coe 0 1 (R/prop x y) in λ j → is-prop (ua _ _ (eq x y) j) + , eq + ) + +-- Hedberg's theorem is a corollary +def paths-stable→set/alt (A : type) (st : (x y : A) → stable (path A x y)) : is-set A = + (mere-relation/set-equiv A (λ x y → neg (neg (path A x y))) + (λ x y → neg/prop (neg (path A x y))) + (λ _ np → np refl) + st + ).fst + +-- 10.1.13 +def suspension-lemma (A : type) (A/prop : is-prop A) : (is-set (susp A)) × (equiv A (path (susp A) north south)) = + let P : susp A → susp A → type = + elim [ + | north → + elim [ + | north → unit + | south → A + | merid b j → symm^1 _ (ua A unit (prop/unit A A/prop b)) j + ] + | south → + elim [ + | north → A + | south → unit + | merid b j → ua A unit (prop/unit A A/prop b) j + ] + | merid a i → + elim [ + | north → symm^1 _ (ua A unit (prop/unit A A/prop a)) i + | south → ua A unit (prop/unit A A/prop a) i + | merid b j → ?merid-hole + ] + ] in + ?suspension-hole + +def choice (X : type) (Y : X → type) : type = (X/set : is-set X) → (Y/set : (x : X) → is-set (Y x)) → ((x : X) → trunc (Y x)) → trunc ((x : X) → Y x) + +def choiceLEM (choice-ax : (X : type) → (Y : X → type) → choice X Y) : (A : type) → (A/prop : is-prop A) → dec A = + λ A A/prop → + let f (b : bool) : susp A = elim b [ + | tt → south + | ff → north + ] in + ?choice-hole \ No newline at end of file diff --git a/library/paths/bool.red b/library/paths/bool.red index db3fd1bd1..dbdd736c6 100644 --- a/library/paths/bool.red +++ b/library/paths/bool.red @@ -3,6 +3,7 @@ import data.void import data.unit import data.bool import basics.isotoequiv +import basics.hedberg def bool-path/code : bool → bool → type = elim [ @@ -24,3 +25,20 @@ def not/equiv : equiv bool bool = def not/path : path^1 type bool bool = ua _ _ not/equiv + +def bool/discrete : discrete bool = + elim [ + | tt → + elim [ + | tt → inl refl + | ff → inr (not/neg ff) + ] + | ff → + elim [ + | tt → inr (not/neg tt) + | ff → inl refl + ] + ] + +def bool/set : is-set bool = + discrete→set bool bool/discrete diff --git a/library/paths/hlevel.red b/library/paths/hlevel.red index c7d87e74a..eb94b319b 100644 --- a/library/paths/hlevel.red +++ b/library/paths/hlevel.red @@ -1,7 +1,12 @@ import prelude +import data.unit +import basics.isotoequiv import paths.sigma import paths.pi +def prop/unit (A : type) (A/prop : is-prop A) (x0 : A) : equiv A unit = + iso→equiv A unit (λ _ → ★, λ _ → x0, unit/prop ★, A/prop x0) + def contr-equiv (A B : type) (A/contr : is-contr A) (B/contr : is-contr B) : equiv A B = diff --git a/library/paths/sigma.red b/library/paths/sigma.red index 44fcd1722..f66cec63e 100644 --- a/library/paths/sigma.red +++ b/library/paths/sigma.red @@ -2,6 +2,28 @@ import prelude import basics.isotoequiv import basics.retract +def sigma/assoc (A : type) (B : A → type) (C : ((x : A) × B x) → type) + : equiv ((x : A) × (y : B x) × C (x, y)) ((p : ((x : A) × B x)) × C p) + = + ( λ x → ((x.fst, x.snd.fst), x.snd.snd) + , λ b → ( ((b.fst.fst, b.fst.snd, b.snd), refl) + , λ c i → + ( ((c.snd i).fst.fst, (c.snd i).fst.snd, (c.snd i).snd) + , λ j → weak-connection/or _ (c.snd) i j + ) + ) + ) + +def sigma/contr/equiv/fst (A : type) (P : A → type) (P/contr : (x : A) → is-contr (P x)) + : equiv ((x : A) × P x) A + = + iso→equiv ((x : A) × P x) A + ( λ s → s.fst + , λ x → (x, (P/contr x).fst) + , refl + , λ s i → (s.fst, symm _ ((P/contr (s.fst)).snd (s.snd)) i) + ) + def sigma/path (A : type) (B : A → type) (a : A) (b : B a) (a' : A) (b' : B a') : equiv ((p : path A a a') × pathd (λ i → B (p i)) b b') (path ((a : A) × B a) (a,b) (a',b')) = From e03394acdff3ddc3e2405cefb868f3cdc1fa0075 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Mon, 5 Nov 2018 19:42:23 +0200 Subject: [PATCH 2/7] WIP using motive --- library/cool/logic.red | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/library/cool/logic.red b/library/cool/logic.red index b6fcd6c90..521912837 100644 --- a/library/cool/logic.red +++ b/library/cool/logic.red @@ -7,6 +7,7 @@ import basics.hedberg import basics.retract import data.susp import data.unit +import data.truncation import paths.hlevel def no-double-neg-elim (f : (A : type) → stable A) : void = @@ -67,26 +68,31 @@ def paths-stable→set/alt (A : type) (st : (x y : A) → stable (path A x y)) : -- 10.1.13 def suspension-lemma (A : type) (A/prop : is-prop A) : (is-set (susp A)) × (equiv A (path (susp A) north south)) = - let P : susp A → susp A → type = - elim [ + let Au (a : A) = ua A unit (prop/unit A A/prop a) in + let uA (a : A) = symm^1 _ (Au a) in + let P (s1 s2 : susp A) : type = + elim s1 [ | north → - elim [ + elim s2 [ | north → unit | south → A - | merid b j → symm^1 _ (ua A unit (prop/unit A A/prop b)) j + | merid b j → uA b j ] | south → - elim [ + elim s2 [ | north → A | south → unit - | merid b j → ua A unit (prop/unit A A/prop b) j + | merid b j → Au b j ] | merid a i → - elim [ - | north → symm^1 _ (ua A unit (prop/unit A A/prop a)) i - | south → ua A unit (prop/unit A A/prop a) i - | merid b j → ?merid-hole - ] + let mot (s : susp A) : type^1 = + path^1 type (elim s [north → unit | south → A | merid b j → uA b j]) (elim s [ north → A | south → unit | merid b j → Au b j]) + in + elim s2 in mot [ + | north → uA a + | south → Au a + | merid b j → λ k → ?merid-hole + ] i ] in ?suspension-hole @@ -98,4 +104,4 @@ def choiceLEM (choice-ax : (X : type) → (Y : X → type) → choice X Y) : (A | tt → south | ff → north ] in - ?choice-hole \ No newline at end of file + ?choice-hole From 8a1c75a63875dc60c12aff8a861714d40ead441b Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Tue, 6 Nov 2018 14:38:38 +0200 Subject: [PATCH 3/7] print mismatched names in Quote --- src/core/Quote.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 41ae779e7..ca0a598e6 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -2,6 +2,7 @@ open Domain open RedBasis open Bwd open BwdNotation +open Name module D = Domain @@ -399,12 +400,12 @@ struct if info0.name = info1.name && info0.twin = info1.twin && info0.ushift = info1.ushift then Tm.Var {name = info0.name; twin = info0.twin; ushift = info0.ushift}, stk else - failwith "global variable name mismatch" + failwith @@ "global variable name mismatch: " ^ to_string info0.name ^ " <> " ^ to_string info1.name | Meta meta0, Meta meta1 -> if meta0.name = meta1.name && meta0.ushift = meta1.ushift then Tm.Meta {name = meta0.name; ushift = meta0.ushift}, stk else - failwith "global variable name mismatch" + failwith @@ "global variable name mismatch: " ^ to_string meta0.name ^ " <> " ^ to_string meta1.name | NHComAtType info0, NHComAtType info1 -> let tr, tr' = equate_dir env info0.dir info1.dir in From d48255d207a73e8f6e7e39c14d43de3a29c248e2 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Tue, 6 Nov 2018 18:55:09 +0200 Subject: [PATCH 4/7] finish defining P --- library/cool/logic.red | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/library/cool/logic.red b/library/cool/logic.red index 521912837..7c4cc9971 100644 --- a/library/cool/logic.red +++ b/library/cool/logic.red @@ -67,7 +67,8 @@ def paths-stable→set/alt (A : type) (st : (x y : A) → stable (path A x y)) : ).fst -- 10.1.13 -def suspension-lemma (A : type) (A/prop : is-prop A) : (is-set (susp A)) × (equiv A (path (susp A) north south)) = +def suspension-lemma (A : type) (A/prop : is-prop A) : + (is-set (susp A)) × (equiv A (path (susp A) north south)) = let Au (a : A) = ua A unit (prop/unit A A/prop a) in let uA (a : A) = symm^1 _ (Au a) in let P (s1 s2 : susp A) : type = @@ -86,14 +87,22 @@ def suspension-lemma (A : type) (A/prop : is-prop A) : (is-set (susp A)) × (equ ] | merid a i → let mot (s : susp A) : type^1 = - path^1 type (elim s [north → unit | south → A | merid b j → uA b j]) (elim s [ north → A | south → unit | merid b j → Au b j]) - in + path^1 + type + (elim s [north → unit | south → A | merid c n → uA c n]) + (elim s [north → A | south → unit | merid c n → Au c n]) + in elim s2 in mot [ | north → uA a | south → Au a - | merid b j → λ k → ?merid-hole + | merid b j → λ i → + comp 0 1 (connection/both^1 type (uA a) (Au a) i j) [ + | i=0 k → uA (A/prop a b k) j + | i=1 k → Au (A/prop a b k) j + | ∂[j] → refl + ] ] i - ] in + ] in ?suspension-hole def choice (X : type) (Y : X → type) : type = (X/set : is-set X) → (Y/set : (x : X) → is-set (Y x)) → ((x : X) → trunc (Y x)) → trunc ((x : X) → Y x) From 23bfe199edd5d27bd49299cd8843cd205d587c0a Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Wed, 7 Nov 2018 18:28:19 +0200 Subject: [PATCH 5/7] fix after review --- src/core/Quote.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/core/Quote.ml b/src/core/Quote.ml index ca0a598e6..344b49bfd 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -2,7 +2,6 @@ open Domain open RedBasis open Bwd open BwdNotation -open Name module D = Domain @@ -400,12 +399,12 @@ struct if info0.name = info1.name && info0.twin = info1.twin && info0.ushift = info1.ushift then Tm.Var {name = info0.name; twin = info0.twin; ushift = info0.ushift}, stk else - failwith @@ "global variable name mismatch: " ^ to_string info0.name ^ " <> " ^ to_string info1.name + failwith @@ "global variable name mismatch: " ^ Name.to_string info0.name ^ " <> " ^ Name.to_string info1.name | Meta meta0, Meta meta1 -> if meta0.name = meta1.name && meta0.ushift = meta1.ushift then Tm.Meta {name = meta0.name; ushift = meta0.ushift}, stk else - failwith @@ "global variable name mismatch: " ^ to_string meta0.name ^ " <> " ^ to_string meta1.name + failwith @@ "global variable name mismatch: " ^ Name.to_string meta0.name ^ " <> " ^ Name.to_string meta1.name | NHComAtType info0, NHComAtType info1 -> let tr, tr' = equate_dir env info0.dir info1.dir in From ac578bd753e1fa43109bf0449f1dc7de019d029e Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 8 Nov 2018 16:56:37 +0200 Subject: [PATCH 6/7] surjective/injective --- library/cool/logic.red | 18 ++++++++++++++++-- library/paths/hlevel.red | 3 +++ 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/library/cool/logic.red b/library/cool/logic.red index 7c4cc9971..3faf5a2ba 100644 --- a/library/cool/logic.red +++ b/library/cool/logic.red @@ -105,9 +105,23 @@ def suspension-lemma (A : type) (A/prop : is-prop A) : ] in ?suspension-hole -def choice (X : type) (Y : X → type) : type = (X/set : is-set X) → (Y/set : (x : X) → is-set (Y x)) → ((x : X) → trunc (Y x)) → trunc ((x : X) → Y x) +def is-surjective (A B : type) (f : A → B) : type = (b : B) → trunc (fiber A B f b) -def choiceLEM (choice-ax : (X : type) → (Y : X → type) → choice X Y) : (A : type) → (A/prop : is-prop A) → dec A = +def is-embedding (A B : type) (f : A → B) : type = (x y : A) → equiv (path A x y) (path B (f x) (f y)) + +def is-injective (A B : type) (A/set : is-set A) (B/set : is-set B) (f : A → B) : type = (x y : A) → path B (f x) (f y) → path A x y + +def injective→embedding (A B : type) (A/set : is-set A) (B/set : is-set B) (f : A → B) : injective A B A/set B/set f → embedding A B f = + λ f/inj x y → + prop/equiv (path A x y) (path B (f x) (f y)) + (A/set x y) (B/set (f x) (f y)) + (λ p i → f (p i)) (f/inj x y) + +def has-choice (X : type) (Y : X → type) : type = (X/set : is-set X) → (Y/set : (x : X) → is-set (Y x)) → ((x : X) → trunc (Y x)) → trunc ((x : X) → Y x) + +def LEM (A : type) : type = (A/prop : is-prop A) → dec A + +def choice→LEM (choice-ax : (X : type) → (Y : X → type) → has-choice X Y) : (A : type) → LEM A = λ A A/prop → let f (b : bool) : susp A = elim b [ | tt → south diff --git a/library/paths/hlevel.red b/library/paths/hlevel.red index eb94b319b..ac448f2d6 100644 --- a/library/paths/hlevel.red +++ b/library/paths/hlevel.red @@ -7,6 +7,9 @@ import paths.pi def prop/unit (A : type) (A/prop : is-prop A) (x0 : A) : equiv A unit = iso→equiv A unit (λ _ → ★, λ _ → x0, unit/prop ★, A/prop x0) +def prop/equiv (P Q : type) (P/prop : is-prop P) (Q/prop : is-prop Q) (f : P → Q) (g : Q → P) : equiv P Q = + iso→equiv P Q (f, g, λ p → Q/prop (f (g p)) p, λ q → P/prop (g (f q)) q) + def contr-equiv (A B : type) (A/contr : is-contr A) (B/contr : is-contr B) : equiv A B = From 97e3c4ab1ac3dbd0db70c0ee29b2fdfa2573203c Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Sat, 24 Nov 2018 00:42:24 +0200 Subject: [PATCH 7/7] WIP reflexivity of P --- library/cool/logic.red | 92 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 90 insertions(+), 2 deletions(-) diff --git a/library/cool/logic.red b/library/cool/logic.red index 3faf5a2ba..9ab26659e 100644 --- a/library/cool/logic.red +++ b/library/cool/logic.red @@ -42,7 +42,7 @@ def no-excluded-middle (g : (A : type) → dec A) : void = no-double-neg-elim (λ A → dec→stable A (g A)) -- 7.2.2 -def mere-relation/set-equiv +def hrel/set-equiv (A : type) (R : A → A → type) (R/prop : (x y : A) → is-prop (R x y)) (R/refl : (x : A) → R x x) @@ -60,12 +60,99 @@ def mere-relation/set-equiv -- Hedberg's theorem is a corollary def paths-stable→set/alt (A : type) (st : (x y : A) → stable (path A x y)) : is-set A = - (mere-relation/set-equiv A (λ x y → neg (neg (path A x y))) + (hrel/set-equiv A (λ x y → neg (neg (path A x y))) (λ x y → neg/prop (neg (path A x y))) (λ _ np → np refl) st ).fst +def P (A : type) (A/prop : is-prop A) (s1 s2 : susp A) : type = + let Au (a : A) = ua A unit (prop/unit A A/prop a) in + let uA (a : A) = symm^1 _ (Au a) in + let Nty : susp A → type = elim [north → unit | south → A | merid c n → uA c n] in + let Sty : susp A → type = elim [north → A | south → unit | merid c n → Au c n] in + elim s1 [ + | north → Nty s2 + | south → Sty s2 + | merid a i → + elim s2 in λ s → path^1 _ (Nty s) (Sty s) [ + | north → uA a + | south → Au a + | merid b j → λ m → + comp 0 1 (connection/both^1 type (uA a) (Au a) m j) [ + | m=0 k → uA (A/prop a b k) j + | m=1 k → Au (A/prop a b k) j + | ∂[j] → refl + ] + ] i + ] + +def P/refl (A : type) (A/prop : is-prop A) (x : susp A) : P A A/prop x x = + let Au (a : A) = ua A unit (prop/unit A A/prop a) in + let uA (a : A) = symm^1 _ (Au a) in + + let pface (B : type) (p : 𝕀 → B) (j i : 𝕀) : B = + comp 1 j (p i) [ + | i=0 → refl + | i=1 → p + ] in + + let pface/ua (a : A) : (i : 𝕀) → pface^1 type (uA a) 0 i + = λ i → + comp 1 0 (coe 1 i a in uA a) in + λ j → pface^1 _ (uA a) j i [ + | i=0 → refl + | i=1 k → coe 1 k a in uA a + ] in + + let qface/ua (a : A) : (i : 𝕀) → trans/filler^1 _ (uA a) (Au a) 1 i + = λ i → + comp 0 1 (coe 1 i a in uA a) in + λ j → trans/filler^1 _ (uA a) (Au a) j i [ + | i=0 → refl + | i=1 → λ k → coe 0 k a in Au a + ] in + + let pq/filler (B : type) (p : 𝕀 → B) (q : [i] B [i=0 → p 1]) (j i : 𝕀) : B = + comp 0 j (p 0) [ + | i=0 → pface B p 0 + | i=1 → trans/filler B p q 1 + ] in + + let pq (a : A) : (i : 𝕀) → pq/filler^1 type (uA a) (Au a) 1 i + = λ i → + comp 0 1 (coe 1 0 a in uA a) in + λ j → pq/filler^1 _ (uA a) (Au a) j i [ + | i=0 → pface/ua a + | i=1 → qface/ua a + ] in + + let pqu/filler (B : type) (p : 𝕀 → B) (q : [i] B [i=0 → p 1]) (j i : 𝕀) : B = + comp 0 1 (pq/filler B p q j i) [ + | i=0 → refl + | i=1 → refl + ] in + + let pqu (a : A) : (i : 𝕀) → pqu/filler^1 type (uA a) (Au a) 1 i + = λ i → + comp 0 1 (box refl [coe 1 0 a in uA a | coe 1 0 a in uA a]) in + λ j → pqu/filler^1 _ (uA a) (Au a) j i [ + | i=0 → pface/ua a + | i=1 → qface/ua a + ] in + + elim x [ + | north → ★ + | south → ★ + | merid a i → pqu a i + ] + +/- +def P/prop (A : type) (A/prop : is-prop A) (x y : susp A) : is-prop (P A A/prop x y) = + λ c d i → ?wat + +def P/id (A : type) (A/prop : is-prop A) (x y : susp A) (Pxy : P A A/prop x y) : path (susp A) x y = ?wat + -- 10.1.13 def suspension-lemma (A : type) (A/prop : is-prop A) : (is-set (susp A)) × (equiv A (path (susp A) north south)) = @@ -128,3 +215,4 @@ def choice→LEM (choice-ax : (X : type) → (Y : X → type) → has-choice X Y | ff → north ] in ?choice-hole +-/ \ No newline at end of file