diff --git a/AbsSynToTerm.hs b/AbsSynToTerm.hs
--- a/AbsSynToTerm.hs
+++ b/AbsSynToTerm.hs
@@ -55,18 +55,13 @@
 extractVars _ = throwError "list of variables expected"
 
 resolveTerm :: A.Exp -> Resolver Term
+resolveTerm (A.EDestr x (A.Natural n)) = Destroy (read n) <$> resolveTerm x
 resolveTerm (A.EHole (A.Hole (p,x))) = return $ Hole (Irr p) x
 resolveTerm (A.EParam x) = Param <$> resolveTerm x
-resolveTerm (A.EDestr x (A.Natural n)) = Destroy (Relevance $ read n) <$> resolveTerm x
-resolveTerm (A.EUp x) = Shift (Sort 1 0) <$> resolveTerm x
-resolveTerm (A.ELeft x) = Shift oneRel <$> resolveTerm x
+resolveTerm (A.EUp x) = Shift (Sort 1) <$> resolveTerm x
 resolveTerm (A.EVar (A.AIdent x)) = look x
-resolveTerm (A.ESet (A.Sort (p,'*':s))) = return $ Star (Irr p) $ Sort lvl rel
-    where (l,r) = break (== '@') s
-          lvl = read ('0':l)
-          rel = case r of
-            ('@':xs) -> Relevance $ read ('0':xs)
-            _ -> 0
+resolveTerm (A.ESet (A.Sort (p,"#"))) = return $ Star (Irr p) $ Sort (-1)
+resolveTerm (A.ESet (A.Sort (p,'*':s))) = return $ Star (Irr p) $ Sort (read ('0':s))
 resolveTerm (A.EProj x (A.AIdent (Identifier (_,field)))) = Proj <$> resolveTerm x <*> pure field
 resolveTerm (A.EExtr x (A.AIdent (Identifier (_,field)))) = Extr <$> resolveTerm x <*> pure field
 resolveTerm (A.EApp f x) = (:$:) <$> resolveTerm f <*> resolveTerm x
@@ -76,12 +71,15 @@
                           
    (A.EAbs _ _ _) -> throwError "cannot use lambda for type"
    _              -> Sigma (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)            
