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 54%
rename from connection.red
rename to example/connection.red
index 301e73c12..eb047e9a7 100644
--- a/connection.red
+++ b/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 b/example/equivalence.red
similarity index 71%
rename from equivalence.red
rename to example/equivalence.red
index 14a65f8b3..9ae5da4e6 100644
--- a/equivalence.red
+++ b/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
new file mode 100644
index 000000000..a1a38029d
--- /dev/null
+++ 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
new file mode 100644
index 000000000..16942e862
--- /dev/null
+++ 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 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/example/nat.red b/example/nat.red
new file mode 100644
index 000000000..d4ebad5fd
--- /dev/null
+++ 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
diff --git a/example/ntype.red b/example/ntype.red
new file mode 100644
index 000000000..3daec4032
--- /dev/null
+++ b/example/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/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/hedberg-wip.red b/example/or.red
similarity index 62%
rename from hedberg-wip.red
rename to example/or.red
index 222c3bd69..c285726fe 100644
--- a/hedberg-wip.red
+++ b/example/or.red
@@ -1,9 +1,5 @@
 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)
@@ -27,16 +23,4 @@ let or/elim
     (λ 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/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/example/unit.red b/example/unit.red
new file mode 100644
index 000000000..80f142755
--- /dev/null
+++ b/example/unit.red
@@ -0,0 +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/univalence.red b/example/univalence.red
similarity index 97%
rename from univalence.red
rename to example/univalence.red
index 73cf62b71..196856008 100644
--- a/univalence.red
+++ b/example/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
diff --git a/example/void.red b/example/void.red
new file mode 100644
index 000000000..797032ac6
--- /dev/null
+++ b/example/void.red
@@ -0,0 +1,9 @@
+import ntype
+
+data void where
+
+let neg (A : type) : type =
+  A → void
+
+let void/prop : IsProp void =
+  λ v → elim v []
diff --git a/int.red b/int.red
deleted file mode 100644
index 614d16817..000000000
--- a/int.red
+++ /dev/null
@@ -1,52 +0,0 @@
-import path
-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>>>
diff --git a/nat.red b/nat.red
deleted file mode 100644
index 7dc57998e..000000000
--- a/nat.red
+++ /dev/null
@@ -1,52 +0,0 @@
-import path
-
-
-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))
-  ]
-