Hedberg (#245)

* more efficient connections * basic n-type file * void and unit * finish proof of hedberg * file for or * prove nat is a set with hedberg * prove int is a set with hedberg * folder for examples * prove unit & void are props
RedPRL · Aug 17, 2018 · 26f0b40 · 26f0b40
1 parent 1a5fd04
commit 26f0b40
Show file tree

Hide file tree

Showing 23 changed files with 366 additions and 152 deletions.
diff --git 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 → example/J.red b/J.red → example/J.red
diff --git a/example/Makefile 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 → example/bool.red b/bool.red → example/bool.red
diff --git a/connection.red → example/connection.red b/connection.red → example/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
+    ]
diff --git a/equivalence.red → example/equivalence.red b/equivalence.red → example/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/example/hedberg.red b/example/hedberg.red
@@ -0,0 +1,63 @@
+import void
+import bool
+import or
+import connection
+import ntype
+
+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))
diff --git a/example/int.red b/example/int.red
@@ -0,0 +1,110 @@
+import path
+import void
+import unit
+import nat
+import equivalence
+import isotoequiv
+
+data int where
+| pos [n : nat]
+| negsuc [n : nat]
+
+let pred (x : int) : int =
+  elim x [
+  | pos n ⇒
+    elim n [
+    | zero ⇒ negsuc zero
+    | suc n ⇒ pos n
+    ]
+  | negsuc n ⇒ negsuc (suc n)
+  ]
+
+let isuc (x : int) : int =
+  elim x [
+  | pos n ⇒ pos (suc n)
+  | negsuc n ⇒
+    elim n [
+    | zero ⇒ pos zero
+    | suc n ⇒ negsuc n
+    ]
+  ]
+
+
+let pred-isuc (n : int) : Path int (pred (isuc n)) n =
+  elim n [
+  | pos n ⇒ auto
+  | negsuc n ⇒
+    elim n [
+    | zero ⇒ auto
+    | suc n ⇒ auto
+    ]
+  ]
+
+let isuc-pred (n : int) : Path int (isuc (pred n)) n =
+  elim n [
+  | pos n ⇒
+    elim n [
+    | zero ⇒ auto
+    | suc n' ⇒ auto
+    ]
+  | negsuc n ⇒ auto
+  ]
+
+let isuc-equiv : Equiv int int =
+  Iso/Equiv _ _ <isuc, <pred, <isuc-pred, pred-isuc>>>
+
+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 → <tt, λ i → pos (l i)>)
+        (λ r → <ff, λ p → r (λ i → int-repr (p i))>)
+    | negsuc n ⇒ <ff, int-path/encode _ _>
+    ]
+  | negsuc m ⇒ λ y →
+    elim y [
+    | pos n ⇒ <ff, int-path/encode _ _>
+    | 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 → <tt, λ i → negsuc (l i)>)
+        (λ r → <ff, λ p → r (λ i → int-repr (p i))>)
+    ]
+  ]
+
+let int/set : IsSet int =
+  discrete/to/set int int/discrete
diff --git a/invariance.red → example/invariance.red b/invariance.red → example/invariance.red
diff --git a/isotoequiv.red → example/isotoequiv.red b/isotoequiv.red → example/isotoequiv.red
diff --git a/modal.red → example/modal.red b/modal.red → example/modal.red
diff --git a/example/nat.red b/example/nat.red
@@ -0,0 +1,101 @@
+import path
+import void
+import unit
+import hedberg
+
+data nat where
+| zero
+| suc (x : nat)
+
+let nat-pred (x : nat) : nat =
+  elim x [
+  | zero ⇒ zero
+  | suc n ⇒ n
+  ]
+
+
+let nat-pred/suc (x : nat) : Path nat x (nat-pred (suc x)) =
+  auto
+
+let plus : nat → nat → nat =
+  λ m n →
+    elim m [
+    | zero ⇒ n
+    | suc (m ⇒ plus/m/n) ⇒ suc plus/m/n
+    ]
+
+let plus/unit/l (n : nat) : Path nat (plus zero n) n =
+  auto
+
+let plus/unit/r (n : nat) : Path nat (plus n zero) n =
+  elim n [
+  | zero ⇒ auto
+  | suc (n ⇒ path/n) ⇒ λ i → suc (path/n i)
+  ]
+
+let plus/assoc (n : nat) : (m, o : nat) → Path nat (plus n (plus m o)) (plus (plus n m) o) =
+  elim n [
+  | zero ⇒ auto
+  | suc (n ⇒ plus/assoc/n) ⇒ λ m o i → suc (plus/assoc/n m o i)
+  ]
+
+let plus/suc/r (n : nat) : (m : nat) → Path nat (plus n (suc m)) (suc (plus n m)) =
+  elim n [
+  | zero ⇒ auto
+  | suc (n ⇒ plus/n/suc/r) ⇒ λ m i → suc (plus/n/suc/r m i)
+  ]
+
+
+let plus/comm (m : nat) : (n : nat) → Path nat (plus n m) (plus m n) =
+  elim m [
+  | zero ⇒ plus/unit/r
+  | 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,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 ⇒ <tt, λ _ → zero>
+    | suc n' ⇒ <ff, nat-path/encode zero (suc n')>
+    ]
+  | suc (m' ⇒ nat/discrete/m') ⇒ λ n →
+    elim n [
+    | zero ⇒ <ff, nat-path/encode (suc m') 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 → <tt, λ i → suc (l i)>)
+        (λ r → <ff, λ p → r (λ i → nat-pred (p i))>)
+    ]
+  ]
+
+let nat/set : IsSet nat =
+  discrete/to/set nat nat/discrete