-resolveTerm (A.EPi a _arrow_ b) = case a of
+resolveTerm (A.EPi a arrow b) = case a of
    (A.EAnn vars a') -> do vs <- extractVars vars
-                          manyDep Pi a' vs b
+                          manyDep (Pi o) a' vs b
                           
    (A.EAbs _ _ _) -> throwError "cannot use lambda for type"
-   _              -> Pi (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)
+   _              -> Pi o (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)
+ where o = case arrow of                     
+         A.Arrow "=>" -> Ir
+         A.Arrow "->" -> Re
 resolveTerm (A.EAbs ids _arrow_ b) = manyLam ids b
 resolveTerm (A.EPair (A.Decl (A.AIdent i) e) rest) = Pair (Irr i) <$> resolveTerm e <*> local (insertVar i) (resolveTerm rest)
 resolveTerm (A.EPair (A.PDecl (A.AIdent i) e t) rest) = 
diff --git a/Basics.hs b/Basics.hs
--- a/Basics.hs
+++ b/Basics.hs
@@ -3,12 +3,12 @@
        (module Data.Monoid, (<>),
         module Control.Applicative,
         Irr(..), 
-        Sort(..), prettySortNam, prettyRel,
-        above, oneLev, next, oneRel, zero,
+        Sort(..),
+        above, oneLev, zero,
         Ident, Identifier(..), DisplayContext,
         Position, dummyPosition, identPosition, 
         isDummyId, modId, synthId, dummyId, idString,
-        Relevance(..), (+.),
+        Relevance(..), arrow, colon,
         Lattice(..)) where
 
 import Display
@@ -73,46 +73,45 @@
 instance Lattice Int where
     (⊔) = max
 
-newtype Relevance = Relevance {fromRel :: Int}
-  deriving (Real,Enum,Integral,Num,Ord,Eq,Show,Lattice)
+data Relevance = Re | Ir
+  deriving (Enum,Ord,Eq,Show)
 
 class Lattice a where
     (⊔) :: a -> a -> a
 
 
-data Sort = Sort {sortLevel :: Int, sortRelevance :: Relevance}
-  deriving Eq
+newtype Sort = Sort {sortLevel :: Int}
+  deriving (Eq,Num)
 
+instance Lattice Sort where
+  x ⊔ Sort (-1) = Sort (-1) -- is this a lattice? 
+  Sort x ⊔ Sort y = Sort (x ⊔ y)
+
 instance Show Sort where
-    show s = render (prettySortNam s)
+    show s = render (pretty s)
 
 
 instance Pretty Relevance where
-    pretty (Relevance 0) = mempty
-    pretty (Relevance r) = superscriptPretty r
+    pretty (Re) = mempty
+    pretty (Ir) = "÷"
 
 instance Pretty Sort where
-    pretty s = "∗" <> prettySortNam s  -- ⋆★*∗
+    pretty s = prettyLev s
     
-prettySortNam s = prettyLev s <> prettyRel s
-
-prettyRel (Sort _ r) = pretty r
+star = "∗" -- ⋆★*∗
 
-prettyLev (Sort 0 _) = mempty
-prettyLev (Sort l _) = subscriptPretty l
+prettyLev (Sort (-1) ) = "□"
+prettyLev (Sort 0    ) = star <> mempty
+prettyLev (Sort l    ) = star <> subscriptPretty l
 
-instance Num Sort where
-    Sort l1 r1 + Sort l2 r2 = Sort (l1 + l2) (r1 + r2)
-    negate (Sort l r) = Sort (negate l) (negate r)
+above (Sort l) = Sort (l + 1)
+oneLev = Sort 1
 
-above (Sort l r) = Sort (l + 1) r
-oneLev = Sort 1 0
+zero = Sort 0
 
-oneRel = Sort 0 1
-next :: Relevance -> Relevance
-next = (+ 1)
+arrow Ir = "⇒"
+arrow Re = "→"
 
-zero = Sort 0 0 
+colon Ir = text "÷"                  
+colon Re = text "∶"                  
 
-(+.) :: Relevance -> Sort -> Relevance
-r +. (Sort _ r') = r + r'
diff --git a/Main.hs b/Main.hs
--- a/Main.hs
+++ b/Main.hs
@@ -47,6 +47,7 @@
      putStrLn "Parse Failed."
      putStrV 1 $ "Tokens:" <+> pretty ts
      putStrLn $ fname ++ ":" ++ err
+     return False
    Ok tree -> do 
      process fname tree
 
@@ -60,7 +61,7 @@
     [] -> return ()
     _ -> putStrV 0 $ vcat info -- display constraints, etc.
   case checked of
-    Right (a,b,_o) -> do 
+    Right (a,b) -> do 
        putStrV 0 $ "nf =" <+> pretty a
        putStrV 0 $ "ty =" <+> pretty b
 {-
@@ -70,9 +71,10 @@
            putStrV v $ "T =" <+> prettyTerm (S.singleton i) t
          _ -> putStrV v "not a function!"
 -}
-       putStrLn "Done!"
-    Left (e,err) -> let Irr (line,col) = termPosition e 
-                    in putStrV 0 (text fname <> ":" <> pretty line <> ":" <> pretty (col - 1) <> ":" <+> err)
+       return True
+    Left (e,err) -> do let Irr (line,col) = termPosition e 
+                       putStrV 0 (text fname <> ":" <> pretty line <> ":" <> pretty (col - 1) <> ":" <+> err)
+                       return False
       
 {-
 showTree tree
@@ -83,7 +85,9 @@
 
 main :: IO ()
 main = do 
-  mapM_ runFile (files options)
+  results <- mapM runFile (files options)
+  let oks = filter id results
+  putStrV 0 $ pretty (length oks) <> "/" <> pretty (length results) <+> "files typecheck."
 
 
 
diff --git a/Normal.hs b/Normal.hs
--- a/Normal.hs
+++ b/Normal.hs
@@ -24,39 +24,53 @@
      
      Star :: Sort -> NF     
      
-     -- FIXME: only "column" / relevance should be here.
      Pi  :: Relevance -> Ident -> NF -> NF -> NF
      Lam :: Relevance -> Ident -> NF -> NF -> NF 
      App :: Relevance -> Neutral -> NF -> Neutral -- The sort is that of the argument.
      
      Sigma :: Relevance -> Ident -> NF -> NF -> NF
      Pair  :: Relevance -> Ident -> NF -> NF -> NF  -- Pair does not bind any variable.
-     Proj  :: Relevance -> -- ^ Sort of the argument
+     Proj  :: Relevance -> -- ^ Sort of the argument (only needed for
+                           -- the 1st projection: 2nd projection does
+                           -- not change relevance)
               Neutral -> Bool -> -- ^ True for 1st projection; False for 2nd.
               Irr String -> Neutral 
      
      
      OfParam :: Ident -> NF -> Neutral
 
-     Destr :: Relevance -> Variable -> Variable -- argument: level destroyed
-     Param :: Relevance -> Variable -> Variable 
+     Destr :: Int -> Variable -> Variable -- argument: depth where destruction occurs.
+     Param :: Variable -> Variable 
      V :: Sort -> Int -> Variable -- shift, deBruijn 
      Hole :: String -> Variable
 
+etaExpand :: Relevance -> Neutral -> NF -> NF
+etaExpand o' v (Pi    o i a b) = Lam  o i a (etaExpand o' (App o (wkne 1 v) 
+                                                           $ etaExpand o (var' 0) a) b)
+etaExpand o' v (Sigma o i a b) = Pair o i   (etaExpand o  (Proj o' v True  (Irr $ idString i)) a) 
+                                            (etaExpand o' (Proj o' v False (Irr $ idString i)) b)
+etaExpand o' v _ = Neu v
+
+
+
 type Subst = [NF]
 
 deriving instance Eq (Term n)
+deriving instance Show (Term n)
 
 var :: Int -> NF
 var x = Neu $ var' x
 
-var' x = Var $ V (Sort 0 0) x
+var'' = V (Sort 0)
 
+var' x = Var $ V (Sort 0) x
 
+
 -- | Hereditary substitution
 subst0 :: NF -> NF -> NF
 subst0 u = subst (u:map (var) [0..])  
 
+showShift (Sort l) = replicate l '^' 
 
 subst :: Subst -> Term n -> NF
 subst f t = case t of
@@ -74,15 +88,47 @@
 
   OfParam i x -> Neu (OfParam i (s x))
   
+  Destr d x -> destroy d (s x)
   Hole x -> Neu $ Var $ Hole x
   V s x -> shift s (f !! x)
-  Param o x -> param o (s x)
-  Destr f x -> destroy f (s x)
+  Param x -> param (s x)
  where s' = subst (var 0 : map wk f)
        s  = subst f
 
+
 -- Double renaming substitution
 -- 1st component: regular; 2nd component: param
+subst2 :: [(NF,NF)] -> Term n -> NF
+subst2 f t = case t of
+  Neu x -> s x
+  Var x -> s x
+  
+  Star x -> Star x
+  
+  Lam o i ty bo -> Lam o i (s ty) (s' bo)
+  (Pair o i x y) -> Pair o i (s x) (s y)
+  Pi o i a b -> Pi o i (s a) (s' b)
+  Sigma o i a b -> Sigma o i (s a) (s' b)
+  (App o a b) -> app o (s a) (s b)
+  (Proj o x k f) -> proj o (s x) k f
+
+  OfParam i x -> Neu (OfParam i (s x))
+  
+  Hole x -> Neu $ Var $ Hole x
+  V s x -> shift s (fst $ f !! x)
+  Param (V s x) -> shift s (snd $ f !! x)
+  Destr d x -> destroy d (s x)
+  Param x -> param (s x)
+ where s' = subst2 ((var 0, param $ var 0) : map (both wk) f)
+       s  = subst2 f
+
+
+subst2d :: Int -> (NF,NF) -> Term n -> NF
+subst2d d u = subst2 $ [(var i,param $ var i) | i <- [0..d-1]] ++ u : 
+                       [(var i,param $ var i) | i <- [d..]]
+
+
+{-
 subst' :: [(Variable,Variable)] -> Term n -> Term n
 subst' f t = case t of
   Neu x -> Neu (s x)
@@ -101,34 +147,33 @@
   
   Hole x -> Hole x
   V s x -> shift s (fst $ f !! x)
-  Param o (V s x) -> shift s (snd $ f !! x)
-  Param o x -> Param o (s x)
-  Destr f x -> Destr f (s x)
- where s' o = subst' (p o f)
+  Param (V s x) -> shift s (snd $ f !! x)
+  Param x -> Param (s x)
+ where s' o = subst' (p f)
        s  = subst' f
-       p o xs = (V zero 0, Param o $ V zero 0) : map (both $ wkv 1) xs
-       
+       p xs = (V zero 0, Param $ V zero 0) : map (both $ wkv 1) xs
+-}   
+
 both f (x,y) = (f x, f y)
 
 shift' :: Int -> Sort -> Term n -> Term n
-shift' n d@(Sort _ r) t = case t of
+shift' n d t = case t of
   Neu x -> Neu $ s x
   Var x -> Var (s x)
   
   Star o -> Star (o + d)
   
-  Lam o i ty bo -> Lam (o +. d) i (s ty) (s' bo)
-  (Pair o i x y) -> Pair (o +. d) i (s x) (s y)
-  Pi o i a b -> Pi (o +. d) i (s a) (s' b)
-  Sigma o i a b -> Sigma (o +. d) i (s a) (s' b)
-  (App o a b) -> App (o +. d) (s a) (s b)
-  (Proj o x k f) -> Proj (o +. d) (s x) k f
+  Lam o i ty bo -> Lam o i (s ty) (s' bo)
+  (Pair o i x y) -> Pair o i (s x) (s y)
+  Pi o i a b -> Pi o i (s a) (s' b)
+  Sigma o i a b -> Sigma o i (s a) (s' b)
+  (App o a b) -> App o (s a) (s b)
+  (Proj o x k f) -> Proj o (s x) k f
   
-  OfParam i x -> OfParam i (s x)
+  OfParam i x -> OfParam (modId (++showShift d) i) (s x)
 
   Hole x -> Hole x
-  Param o x -> Param (o +. d) (s x)
-  Destr f x -> Destr (f + r) (s x)
+  Param x -> Param (s x)
   V s x | x < n  -> V s x
         | x >= n -> V (s + d) x
  where s = shift' n d
@@ -151,19 +196,29 @@
 
 wkn :: Int -> NF -> NF
 wkn n = subst (map var [n..])
+
+wkdn :: Int -> Int -> NF -> NF
+wkdn d n = subst (map var [0..d-1] ++ map var [d+n..])
+
 wk = wkn 1
 str = subst0 (Neu $ Var $ Hole "str: oops!")
 
 wkv :: Int -> Variable -> Variable
-wkv n (Destr d x) = Destr d (wkv n x)
-wkv n (Param o x) = Param o (wkv n x)
+wkv n (Param x) = Param (wkv n x)
 wkv n (V s x) = V s (x + n)
 wkv n (Hole x) = Hole x
 
-param :: Relevance -> NF -> NF
-param o t = transNF 0 t o
+wkne :: Int -> Neutral -> Neutral
+wkne n (Var x) = Var (wkv n x)
+wkne n (App o a b) = App o (wkne n a) (wkn n b)
+wkne n (Proj o a k f) = Proj o (wkne n a) k f
+wkne n (OfParam i a) = OfParam i (wkn n a)
 
 
+param :: NF -> NF
+param t = transNF 0 t
+
+
 -----------------------------------
 -- Display
 
@@ -171,6 +226,7 @@
 
 freeVars :: Term n -> [Int]
 freeVars (Var x) = freeVars x
+freeVars (Destr _ x) = freeVars x
 freeVars (Neu x) = freeVars x
 freeVars (Pi _ _ a b) = freeVars a <> (dec $ freeVars b)
 freeVars (Sigma _ _ a b) = freeVars a <> (dec $ freeVars b)
@@ -181,38 +237,37 @@
 freeVars (Hole _) = mempty
 freeVars (Pair _ _ x y) = freeVars x <> freeVars y
 freeVars (Proj _ x _ _) = freeVars x
-freeVars (Param _ x) = freeVars x
+freeVars (Param x) = freeVars x
 freeVars (OfParam _ x) = freeVars x
-freeVars (Destr _ x) = freeVars x
 
 iOccursIn :: Int -> Term n -> Bool
 iOccursIn x t = x `elem` (freeVars t)
 
-prettyRel' = prettySortNam
-
 cPrint :: Int -> DisplayContext -> Term n -> Doc
 cPrint p ii (Var x) = cPrint p ii x
 cPrint p ii (Neu x) = cPrint p ii x
-cPrint p ii (Destr i x) = cPrint p ii x <> "%" <> pretty i
-cPrint p ii (Param o x) = cPrint p ii x <> sss (pretty o) <> "!"
+cPrint p ii (Param x) = cPrint p ii x <> "!"
+cPrint p ii (Destr d x) = cPrint p ii x <> "%" <> pretty d
 cPrint p ii (OfParam i x) = pretty i
                              -- "⌊" <> cPrint (-1) ii x <> "⌋"
 cPrint p ii (Hole x) = text x
 cPrint p ii (Star i) = pretty i
-cPrint p ii (V s k) 
+cPrint p ii (V o@(Sort l) k) 
   | k < 0 || k >= length ii  = text "<deBrujn index" <+> pretty k <+> text "out of range>"
   | otherwise = pretty (ii `index` k)  <> shft
-  where shft | s == Sort 0 0 = mempty
-             | otherwise = "⇧" <> prettySortNam s
-cPrint p ii (Proj o x k (Irr f))     = cPrint p ii x <> sss (pretty o) <> (if k then "#" else "/") <> text f
+  where shft = text (showShift o)
+cPrint p ii (Proj o x k (Irr f))     = cPrint p ii x <> sss (pretty o) <> (if k then "." <> text f else "/")
 cPrint p ii t@(App _ _ _)     = let (fct,args) = nestedApp t in 
                                  parensIf (p > 3) (cPrint 3 ii fct <+> sep [ sss (pretty o <> "· ") <> cPrint 4 ii a | (o,a) <- args]) 
-cPrint p ii t@(Pi _ _ _ _)    = parensIf (p > 1) (printBinders "→" ii mempty $ nestedPis t)
-cPrint p ii t@(Sigma _ _ _ _) = parensIf (p > 1) (printBinders "×" ii mempty $ nestedSigmas t)
-cPrint p ii (t@(Lam _ _ _ _))   = parensIf (p > 1) (nestedLams ii mempty t)
+cPrint p ii t@(Pi _ _ _ _)    = parensIf (p > 1) (printBinders arrow ii mempty $ nestedPis t)
+cPrint p ii t@(Sigma _ _ _ _) = parensIf (p > 1) (printBinders cross ii mempty $ nestedSigmas t)
+cPrint p ii (t@(Lam _ _ _ _)) = parensIf (p > 1) (nestedLams ii mempty t)
 cPrint p ii (Pair _ name x y) = parensIf (p > (-1)) (sep [pretty name <+> text "=" <+> cPrint 0 ii x <> comma,
                                                           cPrint (-1) ii y])
 
+cross Ir = "⤬" -- ⚔⤬⤫⨯
+cross Re = "×" -- ×⨯
+
 nestedPis  :: NF -> ([(Ident,Bool,NF,Relevance)], NF)
 nestedPis (Pi o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedPis b)
 nestedPis x = ([],x)
@@ -221,23 +276,24 @@
 nestedSigmas (Sigma o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedSigmas b)
 nestedSigmas x = ([],x)
 
-printBinders :: Doc -> DisplayContext -> Seq Doc -> ([(Ident,Bool,NF,Relevance)], NF) -> Doc
-printBinders sep ii xs (((i,occurs,a,o):pis),b) = printBinders sep (i <| ii) (xs |> (printBind' ii i occurs a o <+> sep)) (pis,b)
+printBinders :: (Relevance -> Doc) -> DisplayContext -> Seq Doc -> ([(Ident,Bool,NF,Relevance)], NF) -> Doc
+printBinders sep ii xs (((i,occurs,a,o):pis),b) = printBinders sep (i <| ii) (xs |> (printBind' ii i occurs a o <+> sss (pretty o) <> sep o)) (pis,b)
 printBinders _ ii xs ([],b)                 = sep $ toList $ (xs |> cPrint 1 ii b) 
 
 
 nestedLams :: DisplayContext -> Seq Doc -> Term n -> Doc
-nestedLams ii xs (Lam o x ty c) = nestedLams (x <| ii) (xs |> parens (sss (pretty o) <> pretty x <+> ":" <+> cPrint 0 ii ty)) c
+nestedLams ii xs (Lam o x ty c) = nestedLams (x <| ii) (xs |> parens (sss (pretty o) <> pretty x <+> colon o <+> cPrint 0 ii ty)) c
 nestedLams ii xs t         = (text "\\ " <> (sep $ toList $ (xs |> "->")) <+> nest 3 (cPrint 0 ii t))
 
-printBind' ii name occurs d o = case not (isDummyId name) ||  occurs of
-                  True -> parens (sss (pretty o) <> pretty name <+> text ":" <+> cPrint 0 ii d)
+printBind' ii name occurs d o = case not (isDummyId name) || occurs of
+                  True -> parens (pretty name <+> colon o <+> cPrint 0 ii d)
                   False -> cPrint 2 ii d
-
+                  
 nestedApp :: Neutral -> (Neutral,[(Relevance, NF)])
 nestedApp (App o f a) = (second (++ [(o,a)])) (nestedApp f)
 nestedApp t = (t,[])
 
+
 sss x = if showSorts options then x else mempty
 
 prettyTerm = cPrint (-100)
@@ -259,16 +315,22 @@
                       in (v, Hole "does not appear!")
                           -- Param evil v)
 
-evil = Sort 0 666
+-- paramShift = if collapseRelevance options then zero else oneRel
+              -- TODO: have this as an argument to
+              -- Param. Alternatively, add a construct to collapse
+              -- levels.
 
+next :: Relevance -> Relevance
+next _ = Ir -- (+ (sortRelevance paramShift))
 
-renam :: Int -> Int -> NF -> NF
-renam d idx = subst [var $ mv d $ x | x <- [0..]] . shift' d oneRel
 
-renam' d = subst' (map (mv' d) [0..])
+-- renam :: Int -> Int -> NF -> NF
+-- renam d idx = id -- subst [var $ mv d $ x | x <- [0..]] 
 
+-- renam' d = subst' (map (mv' d) [0..])
+
 re :: Ident -> Ident
-re (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,x++"₁")))
+re (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,x++"°")))
 
 arity, idx :: Int
 arity = 1
@@ -276,66 +338,58 @@
 
 
 -- | Transform a term to its relational interpretation
--- NOTE: the level of the sort is incorrect! In fact only the rel. ever matters. (Destroy)
-transV :: Int -> Variable -> Relevance -> Variable
-
-transV d (V o x) o' | x < d =                V o $ (arity + 1) * x
-                    | otherwise = Param o' $ V o $ (x - d) + (arity + 1) * d
-transV d (Param o' x) o = Param o' $ transV d x o
-transV d (Destr n x) o = destroy n (transV d x o)
-transV d (Hole s) _ = Hole (s ++ "!")
+transV    :: Int -> Variable -> Variable
 
-transNe :: Int -> Neutral -> Relevance -> NF
-transNe d (Var v) o = Neu $ Var $ transV d v o
-transNe d (App o f a) o' = app o (app (next o) (transNe d f o') (renam d idx a)) (transNF d a o) 
-transNe d (Proj o x k f) o' = proj o (transNe d x o) k f
-transNe d (OfParam i t) o = app o (renam' d t) (renam d idx (Neu $ OfParam i t))
+transV  d (V o x) = Param $ V o x
+transV  d (Param x) = Param $ transV d x
+transV  d (Hole s) = Hole (s ++ "!")
 
-transNF :: Int -> NF -> Relevance -> NF
-transNF d (Neu v) o = transNe d v o
-transNF d (Lam o i ty bo) o' = transBind d Lam o i ty (transNF (d+1) bo o')
-transNF d (Pair o i x y) o' = Pair o i (transNF d x o) (transNF d y o') 
-transNF d ty@(Star  _) o = trans' d ty o
-transNF d ty@(Pi    _ _ _ _) o = trans' d  ty o
-transNF d ty@(Sigma _ _ _ _) o = trans' d ty o
+transNe :: Int -> Neutral -> NF
+transNe d (Var v)      = Neu $ Var $ transV d v
+transNe d (App Re f a)  = app Re (app Ir (transNe d f) a) (transNF d a) 
+transNe d (App Ir f a)  =         app Ir (transNe d f) a
+transNe d (Proj o x k f) = proj o (transNe d x) k f
+transNe d (OfParam i t)  = app Ir t (Neu $ OfParam i t)
 
-trans' d ty o = Lam (next o) (synthId "z₁") (renam d idx ty) (zerInRel d ty o)
+transNF :: Int -> NF -> NF
+transNF d (Neu v) = transNe d v
+transNF d (Lam o i ty bo) = transBind d Lam o i ty (transNF (d+1) bo)
+transNF d (Pair o i x y)  = Pair o i (transNF d x) (transNF d y) 
+transNF d ty@(Star  _)  = trans' d ty
+transNF d ty@(Pi    _ _ _ _) = trans' d ty
+transNF d ty@(Sigma _ _ _ _) = trans' d ty
 
--- | Build a relation witnessing x ∈ ⟦ty⟧. (where 'x' is Bound 0 in 'ty'.)
+trans'  d ty = Lam Ir (synthId "z") ty (zerInRel d ty)
 
--- In the translated context, 'z1', ... 'zn' are bound, but not
--- 'zR'. (we are going to bind it soon).  However, 'inTrans' assumes
--- it has "full" translated context.  So we weaken 'ty' (putting 'z' in scope) and apply the
--- translation as normal.  But the translation is well behaved, so it
--- does not use 'zR'. We substitute it with nothing when the job is
--- done.
-zerInRel d ty o = str $ inTrans (d + 1) (wk ty) o (var 0)
+-- | Build the relation x ∈ ⟦ty⟧. (where 'x' is 0; but not bound in 'ty'.)
+zerInRel d ty = inTrans (d + 1) (wk ty) (var 0)
 
 -- | Build a relation z ∈ ⟦ty⟧.  z is a term that, after renaming,
 -- gives the vector of terms member of the relation.  Note that
 -- 'trans' is never applied to 'z', therefore 'zR' never occurs in the result.
 
-inTrans :: Int -> NF -> Relevance -- ^ sort of the 1st argument
-           -> NF -> NF
-inTrans d (Star  s)       o z = (Pi (next o) dummyId (renam d idx z) (Star s))
-inTrans d (Pi    o i a b) o' z = transBind d Pi o i a (inTrans (d + 1) b o' (app o (wk z) (var 0)))
-inTrans d (Sigma o i a b) o' z = Sigma o i (inTrans d a o (proj o z True f)) 
-                             (subst (var 0:wk (renam d idx (proj o z True f)):map var [1..]) $
-                              inTrans (1 + d) b o' (proj o (wk z) False f)) -- TEST: is depth ok?
+
+inTrans :: Int -> NF -> NF -> NF
+inTrans d (Star  s)       z = (Pi Ir dummyId z (Star s))
+inTrans d (Pi    o i a b) z = transBind d Pi o i a (inTrans (d + 1) b (app o (wk z) (var 0)))
+inTrans d (Sigma o i a b) z = Sigma o (re i) (inTrans d a (proj o z True f)) $
+                              subst2d 1 (wk $ proj o z True f, var 0) $ wk $
+                              inTrans (1 + d) b (proj o (wk z) False f) -- TEST: is depth ok?
  where (Irr (Identifier (_,nam))) = i
        f = Irr nam
-inTrans d t o z = app (next o) (transNF d t o) (renam d idx z) 
+inTrans d t z = app Ir (transNF d t) z
 
 
 -- | Translate a binding (x : A) into (x₁ : A₁) (⟦x⟧ : ⟦A⟧ x₁)
 transBind :: Int -> (Relevance -> Ident -> NF -> NF -> NF) -> Relevance -> Ident -> NF -> NF -> NF
-transBind d binder o i a rest = binder (next o) (re i) (renam d idx a) $
-                                binder o            i  (zerInRel d a o) $ 
-                                rest
+transBind d binder Re i a rest = binder Ir i a $ 
+                                 binder Re (re i) (zerInRel d a) $ 
+                                 subst2d 2 (var 1,var 0) $ wkn 2 rest
 
+transBind d binder Ir i a rest = binder Ir i a rest
 
 -- Invariant: the whole term is not destroyed.
-destroy :: Relevance -> Term n -> Term n
+destroy :: Int -> Term n -> Term n
 destroy d t = case t of
   Var x -> Var $ pr x
   Neu x -> Neu $ pr x
@@ -343,8 +397,8 @@
   V o x -> V o x
   Hole x -> Hole x
   Destr d' t -> destroy (min d d') t -- coalesce
-  Param r x | r+1 == d -> x
-            | otherwise -> Destr d $ Param r x 
+  Param x | d == 0 -> x
+          | otherwise -> Destr d $ Param x 
 
   (Star o) -> Star o
   (Pi o i a b)    -> mb Pi    o i a b 
@@ -352,24 +406,24 @@
   (Lam o i ty bo) -> mb Lam   o i ty bo  
   (Pair o i a b) 
       | isDestroyed o -> pr b
-      | otherwise -> Pair o i (pr a) (pr b) 
+      | otherwise -> Pair o i (pr' o a) (pr b) 
   (App o a b)  -> case isDestroyed o of
                    True -> pr a
-                   False -> App o (pr a) (pr b)
+                   False -> App o (pr a) (pr' o b)
   (Proj o x k f) -> case isDestroyed o of
     True -> pr x -- result of the projection is not destroyed (by
                   -- assumpt.) but the whole pair would be -> we must
                   -- keep the 1st component.
-    False -> Proj o (pr x) k f
+    False -> Proj o (pr x) k f -- FIXME: hmmm, here we should probably use pr' (symmetry)
   (OfParam n x) -> OfParam (modId (++ "%" ++ show d) n) $ pr x
   
  where 
-   isDestroyed o = d `destroys` o
+   isDestroyed o = d == 0 && o == Ir
    mb :: (Relevance -> Ident -> NF -> NF -> NF) -> Relevance -> Ident -> NF -> NF -> NF
    mb binder o i a b = case isDestroyed o of
                              True -> str (pr b)
-                             False -> binder o i (pr a) (pr b)
+                             False -> binder o i (pr' o  a) (pr b)
    pr x = destroy d x
-
+   pr' Ir x = destroy (d-1) x
+   pr' Re x = pr x
 
-r `destroys` r' = r' >= r
diff --git a/Options.hs b/Options.hs
--- a/Options.hs
+++ b/Options.hs
@@ -13,6 +13,7 @@
   Args {verb :: Int,
         typeSystem :: TypeSystem,
         showSorts :: Bool,
+        collapseRelevance :: Bool,
         files :: [String]
         } 
   deriving (Show, Data, Typeable)
@@ -23,6 +24,7 @@
                                    CCω &= name "I" &= help "CCω (Impredicative)"]
                                , -- &= opt (0 :: Int),
                 showSorts = False &= help "display sort annotations in normal forms",
+                collapseRelevance  = False &= help "! (param) does not generate new relevance levels.",
                 files = [] &= args &= typFile
               }
          
diff --git a/RawSyntax.hs b/RawSyntax.hs
--- a/RawSyntax.hs
+++ b/RawSyntax.hs
@@ -15,9 +15,9 @@
 ESet.    Exp6 ::= Sort ;
 EParam.  Exp4 ::= Exp4 "!";
 EUp.     Exp4 ::= Exp4 "^";
-ELeft.   Exp4 ::= Exp4 "<";
+-- ELeft.   Exp4 ::= Exp4 "<";
 EDestr.  Exp4 ::= Exp4 "%" Natural ;
-EProj.   Exp4 ::= Exp4 "#" AIdent ;
+EProj.   Exp4 ::= Exp4 "." AIdent ;
 EExtr.   Exp4 ::= Exp4 "/" AIdent ;
 EApp.    Exp3 ::= Exp3 Exp4 ;
 EPi.     Exp2  ::= Exp3 Arrow Exp2 ;
@@ -33,7 +33,7 @@
 terminator AIdent "" ;
 terminator Decl ";" ;
 
-token Arrow  '-' '>' ;
+token Arrow  ('-' '>') | ('=' '>') ;
 
 NoBind. Bind   ::= AIdent ; 
 Bind.   Bind   ::= "(" AIdent ":" Exp ")" ;
@@ -46,6 +46,6 @@
 
 position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;
 
-position token Sort '*' (digit*) ('@' digit+)?;
+position token Sort ('#' | '*' (digit*));
 
 |]
diff --git a/Terms.hs b/Terms.hs
--- a/Terms.hs
+++ b/Terms.hs
@@ -21,7 +21,7 @@
      Hole :: Irr Position -> String -> Term -- placeholder
      Star :: Irr Position -> Sort -> Term -- sort
      Bound :: Irr Position -> Int -> Term -- variable
-     Pi :: Ident -> Term -> Term -> Term 
+     Pi :: Relevance -> Ident -> Term -> Term -> Term 
      Sigma :: Ident -> Term -> Term -> Term
      Lam :: Ident -> Term -> Term -> Term 
      Pair :: Ident -> Term -> Term -> Term 
@@ -43,13 +43,13 @@
      -- relational interpretations and world destruction.  In normal
      -- form, arguments to these are either themselves or a variable.
      Param :: Term -> Term 
-     Destroy :: Relevance -> Term -> Term
+     Destroy :: Int -> Term -> Term
 
 termPosition :: Term -> Irr Position 
 termPosition (Hole p _) = p
 termPosition (Star p _) = p
 termPosition (Bound p _) = p
-termPosition (Pi i _ _) = identPosition i
+termPosition (Pi _ i _ _) = identPosition i
 termPosition (Sigma i _ _) = identPosition i
 termPosition (Lam i _ _) = identPosition i
 termPosition (Pair i _ _) = identPosition i
@@ -147,7 +147,7 @@
 
 freeVars :: Term -> [Int]
 freeVars (Ann a b) = freeVars a <> freeVars b
-freeVars (Pi _ a b) = freeVars a <> (dec $ freeVars b)
+freeVars (Pi _ _ a b) = freeVars a <> (dec $ freeVars b)
 freeVars (Sigma _ a b) = freeVars a <> (dec $ freeVars b)
 freeVars (Bound _ x) = [x]
 freeVars (a :$: b) = freeVars a <> freeVars b
@@ -170,7 +170,8 @@
 
 cPrint :: Int -> DisplayContext -> Term -> Doc
 cPrint p ii (Destroy i x) = cPrint p ii x <> "%" <> pretty i
-cPrint p ii (Shift o x) = cPrint 6 ii x <> "⇧" <> prettySortNam o
+cPrint p ii (Shift (Sort l) x) = cPrint 6 ii x <> text (replicate l '^') 
+                                   -- "⇧" <> prettySortNam o
 cPrint p ii (Param x) = cPrint p ii x <> "!"
 cPrint p ii (OfParam i x) = pretty i
                              -- "⌊" <> cPrint (-1) ii x <> "⌋"
@@ -183,7 +184,8 @@
 cPrint p ii (Extr x f)     = cPrint p ii x <> "/" <> text f
 cPrint p ii t@(_ :$: _)     = let (fct,args) = nestedApp t in 
                                  parensIf (p > 3) (cPrint 3 ii fct <+> sep (map (cPrint 4 ii) args))
-cPrint p ii (Pi name d r)    = parensIf (p > 1) (sep [printBind ii name d r <+> text "→", cPrint 1 (name <| ii) r])
+cPrint p ii (Pi o name d r)    = parensIf (p > 1) (sep [printBind ii name d r <+> arrow o, cPrint 1 (name <| ii) r])
+                                 
 cPrint p ii (Sigma name d r) = parensIf (p > 1) (sep [printBind ii name d r <+> text "×",  cPrint 1 (name <| ii) r])
 cPrint p ii (t@(Lam _ _ _))   = parensIf (p > 1) (nestedLams ii mempty t)
 cPrint p ii (Ann c ty)      = parensIf (p > 0) (cPrint 1 ii c <+> text ":" <+> cPrint 0 ii ty)
diff --git a/TypeCheckerNF.hs b/TypeCheckerNF.hs
--- a/TypeCheckerNF.hs
+++ b/TypeCheckerNF.hs
@@ -67,59 +67,62 @@
 dispContext ctx = case viewl ctx of
   EmptyL -> mempty
   Bind x val typ o :< ctx' -> let di = display ctx' in (case val of
-    Abstract   ->             pretty x <+>                             ":" <+> di typ <+> ":" <+> pretty o
+    Abstract   ->             pretty x <+>                             colon o <+> di typ
 --    Direct (OfParam _ v) ->   "⟦"<>pretty x<>"⟧" <+> sep ["=" <+> parens (di v), "::" <+> di typ]
-    Direct   v ->             pretty x <+> sep ["=" <+> parens (di v), ":" <+> di typ <+> ":" <+> pretty o]
+    Direct   v ->             pretty x <+> sep ["=" <+> parens (di v), colon o <+> di typ]
     ) $$ dispContext ctx'
 
-instance Lattice Sort where 
-  s1@(Sort l1 r1) ⊔ s2@(Sort l2 r2) 
-    | r1 /= r2 = s2
-    | otherwise = case typeSystem options of
-      CCω | l2 == 0 -> s2 -- The impredicative rule of CCω
-      _ -> Sort (max l1 l2) r2
+-- FIXME: flag an error if impredicativity disabled and we use it anyway.
 
 hole = Neu . Var . Hole
 
-iType :: Context -> Term -> Result (Value,Type,Relevance)
+todo = Re
+
+resurrect :: Relevance -> Context -> Context
+resurrect Re = id
+resurrect Ir = fmap (\e -> e {entryRelevance = Re})
+
+iType :: Context -> Term -> Result (Value,Type)
 iType g (Ann e tyt)
   =     do  (ty,o) <- iSort g tyt 
             v <- cType g e ty
-            return (v,ty,sortRelevance o) -- annotations are removed
+            return (v,ty) -- annotations are removed
 iType g t@(Terms.Star p s)
-   =  return (Star s,Star $ above s, sortRelevance s)  
-iType g (Terms.Pi ident tyt tyt')  
-   =  do  (ty ,s1) <- iSort g tyt 
-          let r1 = sortRelevance s1
+   =  return (Star s,Star $ above s)  
+iType g (Terms.Pi r1 ident tyt tyt')  
+   =  do  (ty ,s1) <- iSort (resurrect r1 g) tyt 
           (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'
           let o = s1 ⊔ s2
-          return (Pi r1 ident ty ty', Star o, sortRelevance o)
+          return (Pi r1 ident ty ty', Star o)
 iType g (Terms.Sigma ident tyt tyt')  
-   =  do  (ty,s1)  <- iSort g tyt 
-          let r1 = sortRelevance s1
+   =  do  let r1 = todo
+          (ty,s1)  <- iSort (resurrect r1 g) tyt 
           (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'
           let o = s1 ⊔ s2
-          return (Sigma r1 ident ty ty', Star o, sortRelevance o)
-iType g e@(Terms.Bound _ x) = return $ (val $ entryValue e, wkn (x+1) $ entryType e,entryRelevance e)
+          return (Sigma r1 ident ty ty', Star o)
+iType g e@(Terms.Bound _ x) = case o of
+  Ir -> throwError (e,"Cannot use irrelevant variable in relevant context")
+  Re -> return $ (val $ value, wkn (x+1) $ typ)
   where val (Direct v) = wkn (x+1) v
-        val _ = var x
-        e = g `index` x
+        val _ = var x -- etaExpand o (var' x) typ
+        Bind _ value typ o = g `index` x
+        
 iType g (Terms.Hole p x) = do
   report $ hang (text ("context of " ++ x ++ " is")) 2 (dispContext g)
-  return (hole x, hole ("type of " ++ x), 0)
+  return (hole x, hole ("type of " ++ x))
 iType g (e1 Terms.:$: e2)
-  =     do  (v1,si,o') <- iType g e1
+  =     do  (v1,si) <- iType g e1
             case si of
               Pi o _ ty ty' -> do 
-                   v2 <- cType g e2 ty
-                   return (app o v1 v2, subst0 v2 ty',o') 
+                   v2 <- cType (resurrect o g) e2 ty
+                   return (app o v1 v2, subst0 v2 ty') 
               _             ->  throwError (e1,"invalid application")
 iType g (Terms.Proj e f) = do
-  (v,t,o') <- iType g e
+  (v,t) <- iType g e
   search v t
- where search :: NF -> NF -> Result (Value,Type,Relevance)
+ where search :: NF -> NF -> Result (Value,Type)
        search v (Sigma o (Irr (Identifier (_,f'))) ty ty') 
-              | f == f' = return (π1,ty,o)
+              | f == f' = return (π1,ty)
               | otherwise = search π2 (subst0 π1 ty')
            where 
                  (π1,π2) = (case v of
@@ -129,39 +132,39 @@
        search _ _ = throwError (e,"field not found")
 
 iType g (Terms.Pair ident e1 e2) = do
-  (v1,t1,o) <- iType g e1
-  (v2,t2,o') <- iType (Bind ident (Direct v1) t1 o <| g) e2
-  return $ (Pair o ident v1 (str v2),Sigma o ident t1 t2,o ⊔ o')
+  (v1,t1) <- iType g e1
+  let r1 = todo
+  (v2,t2) <- iType (Bind ident (Direct v1) t1 r1 <| g) e2
+  return $ (Pair r1 ident v1 (str v2),Sigma r1 ident t1 t2)
 -- Note: the above does not infer a most general type: any potential dependency is discarded.
 
 iType g t@(Terms.Lam x (Terms.Hole _ _) e) = throwError (t,"cannot infer type for" <+> displayT g t)
 iType g (Terms.Lam x ty e) = do
-    (vty,Sort _ o) <- iSort g ty
-    (ve,t,o') <- iType (Bind x Abstract vty o <| g) e
-    return $ (Lam o x vty ve, Pi o x vty t, o')
+    (vty,Sort _) <- iSort g ty
+    let o = todo
+    (ve,t) <- iType (Bind x Abstract vty o <| g) e
+    return $ (Lam o x vty ve, Pi o x vty t)
 
 iType g (Terms.Param e) = do
-  (v,t,o) <- iType g e
-  return (param o v, app (next o) (param o t) (shift oneRel v), o)
+  (v,t) <- iType g e
+  return (param v, app Ir (param t) v)
 
 iType g (Terms.Shift f e) = do
-  (v,t,o) <- iType g e
-  return (shift f v, shift f t, o + sortRelevance f)
+  (v,t) <- iType g e
+  return (shift f v, shift f t)
 
 iType g x@(Terms.Destroy d e) = do
-  (v,t,o) <- iType g e  
-  case d `destroys` o of
-    True -> throwError (x,"total destruction is forbidden. destroyed term:" <+> display g v)
-    False -> return (destroy d v,destroy d t, d-1) 
+  (v,t) <- iType g e  
+  return (destroy d v,destroy d t) 
 
 iSort :: Context -> Term -> Result (Type,Sort)
 iSort g e = do
-  (val,v,_) <- iType g e
+  (val,v) <- iType g e
   case v of 
     Star i -> return (val,i)
     (Neu (Var (Hole h))) -> do 
          report $ text h <+> "must be a type"
-         return $ (hole h, Sort 1 0)
+         return $ (hole h, Sort 1)
     _ -> throwError (e,displayT g e <+> "is not a type")
 
 unify :: Context -> Term -> Type -> Type -> Result ()
@@ -207,11 +210,7 @@
   -- Γ ⊢ A ⌊A⌋ : ⟦B⟧ ⌊A⌋
   -- Γ ⊢ A x   : ⟦B⟧ x
   -- Γ ⊢ A     : (x : ⌊B⌋) → ⟦B⟧ x
-  -- FIXME: here I just assume the relevance of t is the following.
-  let theRelevance = 0 
-      theType = Pi (next theRelevance) i (shift oneRel $ t) 
-                   (zerInRel 0 t theRelevance)
-  e' <- cType g e theType       
+  e' <- cType g e $ Pi Ir i t (zerInRel 0 t)
   return (Neu $ OfParam i e')
 
 cType g (Terms.Shift f e) t = do
@@ -222,7 +221,7 @@
   -- sort.
 
 cType g e v 
-  =     do (e',v',_o) <- iType g e
+  =     do (e',v') <- iType g e
            unify g e v v'
            return e'
 
diff --git a/tutorial/01-Module.ua b/tutorial/01-Module.ua
--- a/tutorial/01-Module.ua
+++ b/tutorial/01-Module.ua
@@ -49,12 +49,12 @@
 -- Dependent pairs can also be declared
 depPair  = (A = Nat, suc) : ((A : *1) ; A -> A),
 
--- fields named in the type can be extracted using #:
-extract = depPair # A,
+-- fields named in the type can be extracted using .:
+extract = depPair.A,
 
 -- Finally we must give the last component of the tuple, which is NOT
 -- named.  Since we have nothing special in mind, let's just give a
--- trival (meaningless) term:
+-- random simple term:
 
 *
 
diff --git a/tutorial/02.1-Relevance.ua b/tutorial/02.1-Relevance.ua
--- a/tutorial/02.1-Relevance.ua
+++ b/tutorial/02.1-Relevance.ua
@@ -1,61 +1,60 @@
--- Relevance levels and erasure
----------------------------------
+-- Relevance and erasure
+-------------------------
 
--- In uAgda, each term can exist at a specific relevance. 
--- 
--- For example * is the most relevant level, *< is less relevant, etc.
--- 
--- The idea is that a term less relevant worlds can be erased, and the
--- terms remains meaningful.
+-- In uAgda, there are two flavours of quantification:
+-- relevant and irrelevant. (We borrow the notion from Pfenning (2001)).
 
+-- One can roughly thing as irrelevant things as things whose
+-- computational content is inaccessible ("proofs"), while relevant
+-- ones are regular terms whose computational content is relevant.
+-- Irrelevant product is denoted with =>. Irrelevancy of abstraction
+-- and applications is inferred.
 
--- For example, we can use a more precise type of the Leibniz equality
--- that says that the actual type used is irrelevant for the predicate:
+-- Irrelevancy is enforced by making sure irrelevant variables are
+-- never directly returned. They can only be used as arguments to
+-- irrelevant applications or on the LHS of =>.
 
-Eq = \ A a b -> (P : A -> *) -> P a -> P b
-     : (A : *<) -> (a b : A) -> *1,
+-- For example the following term does not type-check because 'A' is
+-- used in the result directly, while it is irrelevant: 
 
+{-
+Wrong = \(A : *) -> A 
+      : * => *,
+-}
+
+-- An example where irrelevance can be used for more precise typing is
+-- the following. We can use a more precise type of the Leibniz
+-- equality that says that the actual type used is irrelevant for the
+-- predicate:
+
+Eq = \ A a b -> (P : A => *) -> P a -> P b
+     : (A : *) -> (a b : A) => *1,
+
 -- Another example is the following: the inductive principle for
 -- natural numbers is independent on the actual representation of the
 -- naturals, so they are irrelevant.  This can be expressed as
--- follows:
+-- follows...
 
--- We assume an (abstract) representation N of naturals, in a less
--- relevant world, as well as constructors for successor and zero.
 
-Nat = \(N : *<) (s : N -> N) (z : N) ->
+Nat = 
+      -- We assume an (abstract) representation N of naturals, as well as
+      -- constructors for successor and zero.
+      \(N : *) (s : N -> N) (z : N) ->
 
--- Then define the induction principle as normal (the predicate is in *)
-\(n : N) -> (P : N -> *) -> P z -> ((m : N) -> P m -> P (s m)) -> P n,
+      -- Then define the induction principle:
+      \(n : N) -> (P : N => *) -> P z -> ((m : N) => P m -> P (s m)) -> P n,
 
 
 -- We know that all the programs we have written using naturals
 -- satisfying the above induction principle can be represented by
 -- Naturals where the irrelevant parts are erased. We can access this
 -- erasure within uAgda by using the % operator. The second argument
--- is the first world of relevance to erase (all less relevant worlds
--- will be erased as well).
+-- is the depth of irrelevancy to erase. 
 
-Nat-representation = Nat % 1,
+Nat-representation = Nat % 0,
 
 -- The normal form of the above term reveals that the result is the
 -- usual Church encoding for naturals.
-
-
--- Each term can be copied to a less relevant world:
-
-shiftType = \A -> A<
-          : * -> *<,
-
-shiftValue 
-  = \ A a -> a<
-  : (A : *) -> (a : A) -> A<,
-
-
--- In summary, occurences of the < operator can be understood as
--- relevance annotations. They can be used mark types, terms and their
--- usage as irrelevant. They are useful for erasure, but may be safely
--- ignored otherwise.
 
 
 *
diff --git a/tutorial/03-Parametricity.ua b/tutorial/03-Parametricity.ua
--- a/tutorial/03-Parametricity.ua
+++ b/tutorial/03-Parametricity.ua
@@ -6,27 +6,18 @@
 \(A : *) (B : *) (f : A -> B) -> (
 
 -- we can use the fact that it is parametric by using the postfix '!' operator:
-fparam = f! : (x : A<) -> A! x -> B! (f< x),
-
-
--- Note that the "x" an irrelevant argument to f!. We say that it lies
--- in another relevance world. This is indicated by the postfix <
--- after its type.
-
--- that is ok, because we can always convert a term into a copy of it at 
--- a less relevant level (using that operator).
-
+fparam = f! : (x : A) => A! x -> B! (f x),
 
 -- It is also possible to erase all the stuff less relevant than a
 -- certain world by using the operator '%'. For example, after
 -- erasing all the (level one) irrelevant stuff from the above type we
 -- recover the original (check the normal form):
 
-eraseType = ((x : A<) -> A! x -> B! (f< x)) % 1,
+eraseType = ((x : A) => A! x -> B! (f x)) % 0,
 
 
--- Indeed, f!%1 = f.
-fAgain = fparam %1,
+-- Indeed, f!%0 = f.
+fAgain = fparam %0,
 
 
 -- We can get binary parametricity by combination of unary
@@ -35,9 +26,7 @@
 
 -- http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466
 
-fparam2 = f!!%2 : (x y : A<) -> A!!%2 x y -> B!!%2 (f< x) (f< y),
-
-
+fparam2 = f!!%1, -- : (x y : A) => A!!%2 x y => B!!%2 (f x) (f y),
 
 
 *)
diff --git a/tutorial/03.1-Parametricity-Use.ua b/tutorial/03.1-Parametricity-Use.ua
--- a/tutorial/03.1-Parametricity-Use.ua
+++ b/tutorial/03.1-Parametricity-Use.ua
@@ -1,26 +1,23 @@
 -- let's use parametricity in a useful way: prove that any
--- function of type (X : *) -> X -> X is the identity.
+-- function of type (X : #) -> X -> X is the identity.
 
--- To simplify the example we use impredicativity here, use
--- the -I flag to enable it.
+-- To simplify the example we use impredicativity here.
 
-Eq = \A a b -> (P : A -> *) -> P a -> P b
-   : (A : *<) -> A -> A -> *
+Eq = \A a b -> (P : A => #) -> P a -> P b
+   : (A : #) -> A => A => #
    ,
 
 Theorem = 
-  (f : (A : *) -> A -> A) ->
-  (A : *) ->
+  (f : (A : #) -> A -> A) ->
+  (A : #) ->
   (x : A) ->
-  Eq A< x< (f A x)<,
+  Eq A x (f A x),
 
 
-proof = \(f : (A : *) -> (a : A) -> A) ->
-        \(A : *) ->
-        \(x : A) -> f! A< (Eq A< x<) x< (\_ p -> p)
+proof = \(f : (A : #) -> (a : A) -> A) ->
+        \(A : #) ->
+        \(x : A) -> f! A (\y -> Eq A x y) x (\_ p -> p)
       : Theorem
-
-
 ,
-* 
+# 
 
diff --git a/tutorial/04-Data.ua b/tutorial/04-Data.ua
--- a/tutorial/04-Data.ua
+++ b/tutorial/04-Data.ua
@@ -29,7 +29,7 @@
 
 param Q = \ q -> (
 
-Nat = \n -> (P : q#Nat -> *) -> ((n : q#Nat) -> P n -> P (q#suc n)) -> (P q#zer) -> P n,
+Nat = \n -> (P : q.Nat => *) -> ((n : q.Nat) => P n -> P (q.suc n)) -> (P q.zer) -> P n,
 zer = \P s z -> z,
 suc = \m n P s z -> s m (n P s z),
 \ _ -> *)
@@ -45,15 +45,15 @@
 
 
 -- From there we can do simple computations:
-one = Q#suc Q#zer : Q#Nat,
-two = Q#suc one,
+one = Q.suc Q.zer : Q.Nat,
+two = Q.suc one,
 
 
 
 -- And we can also do inductive reasoning (but indexed by a less
 -- relevant version of the type/values):
 Nat-elim = \n -> n!
-         : (n : Q#Nat) -> (P : Q<#Nat -> *) -> ((n : Q<#Nat) -> P n -> P (Q<#suc n)) -> (P Q<#zer) -> P n<,
+         : (n : Q.Nat) -> (P : Q.Nat => *) -> ((n : Q.Nat) => P n -> P (Q.suc n)) -> (P Q.zer) -> P n,
 
 
 -- In particular, we can also inductive computation.  In that case,
@@ -62,11 +62,11 @@
 -- That's fine, because we also have an operator for that: postfix ^.
 
 lift = \n -> n^
-     : Q#Nat -> Q#Nat^,
+     : Q.Nat -> Q.Nat^,
 
 plus 
- = \m n -> n^! (\_ -> Q#Nat) (\_ r -> Q#suc r) m 
- : Q#Nat -> Q#Nat -> Q#Nat,
+ = \m n -> n^! (\_ -> Q.Nat) (\_ r -> Q.suc r) m 
+ : Q.Nat -> Q.Nat -> Q.Nat,
 
 
 four = plus two two,
diff --git a/uAgda.cabal b/uAgda.cabal
--- a/uAgda.cabal
+++ b/uAgda.cabal
@@ -1,5 +1,5 @@
 name:           uAgda
-version:        1.0.0.2
+version:        1.1.0.0
 category:       Dependent Types
 synopsis:       A simplistic dependently-typed language with parametricity.
 description: