diff --git a/examples/Bool.pi b/examples/Bool.pi
--- a/examples/Bool.pi
+++ b/examples/Bool.pi
@@ -13,3 +13,35 @@
 andb = \ b c -> case b of {
                   true -> c
                 | false -> 'false };
+
+orb : Bool -> Bool -> Bool;
+orb = \ b c -> case b of {
+                  true -> 'true
+                | false -> c };
+
+eqBool : Bool -> Bool -> Bool;
+eqBool = \ b1 b2 -> 
+   case b1 of
+    { true ->  case b2 of { true -> 'true | false -> 'false}                  
+    | false -> case b2 of { true -> 'false | false -> 'true}};                
+
+EqBool : Bool -> Bool -> Type;
+EqBool = \b1 b2 -> T(eqBool b1 b2);
+
+reflBool : (b : Bool) -> EqBool b b;
+reflBool = \ b -> case b of
+ { true -> 'unit
+   | false -> 'unit}; 
+
+substBool : (P : Bool -> Type) -> 
+	  (b1 b2 : Bool)
+	  -> (EqBool b1 b2)
+	  -> P b1 -> P b2;
+substBool = \ P b1 b2 m m1 ->
+   case b1 of
+     {true -> case b2 of
+          { true -> m1
+           | false -> case m of {}}
+     | false ->  case b2 of
+          { true ->  case m of {}
+           | false -> m1}};
diff --git a/examples/Broken.pi b/examples/Broken.pi
deleted file mode 100644
--- a/examples/Broken.pi
+++ /dev/null
@@ -1,9 +0,0 @@
-Bool : Type;
-Bool = { true false };
-
-broken : Bool -> Bool;
-broken = \ b -> case b of {
-                 true  -> 'true
-               | true  -> 'true
-               | false -> 'true };
-
diff --git a/examples/Conat.pi b/examples/Conat.pi
--- a/examples/Conat.pi
+++ b/examples/Conat.pi
@@ -1,70 +1,74 @@
 :l Empty.pi
 :l Unit.pi
 
-Nat' : Type;
-Nat' = (l : { z s }) * case l of {
+CoNat : Type;
+CoNat = (l : { z s }) * case l of {
                            z -> Unit
-			 | s -> [^ Nat'] };
+			 | s -> Rec [^ CoNat] };
 
 
-zero : Nat';
+zero : CoNat;
 zero = ('z,'unit);
 
-succ : ^Nat' -> Nat';
-succ = \ n -> ('s,n);
+succ : ^CoNat -> CoNat;
+succ = \ n -> ('s,fold n);
 
-one : Nat';
+one : CoNat;
 one = succ [zero];
 
-two : Nat';
+two : CoNat;
 two = succ [one];
 
-omega : Nat';
+omega : CoNat;
 omega = succ [omega];
 
 
-add : Nat' -> Nat' -> Nat';
+add : CoNat -> CoNat -> CoNat;
 add = \ m n -> split m with (lm , m') ->
                  case lm of {
 		     z -> n
- 		   | s -> succ [add (!m') n] };
+ 		   | s -> succ [add (! (unfold m')) n] };
 
-eq : Nat' -> Nat' -> Type;
-eq = \ m n -> split m with (lm , m') ->
+EqCoNat : CoNat -> CoNat -> Type;
+EqCoNat = \ m n -> split m with (lm , m') ->
               split n with (ln , n') ->
                    case lm of {
-		     z -> case ln of { 
+		     z -> case ln of {
 		             z -> Unit
 			   | s -> Empty }
-	           | s -> case ln of { 
+	           | s -> case ln of {
 		             z -> Empty
-			   | s -> [^ (eq (! m') (! n'))]}};
+			   | s -> Rec [^ (EqCoNat (! (unfold m')) (! (unfold n')))]}};
 
 
-refl : (n:Nat') -> eq n n;
-refl = \ n -> split n with (ln , n') ->
+reflCoNat : (n:CoNat) -> EqCoNat n n;
+reflCoNat = \ n -> split n with (ln , n') ->
        	          case ln of {
 		     z -> 'unit
-		   | s -> [refl (!n')] };
+		   | s -> fold [reflCoNat (! (unfold n'))] };
 
-sym : (m:Nat') -> (n:Nat') -> eq m n -> eq n m;
-sym = \ m n p -> 
+symCoNat : (m n:CoNat) -> EqCoNat m n -> EqCoNat n m;
+symCoNat = \ m n p ->
               split m with (lm , m') ->
               split n with (ln , n') ->
                    case lm of {
 		     z -> case ln of {
 		             z -> 'unit
 			   | s -> case p of {}}
-	           | s -> case ln of { 
+	           | s -> case ln of {
 		             z -> case p of {}
-			   | s -> [sym (! m') (! n') (! p)] }};
+			   | s -> fold [symCoNat (! (unfold m')) (! (unfold n')) (! (unfold p))] }};
 
+transCoNat : (l m n:CoNat) -> EqCoNat l m -> EqCoNat m n -> EqCoNat l n;
+--transCoNat = \ l m n p q ->
+	   
+
 {-
-subst : (P : Nat' -> Type) 
-      -> (m : Nat') -> (n : Nat')
-      -> (eq m n)
+subst : (P : CoNat -> Type)
+      -> (m : CoNat) -> (n : CoNat)
+      -> (EqCoNat m n)
       -> P m -> ^ (P n);
-subst = \ P m n q x -> 
+subst = \ P m n q x ->
               split m with (lm , m') ->
               split n with (ln , n') ->
                  case lm of {
@@ -73,9 +77,11 @@
 			             unit -> case n' of {
 				                unit -> [x] }}
 			   | s -> case q of {}}
-	           | s -> case ln of { 
+	           | s -> case ln of {
 		             z -> case q of {}
-			   | s -> [subst (\ i -> P (succ i)) (! m') (! n') (! q) x]}};
+			   | s -> [unfold m' as m' ->
+                                   unfold n' as n' ->
+                                   subst (\ i -> P (succ [i])) (! m') (! n') (! q) x]}};
 -}
 
 {- seems we need an eliminator for boxes, e.g. unbox
diff --git a/examples/Curry.pi b/examples/Curry.pi
--- a/examples/Curry.pi
+++ b/examples/Curry.pi
@@ -4,10 +4,10 @@
 -- Curry's paradox (usually ruled out by positivity check).
 
 A : Type;
-A = [A] → ⊥;
+A = Rec [A] → ⊥;
 
 ¬A : A → ⊥;
-¬A = λ x → x x;
+¬A = λ x → x (fold x);
 
 contradiction : ⊥;
-contradiction = ¬A (λ x → ¬A x);
+contradiction = ¬A (λ x → ¬A (unfold x));
diff --git a/examples/Equal.pi b/examples/Equal.pi
--- a/examples/Equal.pi
+++ b/examples/Equal.pi
@@ -81,7 +81,7 @@
 {- works, uses bet equality in contexts. -}
 
 t11a : Eq (^(^A)) [let x:A=a in [x]] [let y:A=a in [y]]
-    = refl (^(^A)) [let x:A=a in [x]]; 
+    = refl (^(^A)) [let x:A=a in [x]];
 {- works now -}
 
 t12 : Eq (^A) (let y:A=y in [y]) (let z:A=z in [z])
@@ -94,21 +94,21 @@
 -}
 
 Stream : Type;
-Stream = A * [∞ Stream];
+Stream = A * Rec [∞ Stream];
 
-as : Stream;
-as = (a, [as]);
+as' : Stream;
+as' = (a, fold [as']);
 
 repeat : (x : A) → Stream;
-repeat = λ x → (x, [repeat x]);
+repeat = λ x → (x, fold [repeat x]);
 
--- as is equal to its unfolding.
+-- as' is equal to its unfolding.
 
-unfolds : Eq Stream as (a, [as]);
-unfolds = refl Stream as;
+unfolds : Eq Stream as' (a, fold [as']);
+unfolds = refl Stream as';
 
 -- repeat a is not equal to its unfolding.
 {-
-doesNotUnfold : Eq Stream (repeat a) (a, [repeat a]);
+doesNotUnfold : Eq Stream (repeat a) (a, fold [repeat a]);
 doesNotUnfold = refl Stream (repeat a);
 -}
diff --git a/examples/Fin.pi b/examples/Fin.pi
--- a/examples/Fin.pi
+++ b/examples/Fin.pi
@@ -6,7 +6,7 @@
 		     z -> [Empty]
 		   | s -> [(l : { z s }) * case l of {
                                              z -> Unit
-			                   | s -> Fin n'}]};
+			                   | s -> Fin (unfold n')}]};
 
 fz : (n:Nat) -> Fin (succ n);
 fz = \ n -> ('z , 'unit );
@@ -18,7 +18,7 @@
 fmax = \ n -> split n with (ln , n') ->
                  ! case ln of {
 		     z -> [fz zero]
-		   | s -> [fs n (fmax n')] };
+		   | s -> [fs n (fmax (unfold n'))] };
 
 femb : (n:Nat) -> Fin n -> Fin (succ n);
 femb = \ n i -> split n with (ln , n') ->
@@ -27,7 +27,7 @@
 		   | s -> split i with (li , i') ->
 		       	     case li of {
  			       z -> [fz n]
-		             | s -> [fs n (femb n' i')] }};
+		             | s -> [fs n (femb (unfold n') i')] }};
 
 finv : (n:Nat) -> Fin n -> Fin n;
 finv = \ n i -> split n with (ln , n') ->
@@ -35,6 +35,7 @@
 		     z -> case i of {}
 		   | s -> split i with (li , i') ->
 		       	     case li of {
- 			       z -> [fmax n']
-			     | s -> [fs n' (finv n' i')] }};
+ 			       z -> [fmax (unfold n')]
+			     | s -> [unfold n' as n' ->
+                                     fs n' (finv n' i')] }};
 
diff --git a/examples/Foo.pi b/examples/Foo.pi
deleted file mode 100644
--- a/examples/Foo.pi
+++ /dev/null
@@ -1,1 +0,0 @@
-Nat
diff --git a/examples/Id.pi b/examples/Id.pi
new file mode 100644
--- /dev/null
+++ b/examples/Id.pi
@@ -0,0 +1,12 @@
+Id : (A:Type) -> A -> A -> Type;
+refl : (A:Type) -> (a:A) -> Id A a a;
+
+J : (A:Type) -> (P:(a:A) -> (b:A) -> Id A a b -> Type) 
+  -> ((a:A) -> P a a (refl A a))
+  -> (a:A) -> (b:A) -> (p : Id A a b) -> P a b p;
+
+forceEq : (A:Type) -> (a : ^A) -> Id (^A) a [!a];
+{-
+forceEq = \ A a -> unbox a with [x] -> refl (^A) [x]
+should not typecheck!
+-}
diff --git a/examples/Nat.pi b/examples/Nat.pi
--- a/examples/Nat.pi
+++ b/examples/Nat.pi
@@ -3,13 +3,13 @@
 Nat : Type;
 Nat = (l : { z s }) * case l of {
                            z -> Unit
-			 | s -> [Nat] };
+			 | s -> Rec [Nat] };
 
 zero : Nat;
 zero = ('z,'unit);
 
 succ : Nat -> Nat;
-succ = \ n -> ('s,n);
+succ = \ n -> ('s,fold n);
 
 one : Nat;
 one = succ zero;
@@ -21,34 +21,34 @@
 add = \ m n -> split m with (lm , m') ->
                  ! case lm of {
 		     z -> [n]
- 		   | s -> [succ (add m' n)] };
+ 		   | s -> [succ (add (unfold m') n)] };
 
 
-eqbNat : Nat -> Nat -> Bool;
-eqbNat = \ m n -> split m with (lm , m') ->
+eqNat : Nat -> Nat -> Bool;
+eqNat = \ m n -> split m with (lm , m') ->
                   split n with (ln , n') ->
                   ! case lm of {
-		     z -> case ln of { 
+		     z -> case ln of {
 		             z -> ['true]
 			   | s -> ['false] }
 	           | s -> case ln of {
 		             z -> ['false]
-			   | s -> [eqbNat m' n'] } };
+			   | s -> [eqNat (unfold m') (unfold n')] } };
 
-eqNat : Nat -> Nat -> Type;
-eqNat = \ m n -> T (eqbNat m n);
+EqNat : Nat -> Nat -> Type;
+EqNat = \ m n -> T (eqNat m n);
 
-reflNat : (n:Nat) -> eqNat n n;
+reflNat : (n:Nat) -> EqNat n n;
 reflNat = \ n -> split n with (ln , n') ->
        	        ! case ln of {
 		     z -> ['unit]
-		   | s -> [reflNat n'] };
+		   | s -> [reflNat (unfold n')] };
 
-substNat : (P : Nat -> Type) 
+substNat : (P : Nat -> Type)
       -> (m : Nat) -> (n : Nat)
-      -> (eqNat m n)
+      -> (EqNat m n)
       -> P m -> P n;
-substNat = \ P m n q x -> 
+substNat = \ P m n q x ->
               split m with (lm , m') ->
               split n with (ln , n') ->
                  ! case lm of {
@@ -57,38 +57,41 @@
 			             unit -> case n' of {
 				                unit -> [x]}}
 			   | s -> case q of {}}
-	           | s -> case ln of { 
+	           | s -> case ln of {
 		             z -> case q of {}
-			   | s -> [substNat (\ i -> P (succ i)) m' n' q x]}};
+			   | s -> [unfold m' as m' ->
+                                   unfold n' as n' ->
+                                   substNat (\ i -> P (succ i)) m' n' q x]}};
 
 
-symNat : (m:Nat) -> (n:Nat) -> eqNat m n -> eqNat n m;
-symNat = \ m n p -> substNat (\ i -> eqNat i m) m n p (reflNat m);
+symNat : (m:Nat) -> (n:Nat) -> EqNat m n -> EqNat n m;
+symNat = \ m n p -> substNat (\ i -> EqNat i m) m n p (reflNat m);
 
 transNat : (i:Nat) -> (j:Nat) -> (k:Nat) ->
-      eqNat i j -> eqNat j k -> eqNat i k;
-transNat = \ i j k p q -> substNat (\ x -> eqNat i x) j k q p;
+      EqNat i j -> EqNat j k -> EqNat i k;
+transNat = \ i j k p q -> substNat (\ x -> EqNat i x) j k q p;
 
-addCom0 : (n:Nat) -> eqNat n (add n zero);
+addCom0 : (n:Nat) -> EqNat n (add n zero);
 addCom0 = \ n -> split n with (ln , n') ->
-	         ! case ln of { 
+	         ! case ln of {
 		      z -> case n' of {
 		              unit -> [reflNat zero]}
-	            | s -> [addCom0 n'] };
+	            | s -> [addCom0 (unfold n')] };
 
 addComS : (m:Nat) -> (n:Nat) ->
-	  (eqNat  (add (succ m) n) (add m (succ n)));
+	  (EqNat  (add (succ m) n) (add m (succ n)));
 addComS = \ m n -> split m with (lm , m') ->
 	           ! case lm of {
 		       z -> [reflNat (succ n)]
-		     | s -> [addComS m' n] };
+		     | s -> [addComS (unfold m') n] };
 
 addCom : (m:Nat) -> (n:Nat) ->
-	  (eqNat (add m n) (add n m));
+	  (EqNat (add m n) (add n m));
 addCom = \ m n ->  split m with (lm , m') ->
 	           ! case lm of {
 		       z ->  case m' of {
 		                unit -> [addCom0 n] }
-		     | s -> [transNat (add (succ m') n) (add (succ n) m') (add n (succ m'))
+		     | s -> [unfold m' as m' ->
+                             transNat (add (succ m') n) (add (succ n) m') (add n (succ m'))
 		                      (addCom m' n) (addComS n m')] };
 
diff --git a/examples/Parser.pi b/examples/Parser.pi
--- a/examples/Parser.pi
+++ b/examples/Parser.pi
@@ -1,89 +1,41 @@
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
-Nat : type;
+:l Bool.pi
+
+andb' : Bool -> Bool -> Bool;
+andb' = \ b c -> case c of {
+                  true -> b
+                | false -> 'false };
+
+inftyOpt : Type -> Bool -> Type
+   = \ A b -> case b of {
+                 true -> A
+               | false -> ^ A };
+
+boxOpt : (b:Bool) -> (A:Type) -> A -> inftyOpt A b
+       = \ b A a -> case b of { true -> a
+		              | false -> [a] };
+
+forceOpt : (b:Bool) -> (A:Type) -> inftyOpt A b -> A 
+       = \ b A a -> case b of { true -> a
+		              | false -> !a };
+
+Tok : Type;
+
+P : Bool -> Type
+  = \ b -> (l : { fail empty sat alt seq } ) *
+           case l of {
+             fail -> EqBool 'false b
+           | empty -> EqBool 'true b
+           | sat -> (Tok -> Bool) * (EqBool 'false b)
+           | alt -> (n1 n2 : Bool) * Rec [P n1] * Rec [P n2] * (EqBool (orb n1 n2) b)
+           | seq -> (n1 n2 : Bool) * inftyOpt (Rec [P n1]) n2 *
+                                     inftyOpt (Rec [P n2]) n1 * (EqBool (andb' n1 n2) b) };
+
+
+star : P 'false -> P 'true;
+plus : P 'false -> P 'false;
+
+star = \ p -> ('alt , ('true, ('false, (fold ('empty, reflBool 'true),
+                                       (fold (plus p),
+                                       reflBool 'false)))));
+
+plus = \ p -> ('seq, ('false, ('true, (fold p, ([fold (star p)], reflBool 'false)) )) );
diff --git a/examples/Parser2.pi b/examples/Parser2.pi
deleted file mode 100644
--- a/examples/Parser2.pi
+++ /dev/null
@@ -1,331 +0,0 @@
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
-Nat;
diff --git a/examples/Parser3.pi b/examples/Parser3.pi
deleted file mode 100644
--- a/examples/Parser3.pi
+++ /dev/null
@@ -1,331 +0,0 @@
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
-Nat
diff --git a/examples/Streams.pi b/examples/Streams.pi
--- a/examples/Streams.pi
+++ b/examples/Streams.pi
@@ -16,13 +16,13 @@
 Nat : Type;
 Nat = (l : { z s }) * case l of {
                            z -> Unit
-			 | s -> [Nat] };
+			 | s -> Rec [Nat] };
 
 zero : Nat;
 zero = ('z,'unit);
 
 succ : Nat -> Nat;
-succ = \ n -> ('s,n);
+succ = \ n -> ('s, fold n);
 
 one : Nat;
 one = succ zero;
@@ -34,18 +34,18 @@
 add = \ m n -> split m with (lm , m') ->
                  ! case lm of {
 		     z -> [n]
- 		   | s -> [succ (add m' n)] };
+ 		   | s -> [succ (add (unfold m') n)] };
 
 eqbNat : Nat -> Nat -> Bool;
 eqbNat = \ m n -> split m with (lm , m') ->
                   split n with (ln , n') ->
                   ! case lm of {
-		     z -> case ln of { 
+		     z -> case ln of {
 		             z -> ['true]
 			   | s -> ['false] }
 	           | s -> case ln of {
 		             z -> ['false]
-			   | s -> [eqbNat m' n'] } };
+			   | s -> [eqbNat (unfold m') (unfold n')] } };
 
 eqNat : Nat -> Nat -> Type;
 eqNat = \ m n -> T (eqbNat m n);
@@ -54,38 +54,39 @@
 reflNat = \ n -> split n with (ln , n') ->
        	        ! case ln of {
 		     z -> ['unit]
-		   | s -> [reflNat n'] };
+		   | s -> [reflNat (unfold n')] };
 
 
 Stream : Type -> Type;
-Stream = \ a -> a * [^ (Stream a)];
+Stream = \ a -> a * Rec [^ (Stream a)];
 
 put : (a : Type) -> a -> Stream a -> Stream a;
-put = \ a x xs -> (x,[xs]);
+put = \ a x xs -> (x, fold [xs]);
 
 from : Nat -> Stream Nat;
-from = \ n -> (n, [from (succ n)]);
+from = \ n -> (n, fold [from (succ n)]);
 
 tail : (a:Type) -> Stream a -> Stream a;
-tail = \ a xs -> split xs with (x , xs') -> ! xs';
+tail = \ a xs -> split xs with (x , xs') -> ! (unfold xs');
 
 head : (a:Type) -> Stream a -> a;
 head = \ a xs -> split xs with (x , xs') -> x;
 
 map : (a : Type) -> (b : Type) -> (a -> b) -> Stream a -> Stream b;
-map = \ a b f xs -> split xs with (x , xs') -> (f x, [map a b f (! xs')]);
+map = \ a b f xs -> split xs with (x , xs') -> (f x, fold [map a b f (! (unfold xs'))]);
 
 eqStream : (a : Type) -> (a -> a -> Type) -> Stream a -> Stream a -> Type;
-eqStream = \ a eq xs ys -> split xs with (x , xs') ->
-	                   split ys with (y , ys') ->
-			   	 (eq x y) * [^ (eqStream a eq (! xs') (! ys'))];
+eqStream = \ a eq xs ys ->
+  split xs with (x , xs') ->
+  split ys with (y , ys') ->
+    eq x y * Rec [^ (eqStream a eq (! (unfold xs')) (! (unfold ys')))];
 
-reflStream :  (a : Type) -> (eq : a -> a -> Type) 
+reflStream :  (a : Type) -> (eq : a -> a -> Type)
 	   -> ((x : a) -> eq x x)
 	   -> (xs : Stream a) -> eqStream a eq xs xs;
-reflStream = \ a eq refl xs -> split xs with (x , xs') -> 
-	       	    	         ((refl x), [reflStream a eq refl (! xs')]);
+reflStream = \ a eq refl xs -> split xs with (x , xs') ->
+	       	    	         (refl x, fold [reflStream a eq refl (! (unfold xs'))]);
 
-lemma : (n : Nat) -> eqStream Nat eqNat (from (succ n)) 
+lemma : (n : Nat) -> eqStream Nat eqNat (from (succ n))
                                         (map Nat Nat succ (from n));
-lemma = \ n -> ((reflNat (succ n)),[lemma (succ n)]);  
+lemma = \ n -> ((reflNat (succ n)), fold [lemma (succ n)]);
diff --git a/examples/SubjectReduction.pi b/examples/SubjectReduction.pi
deleted file mode 100644
--- a/examples/SubjectReduction.pi
+++ /dev/null
@@ -1,58 +0,0 @@
--- Context:
---   Recursion with boxes
---   Thorsten Altenkirch
---   http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=104
-
-Stream : Type;
-Stream = [∞ Stream];
-
-ticks : Stream;
-ticks = [ticks];
-
-Eq : (A : Type) → A → A → Type;
-Eq = λ A x y → (P : A → Type) → P x → P y;
-
-refl : (A : Type) → (x : A) → Eq A x x;
-refl = λ A x P px → px;
-
-unfold : Eq Stream ticks [ticks];
-unfold = refl Stream ticks;
-
--- We can prove this variant of congruence for boxes:
-
-cong : (xs ys : Stream) → Eq Stream xs ys →
-       Eq Stream [let zs : Stream = xs in zs]
-                 [let zs : Stream = ys in zs];
-cong = λ xs ys eq P p → eq (λ zs → P [let us : Stream = zs in us]) p;
-
--- This does not (obviously) break subject reduction, because the
--- following property can be proved using refl:
-
-unfoldInContext : Eq Stream [let xs : Stream =  ticks  in xs]
-                            [let xs : Stream = [ticks] in xs];
-unfoldInContext = cong ticks [ticks] unfold;
-unfoldInContext = refl Stream [let xs : Stream = ticks in xs];
-
--- Note also that unlimited unfolding is not possible (using refl):
-
--- unfoldTwiceInContext : Eq Stream [let xs : Stream =   ticks   in xs]
---                                  [let xs : Stream = [[ticks]] in xs];
--- unfoldTwiceInContext = refl Stream [let xs : Stream = ticks in xs];
-
--- However, we can move lets through boxes, so the idea from
--- Thorsten's blog post needs to be qualified.
-
-letThroughBox : (xs : Stream) →
-                Eq Stream [let ys : Stream = xs in  ys]
-                          (let ys : Stream = xs in [ys]);
-letThroughBox = λ xs → refl Stream [let ys : Stream = xs in ys];
-
-letThrough2Boxes : (xs : Stream) →
-                   Eq Stream [[let ys : Stream = xs in  ys]]
-                             (let ys : Stream = xs in [[ys]]);
-letThrough2Boxes = λ xs → refl Stream [[let ys : Stream = xs in ys]];
-
-anotherExample : (A : Type) → (x : A) →
-                 Eq (∞ (∞ A)) [let y : A = x in [y]]
-                              (let y : A = x in [[let z : A = y in z]]);
-anotherExample = λ A x → refl (∞ (∞ A)) (let y : A = x in [[y]]);
diff --git a/examples/Universe.pi b/examples/Universe.pi
new file mode 100644
--- /dev/null
+++ b/examples/Universe.pi
@@ -0,0 +1,34 @@
+:l Nat.pi
+:l Fin.pi
+:l Bool.pi
+
+U   :  Type;  
+El  :  U -> Type;
+
+U = (l : {enum sigma rec}) * 
+     case l of  { enum   -> Nat
+                | sigma  -> Rec [(a : U) * (El a ->  U)]
+                | rec    -> ^ (Rec [U]) };
+
+El =  \ a ->  split a with (a_l,a_r) -> 
+     ! case a_l of
+       {  enum   ->  [Fin a_r]
+       |  sigma  ->  [unfold a_r as a_r' -> 
+                      split a_r' with (b,c) -> 
+                      (x : El b) * (El (c x))]
+       |  rec    ->  [unfold (! a_r) as a_r' -> 
+                     Rec [El a_r']]};
+
+nat : U =  ('sigma, fold (('enum, succ (succ zero)),
+           (\ i -> split i with (i_l,i_r) ->   
+                    !  case i_l of  
+		       {  z  ->  [('enum, succ zero)]
+                       |  s  ->  [('rec, [fold nat])]})));
+
+eq : (a : U) -> El a -> El a -> Bool;
+
+refl : (a : U) → (x : El a) → T (eq a x x);
+
+subst : (a : U) → (x y : El a) → T (eq a x y) 
+      → (P : El a → Type) → P x → P y;
+
diff --git a/examples/Vec.pi b/examples/Vec.pi
--- a/examples/Vec.pi
+++ b/examples/Vec.pi
@@ -4,7 +4,7 @@
 Vec = \ m a -> split m with (lm , m') ->
                  ! case lm of {
 		     z -> [Unit]
-		   | s -> [a * Vec m' a] }; 
+		   | s -> [a * Vec (unfold m') a] };
 
 vnil : (a : Type) -> Vec zero a;
 vnil = \ a -> 'unit;
@@ -20,4 +20,4 @@
 		             split i with (li , i') ->
 		               case li of {
 		 	         z -> [x]
-		               | s -> [nth a n' xs' i']}}
+		               | s -> [nth a (unfold n') xs' i']}}
diff --git a/examples/stl.pi b/examples/stl.pi
--- a/examples/stl.pi
+++ b/examples/stl.pi
@@ -7,7 +7,7 @@
 
 pair : (a:Bool) -> (b:Bool) -> ((T a) * (T b)) -> T (andb a b);
 pair = \ a b xy ->
-       split xy with (x,y) -> 
+       split xy with (x,y) ->
        case a of {
          true -> y
        | false -> case x of {}};
@@ -21,27 +21,29 @@
        | false -> case x of {}};
 
 Ty : Type;
-Ty = (l : {base arr}) * 
+Ty = (l : {base arr}) *
      case l of {
        base -> Unit
-     | arr -> [Ty * Ty] };
+     | arr -> Rec [Ty * Ty] };
 
 base : Ty;
 base = ('base, 'unit);
 
 arr : Ty -> Ty -> Ty;
-arr = \ a b -> ('arr,(a,b));
+arr = \ a b -> ('arr,fold (a,b));
 
 eqb : Ty -> Ty -> Bool;
 eqb = \ a b -> split a with (la, a') ->
                split b with (lb, b') ->
 	       ! case la of {
-	           base -> case lb of { 
+	           base -> case lb of {
 		   	     base -> ['true]
  			   | arr -> ['false]}
 		 | arr -> case lb of {
 		       	     base -> ['false]
-			   | arr -> split a' with (a0, a1) ->
+			   | arr -> unfold a' as a' ->
+                                    unfold b' as b' ->
+                                    split a' with (a0, a1) ->
 			            split b' with (b0, b1) ->
 				      [andb (eqb a0 b0) (eqb a1 b1)]}};
 
@@ -52,14 +54,15 @@
 refl = \ a -> split a with (la, a') ->
               ! case la of {
 	           base -> ['unit]
-		 | arr -> split a' with (b,c) ->
+		 | arr -> unfold a' as a' ->
+                          split a' with (b,c) ->
 		       	    [pair (eqb b b) (eqb c c) ((refl b) , (refl c))] };
 
-subst : (P : Ty -> Type) 
+subst : (P : Ty -> Type)
       -> (a : Ty) -> (b : Ty)
       -> (eq a b)
       -> P a -> P b;
-subst = \ P a b p x -> 
+subst = \ P a b p x ->
       	       split a with (la, a') ->
                split b with (lb, b') ->
 	       ! case la of {
@@ -70,32 +73,35 @@
 			    | arr -> case p of {}}
                  | arr -> case lb of {
 		       	     base -> case p of {}
-			   | arr -> split a' with (a0 , a1) ->
+			   | arr -> unfold a' as a' ->
+                                    unfold b' as b' ->
+                                    split a' with (a0 , a1) ->
 			            split b' with (b0 , b1) ->
 				    split (unpair (eqb a0 b0) (eqb a1 b1) p) with (p0, p1) ->
 				      [subst (\ z -> P (arr b0 z)) a1 b1 p1
 				             (subst (\ y -> P (arr y a1)) a0 b0 p0 x)]}};
-				    
-{- subst succesfully uses split on a non-variable! -}
 
+{- subst successfully uses split on a non-variable! -}
+
 Con : Type;
-Con = ( l : {empty ext} ) * 
+Con = ( l : {empty ext} ) *
       case l of {
         empty -> Unit
-      | ext -> [Con * Ty] };
+      | ext -> Rec [Con * Ty] };
 
 empty : Con;
 empty = ('empty,'unit);
 
 ext : Con -> Ty -> Con;
-ext = \ g a -> ('ext,(g,a));
+ext = \ g a -> ('ext, fold (g,a));
 
 Var : Con -> Ty -> Type;
-Var = \ g a -> 
-      split g with (lg, g') -> 
+Var = \ g a ->
+      split g with (lg, g') ->
       case lg of {
         empty -> Empty
-      | ext -> split g' with (d, a') ->
+      | ext -> unfold g' as g' ->
+               split g' with (d, a') ->
                   (l : {vz vs}) *
 		  ! case l of {
 		      vz -> [eq a a']
@@ -103,34 +109,35 @@
 
 vz : (g:Con) -> (a:Ty) -> Var (ext g a) a;
 vz = \ g a -> ('vz, (refl a));
-	
+
 vs : (g:Con) -> (a:Ty) -> (b:Ty) -> Var g a -> Var (ext g b) a;
 vs = \ g a b x -> ('vs,x);
 
 Lam : Con -> Ty -> Type;
-Lam = \ g a -> 
+Lam = \ g a ->
       (l : {var app lam}) *
       case l of {
          var -> Var g a
-       | app -> [(b : Ty) * ((Lam g (arr b a)) * (Lam g b))]
+       | app -> Rec [(b : Ty) * (Lam g (arr b a) * Lam g b)]
        | lam -> split a with (la, a') ->
        	     	case la of {
 		  base -> Empty
-		| arr -> split a' with (b, c) ->
-		           [Lam (ext g b) c] }};
-		  
+		| arr -> unfold a' as a' ->
+                         split a' with (b, c) ->
+		           Rec [Lam (ext g b) c] }};
+
 var : (g:Con) -> (a:Ty) -> Var g a -> Lam g a;
 var = \ g a x -> ('var,x);
 
 app : (g:Con) -> (a:Ty) -> (b:Ty)
       -> Lam g (arr a b) -> Lam g a -> Lam g b;
-app = \ g a b t u -> ('app,(a,(t,u)));
+app = \ g a b t u -> ('app, fold (a,(t,u)));
 
 lam : (g:Con) -> (a:Ty) -> (b:Ty)
       -> Lam (ext g a) b -> Lam g (arr a b);
-lam = \ g a b t -> ('lam,t);
+lam = \ g a b t -> ('lam, fold t);
 
-{- 
+{-
 
 Ren : Con -> Con -> Type
 Subst : Con -> Con -> Type
diff --git a/pisigma.cabal b/pisigma.cabal
--- a/pisigma.cabal
+++ b/pisigma.cabal
@@ -1,6 +1,6 @@
 cabal-version: >= 1.6
 name:          pisigma
-version:       0.1.0.3
+version:       0.2
 license:       BSD3
 license-file:  LICENSE
 data-files:    examples/*.pi
@@ -12,13 +12,24 @@
                Darin Morrison <dwm@cs.nott.ac.uk>
 maintainer:    Thorsten Altenkirch <txa@cs.nott.ac.uk>,
                Andres Loeh <kspisigma@andres-loeh.de>
-description:   dependently typed core language
-synopsis:      dependently typed core language
+synopsis:      A dependently typed core language
+description:   
+  PiSigma is a small dependently typed language with only very few
+  constructs: Type:Type, Pi-types, Sigma-types, enumerations and a
+  general meachanism for mutual recursion for types and values
+  controlled by lifted types. It is intended as a core language for
+  dependently typed languages like Agda. It has been described in the
+  paper <em>PiSigma: Dependent Types Without the Sugar</em> which has
+  appeared in the proceedings of FLOPS 2010.
 category:      Development, Language, Dependent Types
 build-type:    Simple
 
+flag debug
+  description:      Enable debug support
+  default:          False
+
 library
-  build-depends:    array           >= 0.2   && < 0.3,
+  build-depends:    array           >= 0.2   && < 0.4,
                     base            >= 4.0   && < 5.0,
                     bytestring      >= 0.9   && < 1.0,
                     haskeline       >= 0.6   && < 0.7,
@@ -27,7 +38,8 @@
                     mtl             >= 1.1   && < 1.2,
                     parsec          >= 3.0   && < 4.0,
                     text            >= 0.5   && < 0.6,
-                    utf8-string     >= 0.3.5 && < 0.4
+                    utf8-string     >= 0.3.5 && < 0.4,
+                    containers      >= 0.2   && < 0.4
 
   exposed-modules:  Language.PiSigma.Check
                     Language.PiSigma.Equality
@@ -40,14 +52,21 @@
                     Language.PiSigma.Util.String.Internal
                     Language.PiSigma.Util.String.Parser
 
-  ghc-options:      -funbox-strict-fields
+  if flag(debug)
+    ghc-options:    -Wall --enable-library-profiling -auto -funbox-strict-fields
+  else
+    ghc-options:    -funbox-strict-fields
 
   hs-source-dirs:   src
 
 
 
 executable pisigma
-  ghc-options:      -funbox-strict-fields
+
+  if flag(debug)
+    ghc-options:    -Wall --enable-library-profiling -auto -funbox-strict-fields
+  else
+    ghc-options:    -funbox-strict-fields
 
   hs-source-dirs:   src
 
diff --git a/src/Language/PiSigma/Check.hs b/src/Language/PiSigma/Check.hs
--- a/src/Language/PiSigma/Check.hs
+++ b/src/Language/PiSigma/Check.hs
@@ -8,26 +8,22 @@
 import Control.Arrow
   ( first )
 import Control.Monad.Error
-import qualified Data.List
-  as List
+import qualified Data.List as List
 
 import Language.PiSigma.Equality
 import Language.PiSigma.Evaluate
 import Language.PiSigma.Pretty
 import Language.PiSigma.Syntax
-import qualified Language.PiSigma.Util.String.Internal
-  as Internal
+import qualified Language.PiSigma.Util.String.Internal as Internal
+import qualified Data.Set as Set
 
---import Debug.Trace
---trace "check\n" $
+-- import Debug.Trace
+-- trace "check\n" $
 
 -- closures are the other way around
 -- should be fixed by changing closures.
 
-{-
-fog :: CTerm -> Closure
-fog (g,t) = (con2scope g,t)
--}
+-- * Error handling
 
 throwErrorc :: (Print b, GetLoc b, Env e) => b -> Pretty -> Eval e a
 throwErrorc t m =
@@ -60,12 +56,49 @@
 
 duplicateLabels :: (GetLoc a, Print a, Env e) => a -> Eval e d
 duplicateLabels t =
-  throwErrorc t $ "Duplicate labels in enum type"
+  throwErrorc t "Duplicate labels in enum type"
 
 nonLinearSplit :: (GetLoc a, Print a, Env e) => a -> Eval e d
 nonLinearSplit t =
-  throwErrorc t $ "Repeated variables in a split"
+  throwErrorc t "Repeated variables in a split"
 
+declaredButNotDefined :: Set.Set Name -> Eval e Scope
+declaredButNotDefined xs = throwError "Variables declared but not defined"
+
+declaredTwice :: Name -> Eval e Scope
+declaredTwice x = throwError "Variable declared twice in the same block."
+
+notDeclHere :: Name -> Eval e Scope
+notDeclHere x = throwError "Name not declared in the same context"
+
+-- * Checking
+
+checkProg :: Env e => Clos Prog -> Eval e Scope
+checkProg st = checkProg' Set.empty Set.empty st
+
+-- to be finished
+checkProg' :: Env e => Set.Set Name -> Set.Set Name -> Clos Prog -> Eval e Scope
+checkProg' decls defns ([],g) = return g
+--    do
+--      let declndef = decls `Set.difference` defns
+--      if not (Set.null declndef)
+--       then declaredButNotDefined declndef
+--       else return g
+checkProg' decls defns ((Decl _ x a):tel,g) =
+    do check (a,g) ty
+       (_,g') <- decl x PrtInfo{ name = x, expand = False } g (Just (a,g))
+       if x `Set.member` decls
+        then declaredTwice x
+        else checkProg' (Set.insert x decls) defns (tel,g')
+checkProg' decls defns ((Defn l x t):tel,g) =
+    do a <- inferVar l (x,g)
+       check (t,g) a
+       i <- getId l x g
+       defn' i (t,g)
+       if not (x `Set.member` decls) 
+        then notDeclHere x
+        else checkProg' decls (Set.insert x defns) (tel,g)
+
 -- | Takes a term and an (unevaluated) type. We first
 -- handle the cases that may potentially change the
 -- environment. If none of those cases match, we can
@@ -73,7 +106,7 @@
 check :: Env e => Clos Term -> Clos Type -> Eval e ()
 --check (g,t) c | trace ("check\ng ="++(show g)++"\n t="++(show t)++"\nc="++(show c)++"\n") False = undefined
 
-check (Let _ p t,g) c = 
+check (Let _ p t,g) c =
     do g' <- checkProg (p,g)
        check (t,g') c
 
@@ -81,9 +114,9 @@
 check (Split _ t (x,(y,u)),g) c | otherwise =
     do sigab <- infer' (t,g)
        case sigab of
-         (VQ Sigma ((a,(z,b)),s)) -> 
+         (VQ Sigma ((a,(z,b)),s)) ->
              do t'      <- eval (t,g)
-                (_,g')  <- tdecl x g (a,s) 
+                (_,g')  <- tdecl x g (a,s)
                 b'      <- subst (z,(b,s)) (Var Unknown x, g')
                 (_,g'') <- tdecl y g' b'
                 case t' of
@@ -98,10 +131,26 @@
                   msg1 = "sigma type" :: Internal.String
                   msg2 = "split"      :: Internal.String
 
-check gt @ (Case _ t lus,g) c = 
+check (Unfold _ t (x,u),g) c =
+    do rec <- infer' (t,g)
+       case rec of
+         VRec (a,s) ->
+             do t'      <- eval (t,g)
+                (_,g')  <- tdecl x g (Force Unknown a,s)
+                case t' of
+                  (Ne (NVar i)) ->
+                      letn' i (Fold Unknown (Var Unknown x), g')
+                            (check (u,g') c)
+                  _ -> check (u,g') c
+         _ -> expectedButFound (t,g) msg1 rec msg2
+                where
+                  msg1 = "rec type" :: Internal.String
+                  msg2 = "unfold"   :: Internal.String
+
+check gt @ (Case _ t lus,g) c =
     do enum <- infer' (t,g)
        case enum of
-         VEnum ls -> 
+         VEnum ls ->
              let ls' = map fst lus
              in if ls /= ls'
                 then -- pt' <- evalPrint t'
@@ -117,7 +166,7 @@
                           -- if the scrutinee is a variable, we add a constraint
                           -- while checking each of the branches
                           (Ne (NVar i)) ->
-                               mapM_ (\ (l,u) -> 
+                               mapM_ (\ (l,u) ->
                                       letn' i (label l)
                                             (check (u,g) c)) lus
                           -- if the scrutinee is not a variable, we do not add
@@ -127,20 +176,17 @@
                 where
                   msg1 = "enum type" :: Internal.String
                   msg2 = "case"      :: Internal.String
-                  
 
-         {- Problem: here and other places: we try to print the term t which isn't yet 
+
+         {- Problem: here and other places: we try to print the term t which isn't yet
             typechecked and may contain undefined variables which may crash the printer...
             see undef-bug.pi
          -}
-check (Force _ t,g) (a , s) =
-    check (t,g) (Lift Unknown a , s)
+check (Force _ t,g) c = check (t,g) (tlift c)
 
-check t a = check' t =<< feval a
+check t a = check' t =<< eval a
 
 check' :: Env e => Clos Term -> Val -> Eval e ()
--- we ignore boxes in types, this is the other part of the lifting story.
-check' gt (VBox (Boxed a)) = check gt a  
 check' (Lam _ (x,t),g) (VQ Pi ((a,(y,b)),s)) =
     do (i,g') <- tdecl x g (a,s)
        let s' = extendScope s y (i,Nothing)
@@ -158,51 +204,39 @@
 check' (Label _ l,_) (VEnum ls) | l `elem` ls = return ()
 check' gt @ (Label _ _,_) a =
     expected gt a "Label"
--- To check that [sigma] is a type, it's sufficient to know
--- that sigma is a type. The alternative would seem to be to
--- assume that ^Type == Type, but that does not work.
-check' (Box _ a,g) VType = 
-    check (a,g) ty
 check' (Box _ t,g) (VLift a) =
     check (t,g) a
-check' gt @ (Box _ _,_) a =
-    expected gt a "Box"
+check' (Fold _ t,g) (VRec a) =
+    check' (t,g) =<< eval (tforce a)
+
 check' t a =
     do b <- infer' t
-       catchE (eq a b) $ const $ expectedButFound t a b "check"
+       catchE (eq a b) $ \ s -> expectedButFound t a b "Check"
+-- line below leads to a runtime error 
+--       catchE (eq a b) $ \ s -> expectedButFound t a b (Internal.append "Check" s)
 
-inferVar :: Env e => Loc -> Clos Name -> Eval e (Clos Type)
-inferVar l (x,g) =
-    case lookupCon g x of
-      Just a  -> return a
-      Nothing -> throwError msg
-        where
-          msg = Internal.concat [ Internal.fromString $ locMessage l
-                                , "\nUndefined variable: "
-                                , x
-                                , "\n(inferVar)\n"
-                                ]
+-- * Inference
 
 infer :: Env e => Clos Term -> Eval e (Clos Type)
 --infer (g,t) | trace ("infer\ng ="++(show g)++"\n t="++(show t)++"\n") False = undefined
 
 infer (Var l x,g) = inferVar l (x,g)
 
-infer (Let _ tel t,g) = 
+infer (Let _ tel t,g) =
     do g' <- checkProg (tel,g)
-       infer (t,g')  
+       infer (t,g')
 
 infer (Type _,_) = return ty
 
-infer (Q _ _ (a,(x,b)),g) = 
+infer (Q _ _ (a,(x,b)),g) =
     do check (a,g) ty
        (_,g') <- tdecl x g (a,g)
        check (b,g') ty
        return ty
 
-infer (App t u,g) = 
+infer (App t u,g) =
     do piab <- infer' (t,g)
-       case piab of 
+       case piab of
          (VQ Pi ((a,(x,b)),s)) -> do check (u,g) (a,s)
                                      subst (x,(b,s)) (u,g)
          _ -> expectedButFound (t,g) msg1 piab msg2
@@ -217,14 +251,14 @@
 
 infer (Box  _ t,g) = liftM (first $ Lift Unknown) (infer (t,g))
 
--- TODO: either use infer', or explain why forced eval
--- cannot be used here.
+infer (Fold  _ t,g) =
+  liftM (first $ Rec Unknown . Box Unknown) (infer (t,g))
+
 infer (Force _ t,g) =
-    do a  <- infer (t,g)
-       a' <- eval a
-       case a' of
+    do a <- infer' (t,g)
+       case a of
          VLift b -> return b
-         _       -> expectedButFound (t,g) msg1 a' msg2
+         _       -> expectedButFound (t,g) msg1 a msg2
                       where
                         msg1 = "lifted type" :: Internal.String
                         msg2 = "Force"       :: Internal.String
@@ -233,29 +267,24 @@
     do check (a,g) ty
        return ty
 
--- infer (LType _ a,g) =
---     do check (a,g) lty
---        return ty
-
+infer (Rec _ a,g) =
+    do check (a,g) lty
+       return ty
 
 infer gt = throwErrorc gt $ "Not inferable" <$> "(infer)"
 
-
 -- | Infers a type and evaluates it.
 infer' :: Env e => Clos Term -> Eval e Val
-infer' gt = feval =<< infer gt
+infer' gt = eval =<< infer gt
 
-checkProg :: Env e => Clos Prog -> Eval e Scope
-checkProg ([],g) = return g
-checkProg ((Decl _ x a):tel,g) = 
-    do check (a,g) ty 
-       (_,g') <- decl x PrtInfo{ name = x, expand = False } g (Just (a,g))
-       checkProg (tel,g')
-checkProg ((Defn l x t):tel,g) =
-    do a <- inferVar l (x,g)
-       check (t,g) a
-       i <- getId l x g
-       defn' i (t,g)
-       checkProg (tel,g)
-       
-                             
+inferVar :: Env e => Loc -> Clos Name -> Eval e (Clos Type)
+inferVar l (x,g) =
+    case lookupCon g x of
+      Just a  -> return a
+      Nothing -> throwError msg
+        where
+          msg = Internal.concat [ Internal.fromString $ locMessage l
+                                , "\nUndefined variable: "
+                                , x
+                                , "\n(inferVar)\n"
+                                ]
diff --git a/src/Language/PiSigma/Equality.hs b/src/Language/PiSigma/Equality.hs
--- a/src/Language/PiSigma/Equality.hs
+++ b/src/Language/PiSigma/Equality.hs
@@ -40,32 +40,33 @@
 instance Equal Val where
     eq (Ne t0) (Ne t1) = eq t0 t1
     eq (VQ ps0 ((a0,(x0,b0)),s0)) (VQ ps1 ((a1,(x1,b1)),s1))
-      | ps0 == ps1 = 
+      | ps0 == ps1 =
         do eq (a0,s0) (a1,s1)
            eq (x0,(b0,s0)) (x1,(b1,s1))
     eq (VLam xt0) (VLam xt1) = eq xt0 xt1
-    eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = 
+    eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) =
         do eq (t0,s0) (t1,s1)
            eq (u0,s0) (u1,s1)
-    eq (VBox b) (VBox b') = eq b b' 
+    eq (VBox b) (VBox b') = eq b b'
     eq (VLift a) (VLift a') = eq a a'
---    eq (VLType a) (VLType a') = eq a a'
+    eq (VRec a) (VRec a') = eq a a'
+    eq (VFold a) (VFold a') = eq a a'
     eq v0 v1 | v0 == v1 = return () -- Type, Label, Enum
              | otherwise = fail "Different values"
 
 {- eqBox implements alpha equality -}
 eqBox :: Env e => Clos Term -> Clos Term -> Eval e ()
 --eqBox c c' | c == c' = return ()
-eqBox (Var l x,s) (Var l' y,s') = 
+eqBox (Var l x,s) (Var l' y,s') =
     do x' <- getId l  x s
        y' <- getId l' y s'
        eq x' y'
-eqBox (Let _ p t,s) c = 
+eqBox (Let _ p t,s) c =
     do s' <- evalProg (p,s)
        eqBox (t,s') c
-eqBox c c'@(Let _ _ _,_) = eqBox c' c 
+eqBox c c'@(Let _ _ _,_) = eqBox c' c
 eqBox (Q _ ps (a,(x,b)),s) (Q _ ps' (a',(x',b')),s')
-      | ps == ps' = 
+      | ps == ps' =
           do eqBox (a,s) (a',s')
              eq (x,Boxed (b,s)) (x',Boxed (b',s'))
 eqBox (Lam _ (x,t),s) (Lam _ (x',t'),s') =
@@ -81,21 +82,25 @@
        eq (x,(y,Boxed (u,s))) (x',(y',Boxed (u',s')))
 eqBox (Case _ t bs,s) (Case _ t' bs',s') =
     do eqBox (t,s) (t',s')
-       zipWithM_ (\ (l,t'') (l',t''') -> 
+       zipWithM_ (\ (l,t'') (l',t''') ->
                       if l==l' then eqBox (t'',s) (t''',s')
                       else fail "eqBox case") bs bs'
 eqBox (Lift _ t,s)  (Lift _ t',s')  = eqBox (t,s) (t',s')
--- eqBox (LType _ t,s)  (LType _ t',s')  = eqBox (t,s) (t',s')
 eqBox (Box _ t,s)   (Box _ t',s')   = eqBox (t,s) (t',s')
-eqBox (Force _ t,s) (Force _ t',s') = eqBox (t,s) (t',s')               
+eqBox (Force _ t,s) (Force _ t',s') = eqBox (t,s) (t',s')
+eqBox (Rec _ t,s)   (Rec _ t',s')   = eqBox (t,s) (t',s')
+eqBox (Fold _ t,s)  (Fold _ t',s')  = eqBox (t,s) (t',s')
+eqBox (Unfold _ t (x, u), s) (Unfold _ t' (x', u'), s') =
+    do eqBox (t,s) (t',s')
+       eq (x,Boxed (u,s)) (x',Boxed (u',s'))
 eqBox (t,_) (t',_) | t == t'   = return () -- Type, Label, Enum
                     | otherwise = fail "Different terms"
-    
+
 instance Equal Boxed where
     eq (Boxed c) (Boxed c') = eqBox c c'
 
 instance Equal Id where
-    eq i0 i1  
+    eq i0 i1
         | i0 == i1  = return ()
         | otherwise = do ei0 <- lookupId i0
                          ei1 <- lookupId i1
@@ -110,7 +115,7 @@
 
 instance Equal Ne where
     eq (NVar i0) (NVar i1) = eq i0 i1
-    eq (t0 :.. u0) (t1 :.. u1) = 
+    eq (t0 :.. u0) (t1 :.. u1) =
         do eq t0 t1
            eq u0 u1
     eq (NSplit t0 xyu0) (NSplit t1 xyu1) =
@@ -126,4 +131,7 @@
                eqBranches _ _ = fail "Case: branches differ"
            eqBranches lus0 lus1
     eq (NForce t) (NForce t') = eq t t'
+    eq (NUnfold t xu) (NUnfold t' xu') = do
+      eq t t'
+      eq xu xu'
     eq t u = fail ("Different neutrals:\n"++ show t ++"\n/=\n"++ show u ++"\n")
diff --git a/src/Language/PiSigma/Evaluate.hs b/src/Language/PiSigma/Evaluate.hs
--- a/src/Language/PiSigma/Evaluate.hs
+++ b/src/Language/PiSigma/Evaluate.hs
@@ -8,9 +8,9 @@
   , decl
   , decl'
   , defn'
+  , force
   , eval
   , evalProg
-  , feval
   , getEnv
   , getId
   , letn
@@ -42,7 +42,7 @@
            , MonadState e )
 
 run :: e -> Eval e a -> Either EvalErr (a, e)
-run e (Eval p) = runIdentity $ runErrorT $ runStateT p e 
+run e (Eval p) = runIdentity $ runErrorT $ runStateT p e
 
 catchE :: Eval e a -> (EvalErr -> Eval e a) -> Eval e a
 catchE = catchError
@@ -54,7 +54,7 @@
 setEnv = put
 
 getId :: Loc -> Name -> Scope -> Eval e Id
-getId l x s = case lookupScope s x of 
+getId l x s = case lookupScope s x of
   Just i  -> return i
   Nothing -> throwError msg
     where
@@ -108,7 +108,7 @@
 subst :: Env e => Bind (Clos Term) -> (Clos Term) -> Eval e (Clos Term)
 subst (x,(t,s)) u =
     do (i,s') <- decl' x s
-       defn' i u    
+       defn' i u
        return (t,s')
 
 evalApp :: Env e => Val -> (Clos Term) -> Eval e Val
@@ -126,23 +126,18 @@
          Closure t -> eval t
          Id j      -> return (Ne (NVar j))
 
--- use subst!
 evalSplit :: Env e
           => Val
           -> Bind (Bind (Clos Term))
           -> Eval e Val
-evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) = 
-    do (x',s2) <- decl' x s'
-       (y',s3) <- decl' y s2
-       defn' x' (l,s)
-       defn' y' (r,s)
-       eval (t,s3)
-
-evalSplit (Ne n) (xy,t) = return (Ne (NSplit n (xy,t)))
+evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) =
+    do ts2 <- subst (x, (t, s')) (l, s)
+       eval =<< subst (y, ts2) (r, s)
+evalSplit (Ne n) b = return (Ne (NSplit n b))
 evalSplit _ _ = throwError "Pair expected"
 
 evalCase :: Env e => Val -> Clos [(Label,Term)] -> Eval e Val
-evalCase (VLabel l) (lts,s) = 
+evalCase (VLabel l) (lts,s) =
     case lookup l lts of
       Nothing -> throwError "case not matched"
       Just t  -> eval (t,s)
@@ -154,13 +149,17 @@
 force (Ne n) = return (Ne (NForce n))
 force _ = throwError "Box expected"
 
+unfold :: Env e => Val -> Bind (Clos Term) -> Eval e Val
+unfold (VFold c) b = eval =<< subst b c
+unfold (Ne n)    b = return (Ne (NUnfold n b))
+unfold _         _ = throwError "Fold expected"
+
 eval :: Env e => (Clos Term) -> Eval e Val
 eval (Var l x, s)               = evalId =<< getId l x s
 eval (Let _ g t, s)             = curry eval t =<< evalProg (g,s)
 eval (Type _, _)                = return VType
 eval (Q _ ps axb, s)            = return (VQ ps (axb,s))
 eval (Lift _ t, s)              = return (VLift (t,s))
---eval (LType _ t, s)   = return (VLType (t,s))
 eval (Lam _ (x,t), s)           = return (VLam (x,(t,s)))
 eval (App t u, s)               = flip evalApp (u,s) =<< eval (t,s)
 eval (Pair _ t u, s)            = return (VPair ((t,u),s))
@@ -170,16 +169,9 @@
 eval (Case _ t lts, s)          = flip evalCase (lts,s) =<< eval (t,s)
 eval (Box _ t, s)               = return (VBox (Boxed (t,s)))
 eval (Force _ t, s)             = force =<< eval (t,s)
-
-
--- forced eval (should be integrated into eval?)
-feval :: Env e => (Clos Term) -> Eval e Val
-feval t = do t' <- eval t
-             case t' of 
-               VBox (Boxed u) -> feval u
-               v -> return v
-
-               
+eval (Rec _ t, s)               = return (VRec (t,s))
+eval (Fold _ t, s)              = return (VFold (t,s))
+eval (Unfold _ t (x, u), s)     = flip unfold (x, (u, s)) =<< eval (t,s)
 
 evalProg :: Env e => Clos Prog -> Eval e Scope
 evalProg ([],s) = return s
diff --git a/src/Language/PiSigma/Lexer.hs b/src/Language/PiSigma/Lexer.hs
--- a/src/Language/PiSigma/Lexer.hs
+++ b/src/Language/PiSigma/Lexer.hs
@@ -124,14 +124,18 @@
                             , "let"
                             , "of"
                             , "split"
-                            , "with" ]
+                            , "with"
+                            , "Rec"
+                            , "fold"
+                            , "unfold"
+                            , "as"]
   , Token.reservedOpNames = [ "!"
                             , "*"
                             , ","
                             , "->"
                             , ":"
                             , ";"
-                            , "="   
+                            , "="
                             , "\\"
                             , "^"
                             , "|"
diff --git a/src/Language/PiSigma/Normalise.hs b/src/Language/PiSigma/Normalise.hs
--- a/src/Language/PiSigma/Normalise.hs
+++ b/src/Language/PiSigma/Normalise.hs
@@ -44,27 +44,31 @@
     nf' b xs i = do e <- getEnv
                     let (PrtInfo x shouldExpand) = prtE e i
                     case getE e i of
-                      (Id _)      -> return (Var Unknown x) 
-                      (Closure t) -> if shouldExpand then nf' b xs t
-                                     -- this is bad, we should not
-                                     -- expand inside a box!
-                                     else return (Var Unknown x) 
+                      (Id _)      -> return (Var Unknown x)
+                      (Closure t) -> if shouldExpand then 
+                                         do t' <- nf' b xs t
+                                            return (Let Unknown 
+                                                [Defn Unknown x t'] (Var Unknown x))
+                                        -- we should also declare x, but we don't know its type!
+                                        -- the let cannot be expanded if inside a box!
+                                     else return (Var Unknown x)
 
 qq :: Env e => Vars -> Clos Term -> Eval e Term
 qq xs (Var l x  , s) = quote xs =<< getId l x s
-qq _  (Let _ _ _, _) = return (Label Unknown "*quote-let-not-implemented*")
---qq xs (Let l g t, s) = fail "quote let: not implemented!"
-{-do s' <- evalProg (g,s)
-                        qq xs (t,s')  
-                       -- this seems wrong! we should return a Let
-                       -- and we should extend xs!
--}
-qq xs (Q l ps (a,(x,b)),s) = 
+--qq _  (Let _ _ _, _) = return (Label Unknown "*quote-let-not-implemented*")
+qq xs (Let l g t, s) = 
+             do s' <- evalProg (g,s)
+                qq (xs ++ decls g) (t,s')
+qq xs (Q l ps (a,(x,b)),s) =
     do a' <- qq xs (a,s)
        xb' <- quote xs (x,(b,s))
        return (Q l ps (a',xb'))
 qq xs (Lift l t,s) = liftM (Lift l) (qq xs (t,s))
--- qq xs (LType l t,s) = liftM (LType l) (qq xs (t,s))
+qq xs (Rec l t,s) = liftM (Rec l) (qq xs (t,s))
+qq xs (Fold l t,s) = liftM (Fold l) (qq xs (t,s))
+qq xs (Unfold l t (x, u), s) = do t' <- qq xs (t, s)
+                                  xu' <- quote xs (x, (u, s))
+                                  return (Unfold l t' xu')
 qq xs (Lam l (x,t), s) = liftM (Lam l) (quote xs (x,(t,s)))
 qq xs (App t u ,s) = do t' <- qq xs (t,s)
                         u' <- qq xs (u,s)
@@ -76,10 +80,10 @@
                                    xyu' <- quote xs (x,(y,(u,s)))
                                    return (Split l t' xyu')
 qq xs (Case l t lts,s) = do t' <- qq xs (t,s)
-                            lts' <- mapM (\ (l',t'') -> 
+                            lts' <- mapM (\ (l',t'') ->
                                               do t''' <- qq xs (t'',s)
                                                  return (l',t''')) lts
-                            return (Case l t' lts')              
+                            return (Case l t' lts')
 qq xs (Box l t,s) = liftM (Box l) (qq xs (t,s))
 qq xs (Force l t,s) = liftM (Force l) (qq xs (t,s))
 qq _ (t,_) = return t -- Type, Enum, Label
@@ -93,11 +97,12 @@
 instance Nf Val Term where
     nf' b xs (Ne n) = nf' b xs n
     nf' _ _  VType = return (Type Unknown)
-    nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) 
+    nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s)
                                         xc' <- nf' b xs (x,(c,s))
                                         return (Q Unknown ps (a',xc'))
     nf' b xs (VLift c) = liftM (Lift Unknown) (nf' b xs c)
---    nf' b xs (VLType c) = liftM (LType Unknown) (nf' b xs c)
+    nf' b xs (VRec c) = liftM (Rec Unknown) (nf' b xs c)
+    nf' b xs (VFold c) = liftM (Fold Unknown) (nf' b xs c)
     nf' b xs (VLam xt) = liftM (Lam Unknown) (nf' b xs xt)
     nf' b xs (VPair ((t,u),s)) = do t' <- nf' b xs (t,s)
                                     u' <- nf' b xs (u,s)
@@ -116,8 +121,11 @@
                                  xyu' <- nf' b xs xyu
                                  return (Split Unknown t' xyu')
     nf' b xs (NCase t (lus,s)) = do t' <- nf xs t
-                                    lus' <- mapM (\ (l,u) -> 
+                                    lus' <- mapM (\ (l,u) ->
                                                    do u' <- nf' b xs (u,s)
                                                       return (l,u')) lus
                                     return (Case Unknown t' lus')
     nf' _ xs (NForce t) = liftM (Force Unknown) (nf xs t)
+    nf' b xs (NUnfold t xu) = do t' <- nf' b xs t
+                                 xu' <- nf' b xs xu
+                                 return (Unfold Unknown t' xu')
diff --git a/src/Language/PiSigma/Parser.hs b/src/Language/PiSigma/Parser.hs
--- a/src/Language/PiSigma/Parser.hs
+++ b/src/Language/PiSigma/Parser.hs
@@ -1,3 +1,72 @@
+{-
+
+The following grammar is (supposed to be) implemented below:
+
+variable ∷= …
+
+label ∷= …
+
+arrow ∷= "→" | "->"
+
+lambda ∷= "λ" | "\\"
+
+branch ∷= label arrow term
+
+branch⋆
+ ∷= branch "|" branch⋆
+  |
+
+label⋆
+ ∷= label label⋆
+  |
+
+variable⁺
+ ∷= variable variable⁺
+  | variable
+
+prefix-operator
+ ∷= "Rec" | "fold" | "unfold" | "^" | "∞" | "!" | "♭" | "♯"
+
+infix-operator ∷= arrow | "*"
+
+entry
+ ∷= variable ":" term ( | "=" term)
+  | variable "=" term
+
+entry⁺
+ ∷= entry ";" entry⁺
+  | entry
+
+program
+ ∷= entry⁺ ";"
+  | entry⁺
+  |
+
+atom
+ ∷= "(" term ")"
+  | variable
+  | "Type"
+  | "(" term "," term ")"
+  | "{" label⋆ "}"
+  | "′" label
+  | "case" term "of" "{" branch⋆ "}"
+  | "[" term "]"
+
+atom-or-application
+ ∷= atom
+  | prefix-operator atom
+  | atom-or-application atom
+
+term
+  ∷= atom-or-application ( | infix-operator term)
+   | "let" program "in" term
+   | "(" variable⁺ ":" term ")" infix-operator term
+   | lambda variable⁺ arrow term
+   | "split" term "with" "(" variable "," variable ")" arrow term
+   | "unfold" term "as" variable arrow term
+
+-}
+
 module Language.PiSigma.Parser
   ( parse
   , sPhrase
@@ -41,70 +110,71 @@
 
 -- * Terms
 
-sTerm5 :: Parser Term
-sTerm5 = choice
-  [ Type  <$> locReserved "Type"
+prefixOperator :: Parser (Term -> Term)
+prefixOperator = choice
+  [ Rec    <$> locReserved "Rec"
+  , Fold   <$> locReserved "fold"
+  , Lift   <$> tokLift
+  , Force  <$> tokForce
+  , Box    <$> locReservedOp "♯"
+  , unfold <$> locReserved "unfold"
+  ]
+  where
+  unfold l t = Unfold l t id
+  id         = ( Internal.fromString " x"
+               , Var Unknown (Internal.fromString " x")
+               )
 
+infixOperator :: Parser (Term -> Term -> Term)
+infixOperator = choice
+  [ (->-) <$ tokArr
+  , (-*-) <$ locReservedOp "*"
+  ]
+
+atom :: Parser Term
+atom = choice
+  [ try $ parens sTerm
+
+  , Type  <$> locReserved "Type"
+
+  , pair  <$>     location
+              <*> parens ((,) <$> sTerm <* comma <*> sTerm)
+          <?> "pair"
+
   , Enum  <$>     location
               <*> braces (many sName)
           <?> "enumeration"
 
+  , Label <$>     location
+              <*> sLabel
+          <?> "label"
+
   , Case  <$>     locReserved "case"
               <*> sTerm
               <*  reserved    "of"
               <*> braces (sBranch `sepBy` locReservedOp "|")
 
-  , Label <$>     location
-              <*> sLabel
-          <?> "label"
-
   , Box   <$>     location
-              <*> boxed sTerm
+              <*> brackets sTerm
           <?> "box"
 
-  , Lift  <$>     tokLift
-              <*> sTerm5
-          <?> "'^'"
-
   , Var   <$> location <*> sName
-  , parens sTerm
   ]
-  where
-    boxed p = choice [ brackets          p
-                     , reservedOp "♯" *> p
-                     ]
-
-sTerm4 :: Parser Term
-sTerm4 = choice
-  [ try $ (uncurry . Pair) <$> location
-                           <*> parens ((,) <$> sTerm <* comma <*> sTerm)
-  , sTerm5
-  ]
-
-sTerm3 :: Parser Term
-sTerm3 = choice
-  [ try (parens (sigmas <$> many1 ((,) <$> location <*> sName) <* reservedOp ":" <*> sTerm) <* reservedOp "*") <*> sTerm2
-  ,        Force <$> tokForce <*> sTerm4
-  , foldl1 App   <$> many1 sTerm4
-  ]
-
-sTerm2 :: Parser Term
-sTerm2 = foldr1 (-*-) <$> sTerm3 `sepBy1` reservedOp "*"
+  where pair = uncurry . Pair
 
--- TODO: make more beautiful or renumber
-sTerm1b :: Parser Term
-sTerm1b = choice
-  [ try (parens (pis <$> many1 ((,) <$> location <*> sName) <* reservedOp ":" <*> sTerm) <* tokArr) <*> sTerm
-  , sTerm2
-  ]
-       
-sTerm1 :: Parser Term
-sTerm1 = foldr1 (->-) <$> sTerm1b `sepBy1` tokArr
+atomOrApplication :: Parser Term
+atomOrApplication =
+  foldl App <$> (atom <|> prefixOperator <*> atom) <*> many atom
 
 sTerm :: Parser Term
 sTerm = choice
-  [ lam   <$  tokLam
-          <*> many ((,) <$> location <*> sName)
+  [ Let   <$> locReserved "let"
+          <*> sProg
+          <*     reserved "in"
+          <*> sTerm
+
+  , lam   <$  tokLam
+          <*> many1 ((,) <$> location <*> sName)
           <*  tokArr
           <*> sTerm
 
@@ -117,11 +187,25 @@
           <*  tokArr
           <*> sTerm
 
-  , Let   <$> locReserved "let"
-          <*> sProg
-          <*     reserved "in"
-          <*> sTerm
-  , sTerm1
+  , try (Unfold <$> locReserved "unfold"
+                <*> sTerm
+                <*  reserved "as")
+                <*> ((,) <$> sName
+                         <*  tokArr
+                         <*> sTerm)
+
+  , try (do (ns, t) <- parens $
+              (,) <$> many1 ((,) <$> location <*> sName)
+                  <*  reservedOp ":"
+                  <*> sTerm
+            op <- choice [ pis    <$ tokArr
+                         , sigmas <$ reservedOp "*"
+                         ]
+            return $ op ns t) <*> sTerm
+
+  , (\a -> maybe a ($ a)) <$>
+      atomOrApplication <*>
+      optionMaybe (flip <$> infixOperator <*> sTerm)
   ]
 
 sProg :: Parser Prog
@@ -154,7 +238,7 @@
   ]
 
 s2Terms :: Parser (Term, Term)
-s2Terms = (,) <$> sTerm5 <*> sTerm5
+s2Terms = (,) <$> atom <*> atom
 
 parse :: Parser a -> SourceName -> Parser.String -> Either ParseError a
 parse p = Parsec.parse (whiteSpace *> p <* eof)
diff --git a/src/Language/PiSigma/Pretty.hs b/src/Language/PiSigma/Pretty.hs
--- a/src/Language/PiSigma/Pretty.hs
+++ b/src/Language/PiSigma/Pretty.hs
@@ -77,25 +77,28 @@
 prettyTerm _ (Var _ x)                   =
       text $ Seq x
 
-prettyTerm _ (Let _ p t)                 =
-      list (map prettyEntry p)
-  <>  prettyTerm 0 t
+prettyTerm c (Let _ p t)                 =
+      contextParens c 0
+   $  text "let"
+  <+> sep (map prettyEntry p)
+  <+> text "in"
+  <+> prettyTerm 0 t
 
 prettyTerm _ (Type _)                    =
       text "Type"
 
 prettyTerm c (Q _ Pi (t1, (n, t2)))      =
-      contextParens c 1
+      contextParens c 0
    $  group
-   $  binding 2 n t1
+   $  binding 1 n t1
   <$> text "->"
-  <+> prettyTerm 1 t2
+  <+> prettyTerm 0 t2
 
 prettyTerm c (Q _ Sigma (t1, (n, t2)))   =
-      contextParens c 2
-   $  binding 3 n t1
+      contextParens c 0
+   $  binding 1 n t1
   <+> text "*"
-  <+> prettyTerm 2 t2
+  <+> prettyTerm 0 t2
 
 prettyTerm c (Lam _ (n, t))              =
       contextParens c 0
@@ -107,9 +110,9 @@
 prettyTerm c (App t1 t2)                 =
       group
    $  hang 2
-   $  contextParens c 3
-   $  prettyTerm 3 t1
-  <$> prettyTerm 4 t2
+   $  contextParens c 1
+   $  prettyTerm 1 t1
+  <$> prettyTerm 2 t2
 
 prettyTerm _ (Pair _ t1 t2)              =
       tupled $ map (prettyTerm 0) [t1, t2]
@@ -142,33 +145,53 @@
   <$> branches bs
 
 prettyTerm c (Lift _ t)                  =
-     contextParens c 5
-   $ text "^"
-  <> prettyTerm 5 t
+      contextParens c 1
+   $  text "^"
+  <+> prettyTerm 2 t
 
 prettyTerm _ (Box _ t)                   =
       brackets $ prettyTerm 0 t
 
 prettyTerm c (Force _ t)                 =
-     contextParens c 3
-   $ text "!"
-  <> prettyTerm 4 t
+      contextParens c 1
+   $  text "!"
+  <+> prettyTerm 2 t
 
+prettyTerm c (Rec _ t)                  =
+     contextParens c 1
+   $ text "Rec"
+  <+> prettyTerm 2 t
 
+prettyTerm c (Fold _ t)                  =
+     contextParens c 1
+   $ text "fold"
+  <+> prettyTerm 2 t
+
+prettyTerm c (Unfold _ t1 (n, t2))       =
+      contextParens c 0
+   $  hang 2
+   $  text "unfold"
+  <+> prettyTerm 0 t1
+  <+> text "as"
+  <+> text (Seq n)
+  <+> text "->"
+  <$> prettyTerm 0 t2
+
+
 prettyEntry :: Entry -> Pretty
 
 prettyEntry (Defn _ n t)                 =
       hang 2
    $  text (Seq n)
   <+> text "="
-  <$> prettyTerm 0 t
+  <+>  prettyTerm 0 t
   <>  text ";"
 
 prettyEntry (Decl _ n t)                 =
       hang 2
    $  text (Seq n)
   <+> text ":"
-  <$> prettyTerm 0 t
+  <>  prettyTerm 0 t
   <>  text ";"
 
 
diff --git a/src/Language/PiSigma/Syntax.hs b/src/Language/PiSigma/Syntax.hs
--- a/src/Language/PiSigma/Syntax.hs
+++ b/src/Language/PiSigma/Syntax.hs
@@ -35,6 +35,7 @@
   , label
   , lam
   , locMessage
+  , decls
   , lookupCon
   , lookupScope
   , pis
@@ -42,7 +43,10 @@
   , setE
   , sigmas
   , split
-  , ty )
+  , ty
+  , lty
+  , tforce
+  , tlift )
   where
 
 import Prelude
@@ -105,6 +109,12 @@
 
 type Prog = [Entry]
 
+decls :: Prog -> [Name]
+decls [] = []
+decls (Decl _ x _ : p) = x:decls p
+decls (Defn _ _ _ : p) = decls p
+
+
 {-
 Maybe better
 data Prog = Decl Type (Bind Prog) | Defn Name Term Prog
@@ -137,7 +147,9 @@
   | Lift  Loc Term
   | Box   Loc Term
   | Force Loc Term
---  | LType Loc Term -- lazy type ($ sigma)
+  | Rec   Loc Term
+  | Fold  Loc Term
+  | Unfold Loc Term (Bind Term)       -- unfold t as x -> u
   deriving (Show,Eq)
 
 instance GetLoc Term where
@@ -155,7 +167,9 @@
   getLoc (Lift  l _  ) = l
   getLoc (Box   l _  ) = l
   getLoc (Force l _  ) = l
---  getLoc (LType l _)   = l
+  getLoc (Rec   l _  ) = l
+  getLoc (Fold  l _  ) = l
+  getLoc (Unfold l _ _) = l
 
 -- * Smart constructors
 
@@ -230,7 +244,7 @@
 We then need a forgetful mapping:
 
 fog :: Ctx -> Scope
-fog c = map (\ (x,(i,a)) -> (x,(i,()))) c 
+fog c = map (\ (x,(i,a)) -> (x,(i,()))) c
 
 Alternatively, we can try to make Scopes
 existential, essentially:
@@ -267,7 +281,7 @@
 
 -- fix order, name of C...
 
-class Closure a where 
+class Closure a where
   getScope :: a -> Scope
   putScope :: a -> Scope -> a
 
@@ -288,9 +302,15 @@
 ty :: Clos Type
 ty = (Type Unknown, emptyScope)
 
---lty :: Clos Type
---lty = (Lift Unknown (Type Unknown), emptyScope)
+lty :: Clos Type
+lty = (Lift Unknown (Type Unknown), emptyScope)
 
+tforce :: Clos Type -> Clos Type
+tforce (a,s) = (Force Unknown a, s)
+
+tlift :: Clos Type -> Clos Type
+tlift (a,s) = (Lift Unknown a, s)
+
 label :: Label -> Clos Term
 label s = (Label Unknown s, emptyScope)
 
@@ -303,15 +323,16 @@
 
 data Val
   = Ne Ne
-  | VType 
+  | VType
   | VQ PiSigma (Clos (Type, Bind Type))
   | VLift (Clos Type)
   | VLam (Bind (Clos Term))
   | VPair (Clos (Term, Term))
   | VEnum [Label]
-  | VLabel Label 
+  | VLabel Label
   | VBox Boxed
---  | VLType (Clos Type)
+  | VRec (Clos Type)
+  | VFold (Clos Term)
   deriving (Show, Eq)
 
 -- | Neutral terms.
@@ -321,6 +342,7 @@
   | NSplit Ne (Bind (Bind (Clos Term)))
   | NCase Ne (Clos [(Label, Term)])
   | NForce Ne
+  | NUnfold Ne (Bind (Clos Term))
   deriving (Show, Eq)
 
 -- ** Environments
@@ -334,7 +356,7 @@
   =  PrtInfo { name   :: Name
              , expand :: Bool }
 
-class Env e where 
+class Env e where
   emptyE :: e
   extE   :: e -> PrtInfo -> (Id,e)
   setE   :: e -> Id -> EnvEntry -> e
diff --git a/src/Tools/Interpreter/Main.hs b/src/Tools/Interpreter/Main.hs
--- a/src/Tools/Interpreter/Main.hs
+++ b/src/Tools/Interpreter/Main.hs
@@ -5,7 +5,7 @@
 import Tools.Interpreter.REPL
 
 main :: IO ()
-main = 
+main =
   do
     args <- getArgs
     let ini = mapM_ (handleCommand . Load) args
diff --git a/src/Tools/Interpreter/REPL.hs b/src/Tools/Interpreter/REPL.hs
--- a/src/Tools/Interpreter/REPL.hs
+++ b/src/Tools/Interpreter/REPL.hs
@@ -105,7 +105,7 @@
 -- * REPL monad
 
 initialREPLState :: REPLState
-initialREPLState = 
+initialREPLState =
   REPLState (emptyScope, emptyE) []
 
 runREPL :: REPL () -> IO ()
@@ -334,7 +334,7 @@
         Left e  -> do
                      liftIO $ Internal.putStrLn e
                      throwError Error
-    
+
 
 inferTerm :: Term -> REPL ()
 inferTerm t =