From 13c726ffd0ef04c12dadb277a98d923dc1fe2648 Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 08:56:25 -0400 Subject: [PATCH 1/9] more efficient connections --- connection.red | 44 +++++++++++++++++++++++++++++++++++++------- 1 file changed, 37 insertions(+), 7 deletions(-) diff --git a/connection.red b/connection.red index 301e73c12..eb047e9a7 100644 --- a/connection.red +++ b/connection.red @@ -16,16 +16,16 @@ let connection/or ; definitional equivalence kicks in to make this work. let face : dim → dim → A = λ l k → - comp 0 l (p k) [ + comp 1 l (p 1) [ | k=1 ⇒ auto | k=0 ⇒ p ] in comp 1 0 (p 1) [ | i=0 ⇒ face j - | i=1 ⇒ face 1 + | i=1 ⇒ λ _ → p 1 | j=0 ⇒ face i - | j=1 ⇒ face 1 + | j=1 ⇒ λ _ → p 1 | i=j ⇒ face i ] @@ -42,17 +42,47 @@ let connection/and λ i j → let face : dim → dim → A = λ l k → - comp 1 l (p k) [ + comp 0 l (p 0) [ | k=0 ⇒ auto | k=1 ⇒ p ] in comp 0 1 (p 0) [ - | i=0 ⇒ face 0 + | i=0 ⇒ λ _ → p 0 | i=1 ⇒ face j - | j=0 ⇒ face 0 + | j=0 ⇒ λ _ → p 0 | j=1 ⇒ face i | i=j ⇒ face i ] - +let connection/both + (A : type) + (p : dim → A) (q : [k] A [k=0 ⇒ p 1]) + : [i j] A [ + | j=0 ⇒ p i + | i=0 ⇒ p j + | j=1 ⇒ q i + | i=1 ⇒ q j + ] + = + λ i j → + let pface : dim → dim → A = + λ m k → + comp 1 m (p k) [ + | k=0 ⇒ λ _ → p 0 + | k=1 ⇒ p + ] + in + let qface : dim → dim → A = + λ m k → + comp 0 m (p k) [ + | k=0 ⇒ λ _ → p 0 + | k=1 ⇒ q + ] + in + comp 0 1 (p 0) [ + | i=0 ⇒ pface j + | i=1 ⇒ qface j + | j=0 ⇒ pface i + | j=1 ⇒ qface i + ] From fa0d2b0269fdfb70204df92a4213a95e9666950a Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 09:23:20 -0400 Subject: [PATCH 2/9] basic n-type file --- equivalence.red | 8 +------- ntype.red | 15 +++++++++++++++ univalence.red | 10 +--------- 3 files changed, 17 insertions(+), 16 deletions(-) create mode 100644 ntype.red diff --git a/equivalence.red b/equivalence.red index 14a65f8b3..9ae5da4e6 100644 --- a/equivalence.red +++ b/equivalence.red @@ -1,11 +1,5 @@ import path - -let IsProp (C : type) : type = - (c, c' : _) - → Path C c c' - -let IsContr (C : type) : type = - (c : _) × (c' : _) → Path C c' c +import ntype let Fiber (A, B : type) (f : A → B) (b : B) : type = (a : _) × Path _ (f a) b diff --git a/ntype.red b/ntype.red new file mode 100644 index 000000000..3daec4032 --- /dev/null +++ b/ntype.red @@ -0,0 +1,15 @@ +import path + +let IsContr (C : type) : type = + (c : _) × (c' : _) → Path C c' c + +let IsProp (C : type) : type = + (c, c' : _) + → Path C c c' + +let IsPropOver (A : dim → type) : type = + (a : A 0) → (b : A 1) → PathD A a b + +let IsSet (C : type) : type = + (c, c' : _) + → IsProp (Path C c c') diff --git a/univalence.red b/univalence.red index 73cf62b71..196856008 100644 --- a/univalence.red +++ b/univalence.red @@ -1,18 +1,10 @@ import path +import ntype import equivalence import connection ; the code in this file is adapted from yacctt and redprl -let IsProp (C : type) : type = - (c, c' : _) → - Path C c c' - -let IsSet (C : type) : type = - (c, c' : _) → - IsProp (Path C c c') - - let Retract (A,B : type) (f : A → B) (g : B → A) : type = (a : A) → Path A (g (f a)) a From 24840ed70e45cc8dfa5d27e8aab7634f6fcd394b Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 09:24:58 -0400 Subject: [PATCH 3/9] void and unit --- unit.red | 2 ++ void.red | 6 ++++++ 2 files changed, 8 insertions(+) create mode 100644 unit.red create mode 100644 void.red diff --git a/unit.red b/unit.red new file mode 100644 index 000000000..29f057980 --- /dev/null +++ b/unit.red @@ -0,0 +1,2 @@ +data unit where +| triv diff --git a/void.red b/void.red new file mode 100644 index 000000000..a9f5bb3d3 --- /dev/null +++ b/void.red @@ -0,0 +1,6 @@ +data void where + +let neg (A : type) : type = + A → void + + From efc5376991ca762e3003f66bd5210f73989a408c Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 09:29:53 -0400 Subject: [PATCH 4/9] finish proof of hedberg --- hedberg-wip.red | 42 ------------------------ hedberg.red | 85 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 85 insertions(+), 42 deletions(-) delete mode 100644 hedberg-wip.red create mode 100644 hedberg.red diff --git a/hedberg-wip.red b/hedberg-wip.red deleted file mode 100644 index 222c3bd69..000000000 --- a/hedberg-wip.red +++ /dev/null @@ -1,42 +0,0 @@ -import bool - -;; WIP - -data void where - -let sg/elim - (A : type) (B : A → type) (C : (x : A) (y : B x) → type) - (t : (x : A) × B x) - (m : (x : A) (y : B x) → C x y) - : C (t.0) (t.1) - = - m (t.0) (t.1) - -; Needed until we have parameterized datatypes -let or (A, B : type) : type = - (b : bool) × elim b [tt ⇒ A | ff ⇒ B] - -let or/elim - (A, B : type) - (C : type) - (t : or A B) - (m0 : A → C) - (m1 : B → C) - : C = - sg/elim bool _ (λ _ _ → C) t - (λ b → - elim b [tt ⇒ m0 | ff ⇒ m1]) - -let neg (A : type) : type = - A → void - -let stable (A : type) : type = - (neg (neg A)) → A - -let dec (A : type) : type = - or A (neg A) - -let dec/stable (A : type) (d : dec A) : stable A = - or/elim A (neg A) (stable A) d - (λ a _ → a) - (λ x y → elim (y x) []) diff --git a/hedberg.red b/hedberg.red new file mode 100644 index 000000000..85fb73e90 --- /dev/null +++ b/hedberg.red @@ -0,0 +1,85 @@ +import void +import bool +import connection +import ntype + +let sg/elim + (A : type) (B : A → type) (C : (x : A) (y : B x) → type) + (t : (x : A) × B x) + (m : (x : A) (y : B x) → C x y) + : C (t.0) (t.1) + = + m (t.0) (t.1) + +; Needed until we have parameterized datatypes +let or (A, B : type) : type = + (b : bool) × elim b [tt ⇒ A | ff ⇒ B] + +let or/elim + (A, B : type) + (C : type) + (t : or A B) + (m0 : A → C) + (m1 : B → C) + : C = + sg/elim bool _ (λ _ _ → C) t + (λ b → + elim b [tt ⇒ m0 | ff ⇒ m1]) + +let stable (A : type) : type = + (neg (neg A)) → A + +let dec (A : type) : type = + or A (neg A) + +let discrete (A : type) : type = + (x,y : A) → dec (Path A x y) + +let dec/to/stable (A : type) (d : dec A) : stable A = + or/elim A (neg A) (stable A) d + (λ a _ → a) + (λ x y → elim (y x) []) + +let neg/is-prop-over (A : dim → type) + : IsPropOver (λ i → neg (A i)) + = + λ c c' i a → + let f : [j] ((A j) → void) [ j=0 ⇒ c | j=1 ⇒ c' ] = + elim (c (coe i 0 a in A)) [] + in + f i a + +; Hedberg's theorem for stable path types +let paths-stable/to/set (A : type) + (st : (x,y : A) → stable (Path A x y)) + : IsSet A + = + λ a b p q i j → + let square : dim → dim → A = + λ k m → + comp 0 k a [ + | m=0 ⇒ p + | m=1 ⇒ q + ] + in + let cap : dim → dim → A = + λ k m → st (p k) (q k) (λ c → c (square k)) m + in + comp 0 1 (cap j i) [ + | i=0 ⇒ λ k → + st (p j) (p j) + (neg/is-prop-over (λ j → neg (Path A (p j) (p j))) + (λ c → c (square 0)) + (λ c → c (square 1)) + j) + k + | i=1 ⇒ λ _ → q j + | j=0 ⇒ λ k → connection/or A (cap 0) i k + | j=1 ⇒ λ k → connection/or A (cap 1) i k + ] + +; Hedberg's theorem for decidable path types +let discrete/to/set (A : type) (d : discrete A) + : IsSet A + = + paths-stable/to/set A (λ x y → dec/to/stable (Path A x y) (d x y)) From f506dff0cd4b1e2f5b89e737a693ccfdae17080a Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 09:33:11 -0400 Subject: [PATCH 5/9] file for or --- hedberg.red | 24 +----------------------- or.red | 26 ++++++++++++++++++++++++++ 2 files changed, 27 insertions(+), 23 deletions(-) create mode 100644 or.red diff --git a/hedberg.red b/hedberg.red index 85fb73e90..a1a38029d 100644 --- a/hedberg.red +++ b/hedberg.red @@ -1,31 +1,9 @@ import void import bool +import or import connection import ntype -let sg/elim - (A : type) (B : A → type) (C : (x : A) (y : B x) → type) - (t : (x : A) × B x) - (m : (x : A) (y : B x) → C x y) - : C (t.0) (t.1) - = - m (t.0) (t.1) - -; Needed until we have parameterized datatypes -let or (A, B : type) : type = - (b : bool) × elim b [tt ⇒ A | ff ⇒ B] - -let or/elim - (A, B : type) - (C : type) - (t : or A B) - (m0 : A → C) - (m1 : B → C) - : C = - sg/elim bool _ (λ _ _ → C) t - (λ b → - elim b [tt ⇒ m0 | ff ⇒ m1]) - let stable (A : type) : type = (neg (neg A)) → A diff --git a/or.red b/or.red new file mode 100644 index 000000000..c285726fe --- /dev/null +++ b/or.red @@ -0,0 +1,26 @@ +import bool + +let sg/elim + (A : type) (B : A → type) (C : (x : A) (y : B x) → type) + (t : (x : A) × B x) + (m : (x : A) (y : B x) → C x y) + : C (t.0) (t.1) + = + m (t.0) (t.1) + +; Needed until we have parameterized datatypes +let or (A, B : type) : type = + (b : bool) × elim b [tt ⇒ A | ff ⇒ B] + +let or/elim + (A, B : type) + (C : type) + (t : or A B) + (m0 : A → C) + (m1 : B → C) + : C = + sg/elim bool _ (λ _ _ → C) t + (λ b → + elim b [tt ⇒ m0 | ff ⇒ m1]) + + From f11441c83e0a8920ec613d037d27db6db4a46095 Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 09:34:07 -0400 Subject: [PATCH 6/9] prove nat is a set with hedberg --- nat.red | 51 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 50 insertions(+), 1 deletion(-) diff --git a/nat.red b/nat.red index 7dc57998e..367f3d396 100644 --- a/nat.red +++ b/nat.red @@ -1,5 +1,7 @@ import path - +import void +import unit +import hedberg data nat where | zero @@ -50,3 +52,50 @@ let plus/comm (m : nat) : (n : nat) → Path nat (plus n m) (plus m n) = | suc (m ⇒ plus/comm/m) ⇒ λ n → trans _ (plus/suc/r n m) (λ i → suc (plus/comm/m n i)) ] +let NatPathCode (m : nat) : nat → type = + elim m [ + | zero ⇒ λ n → + elim n [ + | zero ⇒ unit + | suc _ ⇒ void + ] + | suc (m' ⇒ Code/m') ⇒ λ n → + elim n [ + | zero ⇒ void + | suc n' ⇒ Code/m' n' + ] + ] + +let nat-refl (m : nat) : NatPathCode m m = + elim m [ + | zero ⇒ triv + | suc (m' ⇒ nat-refl/m') ⇒ nat-refl/m' + ] + +let nat-path/encode (m : nat) (n : nat) (p : Path nat m n) + : NatPathCode m n + = + coe 0 1 (nat-refl m) in λ i → NatPathCode m (p i) + +let nat/discrete : discrete nat = + λ m → + elim m [ + | zero ⇒ λ n → + elim n [ + | zero ⇒ + | suc n' ⇒ + ] + | suc (m' ⇒ nat/discrete/m') ⇒ λ n → + elim n [ + | zero ⇒ + | suc n' ⇒ + or/elim (Path nat m' n') (neg (Path nat m' n')) + (or (Path nat (suc m') (suc n')) (neg (Path nat (suc m') (suc n')))) + (nat/discrete/m' n') + (λ l → ) + (λ r → ) + ] + ] + +let nat/set : IsSet nat = + discrete/to/set nat nat/discrete From 2aea3ce671f8c42061f9c62ec888c9b1c2d04b12 Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 09:57:54 -0400 Subject: [PATCH 7/9] prove int is a set with hedberg --- int.red | 58 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ nat.red | 2 +- 2 files changed, 59 insertions(+), 1 deletion(-) diff --git a/int.red b/int.red index 614d16817..16942e862 100644 --- a/int.red +++ b/int.red @@ -1,4 +1,6 @@ import path +import void +import unit import nat import equivalence import isotoequiv @@ -50,3 +52,59 @@ let isuc-pred (n : int) : Path int (isuc (pred n)) n = let isuc-equiv : Equiv int int = Iso/Equiv _ _ >> + +let IntPathCode (x : int) : int → type = + elim x [ + | pos m ⇒ λ y → + elim y [ + | pos n ⇒ NatPathCode m n + | negsuc _ ⇒ void + ] + | negsuc m ⇒ λ y → + elim y [ + | pos _ ⇒ void + | negsuc n ⇒ NatPathCode m n + ] + ] + +let int-refl (x : int) : IntPathCode x x = + elim x [ + | pos m ⇒ nat-refl m + | negsuc m ⇒ nat-refl m + ] + +let int-path/encode (x,y : int) (p : Path int x y) + : IntPathCode x y + = + coe 0 1 (int-refl x) in λ i → IntPathCode x (p i) + +let int-repr (x : int) : nat = + elim x [ pos m ⇒ m | negsuc m ⇒ m ] + +let int/discrete : discrete int = + λ x → + elim x [ + | pos m ⇒ λ y → + elim y [ + | pos n ⇒ + or/elim (Path nat m n) (neg (Path nat m n)) + (or (Path int (pos m) (pos n)) (neg (Path int (pos m) (pos n)))) + (nat/discrete m n) + (λ l → ) + (λ r → ) + | negsuc n ⇒ + ] + | negsuc m ⇒ λ y → + elim y [ + | pos n ⇒ + | negsuc n ⇒ + or/elim (Path nat m n) (neg (Path nat m n)) + (or (Path int (negsuc m) (negsuc n)) (neg (Path int (negsuc m) (negsuc n)))) + (nat/discrete m n) + (λ l → ) + (λ r → ) + ] + ] + +let int/set : IsSet int = + discrete/to/set int int/discrete diff --git a/nat.red b/nat.red index 367f3d396..d4ebad5fd 100644 --- a/nat.red +++ b/nat.red @@ -72,7 +72,7 @@ let nat-refl (m : nat) : NatPathCode m m = | suc (m' ⇒ nat-refl/m') ⇒ nat-refl/m' ] -let nat-path/encode (m : nat) (n : nat) (p : Path nat m n) +let nat-path/encode (m,n : nat) (p : Path nat m n) : NatPathCode m n = coe 0 1 (nat-refl m) in λ i → NatPathCode m (p i) From 1949af06357fc07f599ea97253712c269cb88f4a Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 10:07:11 -0400 Subject: [PATCH 8/9] folder for examples --- Makefile | 10 +--------- J.red => example/J.red | 0 example/Makefile | 14 ++++++++++++++ bool.red => example/bool.red | 0 connection.red => example/connection.red | 0 equivalence.red => example/equivalence.red | 0 hedberg.red => example/hedberg.red | 0 int.red => example/int.red | 0 invariance.red => example/invariance.red | 0 isotoequiv.red => example/isotoequiv.red | 0 modal.red => example/modal.red | 0 nat.red => example/nat.red | 0 ntype.red => example/ntype.red | 0 omega1s1-wip.red => example/omega1s1-wip.red | 0 or.red => example/or.red | 0 path.red => example/path.red | 0 s1.red => example/s1.red | 0 torus.red => example/torus.red | 0 unit.red => example/unit.red | 0 univalence.red => example/univalence.red | 0 void.red => example/void.red | 0 21 files changed, 15 insertions(+), 9 deletions(-) rename J.red => example/J.red (100%) create mode 100644 example/Makefile rename bool.red => example/bool.red (100%) rename connection.red => example/connection.red (100%) rename equivalence.red => example/equivalence.red (100%) rename hedberg.red => example/hedberg.red (100%) rename int.red => example/int.red (100%) rename invariance.red => example/invariance.red (100%) rename isotoequiv.red => example/isotoequiv.red (100%) rename modal.red => example/modal.red (100%) rename nat.red => example/nat.red (100%) rename ntype.red => example/ntype.red (100%) rename omega1s1-wip.red => example/omega1s1-wip.red (100%) rename or.red => example/or.red (100%) rename path.red => example/path.red (100%) rename s1.red => example/s1.red (100%) rename torus.red => example/torus.red (100%) rename unit.red => example/unit.red (100%) rename univalence.red => example/univalence.red (100%) rename void.red => example/void.red (100%) diff --git a/Makefile b/Makefile index 695695e39..85e1719aa 100644 --- a/Makefile +++ b/Makefile @@ -19,15 +19,7 @@ help: @${DUNE} exec -- redtt help examples: - ${DUNE} exec -- redtt load-file nat.red - ${DUNE} exec -- redtt load-file int.red - ${DUNE} exec -- redtt load-file bool.red - ${DUNE} exec -- redtt load-file omega1s1-wip.red - ${DUNE} exec -- redtt load-file torus.red - ${DUNE} exec -- redtt load-file modal.red - ${DUNE} exec -- redtt load-file isotoequiv.red - ${DUNE} exec -- redtt load-file invariance.red - ${DUNE} exec -- redtt load-file univalence.red + $(MAKE) -C example all install: ${OPAM} reinstall redtt diff --git a/J.red b/example/J.red similarity index 100% rename from J.red rename to example/J.red diff --git a/example/Makefile b/example/Makefile new file mode 100644 index 000000000..459d8bb90 --- /dev/null +++ b/example/Makefile @@ -0,0 +1,14 @@ +OPAM=opam +EXEC=${OPAM} config exec +DUNE=${EXEC} dune -- + +all: + ${DUNE} exec -- redtt load-file nat.red + ${DUNE} exec -- redtt load-file int.red + ${DUNE} exec -- redtt load-file bool.red + ${DUNE} exec -- redtt load-file omega1s1-wip.red + ${DUNE} exec -- redtt load-file torus.red + ${DUNE} exec -- redtt load-file modal.red + ${DUNE} exec -- redtt load-file isotoequiv.red + ${DUNE} exec -- redtt load-file invariance.red + ${DUNE} exec -- redtt load-file univalence.red diff --git a/bool.red b/example/bool.red similarity index 100% rename from bool.red rename to example/bool.red diff --git a/connection.red b/example/connection.red similarity index 100% rename from connection.red rename to example/connection.red diff --git a/equivalence.red b/example/equivalence.red similarity index 100% rename from equivalence.red rename to example/equivalence.red diff --git a/hedberg.red b/example/hedberg.red similarity index 100% rename from hedberg.red rename to example/hedberg.red diff --git a/int.red b/example/int.red similarity index 100% rename from int.red rename to example/int.red diff --git a/invariance.red b/example/invariance.red similarity index 100% rename from invariance.red rename to example/invariance.red diff --git a/isotoequiv.red b/example/isotoequiv.red similarity index 100% rename from isotoequiv.red rename to example/isotoequiv.red diff --git a/modal.red b/example/modal.red similarity index 100% rename from modal.red rename to example/modal.red diff --git a/nat.red b/example/nat.red similarity index 100% rename from nat.red rename to example/nat.red diff --git a/ntype.red b/example/ntype.red similarity index 100% rename from ntype.red rename to example/ntype.red diff --git a/omega1s1-wip.red b/example/omega1s1-wip.red similarity index 100% rename from omega1s1-wip.red rename to example/omega1s1-wip.red diff --git a/or.red b/example/or.red similarity index 100% rename from or.red rename to example/or.red diff --git a/path.red b/example/path.red similarity index 100% rename from path.red rename to example/path.red diff --git a/s1.red b/example/s1.red similarity index 100% rename from s1.red rename to example/s1.red diff --git a/torus.red b/example/torus.red similarity index 100% rename from torus.red rename to example/torus.red diff --git a/unit.red b/example/unit.red similarity index 100% rename from unit.red rename to example/unit.red diff --git a/univalence.red b/example/univalence.red similarity index 100% rename from univalence.red rename to example/univalence.red diff --git a/void.red b/example/void.red similarity index 100% rename from void.red rename to example/void.red From 250e202925184fe159a158220747c1f851a72c0e Mon Sep 17 00:00:00 2001 From: ecavallo Date: Fri, 17 Aug 2018 12:18:15 -0400 Subject: [PATCH 9/9] prove unit & void are props --- example/unit.red | 12 ++++++++++++ example/void.red | 5 ++++- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/example/unit.red b/example/unit.red index 29f057980..80f142755 100644 --- a/example/unit.red +++ b/example/unit.red @@ -1,2 +1,14 @@ +import ntype + data unit where | triv + +let unit/prop : IsProp unit = + λ a → + elim a [ + | triv ⇒ λ b → + elim b [ triv ⇒ λ _ → triv ] + ] + +let unit/contr : IsContr unit = + < triv , lam a → unit/prop a triv > diff --git a/example/void.red b/example/void.red index a9f5bb3d3..797032ac6 100644 --- a/example/void.red +++ b/example/void.red @@ -1,6 +1,9 @@ +import ntype + data void where let neg (A : type) : type = A → void - +let void/prop : IsProp void = + λ v → elim v []