diff --git a/AbsSynToTerm.hs b/AbsSynToTerm.hs
--- a/AbsSynToTerm.hs
+++ b/AbsSynToTerm.hs
@@ -5,15 +5,17 @@
 import Terms 
 import qualified RawSyntax as A
 import RawSyntax (Identifier(..))
-import "transformers" Control.Monad.Trans.State (runStateT, StateT)
-import "transformers" Control.Monad.Trans.Reader
-import "transformers" Control.Monad.Trans.Error hiding (throwError)
-import "monads-fd" Control.Monad.Error
-import "monads-fd" Control.Monad.State
+import Control.Monad.Trans.State (runStateT, StateT)
+import Control.Monad.Trans.Reader
+import Control.Monad.Trans.Error hiding (throwError)
+import Control.Monad.Error
+import Control.Monad.State
 import Control.Applicative
 import Data.Functor.Identity
 import Data.List
 import Basics
+import Permutation
+import Data.List.Split
 
 type LocalEnv = [String]
 type GlobalEnv = ()
@@ -26,12 +28,12 @@
                   Left err -> error err
                   Right a -> fst a
 
-look :: Identifier -> Resolver Term
-look (ident@(Identifier (position,x))) = do
+look :: BitVector -> Identifier -> Resolver Term
+look bv (ident@(Identifier (position,x))) = do
   e <- ask
   case elemIndex x e of
     Nothing -> throwError ("unknown identifier: " ++ show ident)
-    Just x -> return $ Bound (Irr position) x
+    Just x -> return $ Bound (Irr position) bv x
 
 insertVar :: Identifier -> LocalEnv -> LocalEnv
 insertVar (Identifier (_pos,x)) e = x:e
@@ -40,52 +42,79 @@
 dummyVar = Identifier ((0,0),"_")
 
 
-manyDep binder a []     b = resolveTerm b
-manyDep binder a (x:xs) b = binder (Irr x) <$> resolveTerm a <*> local (insertVar x) (manyDep binder a xs b)
+manyDep o binder a []     b = resolveTerm b
+manyDep o binder a (x:xs) b = binder (Irr x) <$> resolveMulti o a <*> local (insertVar x) (manyDep o binder a xs b)
 
 manyLam :: [A.Bind] -> A.Exp -> Resolver Term
 manyLam []            b = resolveTerm b
-manyLam (A.NoBind (A.AIdent x):xs) b = Lam (Irr x) (Hole dummyPosition "") <$> local (insertVar x) (manyLam xs b)
-manyLam (A.Bind (A.AIdent x) t:xs) b = Lam (Irr x) <$> resolveTerm t <*> local (insertVar x) (manyLam xs b)
+manyLam (A.NoBind (A.AIdent x):xs) b = Lam Regu (Irr x) (unit $ Hole dummyPosition "") <$> local (insertVar x) (manyLam xs b)
+manyLam (A.Bind (A.AIdent x) (A.Colon o) t:xs) b = Lam (toBnd o) (Irr x) <$> resolveMulti (toBnd o) t <*> local (insertVar x) (manyLam xs b)
 
+toBnd ":" = Regu
+toBnd "::" = Pred
 
 extractVars :: A.Exp -> Resolver [Identifier]
 extractVars (A.EVar (A.AIdent i)) = return [i]
 extractVars (A.EApp (A.EVar (A.AIdent i)) rest) = (i:) <$> extractVars rest
 extractVars _ = throwError "list of variables expected"
 
+trailingHole Regu xs = xs
+trailingHole Pred xs = xs ++ [Hole (Irr (0,0)) "⊘"]
+
+resolveMulti :: Binder -> A.Exp -> Resolver (Cube Term)
+resolveMulti o t = do
+  xs <- trailingHole o <$> resolveMulti' t
+  case cubeFromList xs of
+    Just c -> return c
+    Nothing -> throwError "incomplete cube"
+
+resolveMulti' :: A.Exp -> Resolver [Term]
+resolveMulti' (A.EMulti xs) = mapM resolveTerm xs
+resolveMulti' x = (:[]) <$> resolveTerm x
+
 resolveTerm :: A.Exp -> Resolver Term
-resolveTerm (A.EDestr x (A.Natural n)) = Destroy (read n) <$> resolveTerm x
+resolveTerm (A.EMulti _) = throwError "expression list only allowed in some contexts"
+-- 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.EUp x) = Shift (Sort 1) <$> resolveTerm x
-resolveTerm (A.EVar (A.AIdent x)) = look x
-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
+resolveTerm (A.ESwap x (A.Permutation ('#':p))) = Swap (permFromString p) <$> resolveTerm x
+-- resolveTerm (A.EUp x) = Shift (Sort 1) <$> resolveTerm x
+resolveTerm (A.EVar (A.AIdent x)) = look nil x
+resolveTerm (A.EVarI (A.AIdent x) (A.Natural ix)) = look (bvFromString ix) x
+resolveTerm (A.ESet (A.Sort (p,c:s))) = return $ Star (Irr p) $ Sort level (read ('0':dim))
+   where (lev:dim:_) = splitOn "|" s ++ [""]
+         level = case c of
+                   '#' -> (-1)
+                   '*' -> read ('0':lev)
+resolveTerm (A.EProj x (A.AIdent (Identifier (_,field)))) = Proj True  <$> resolveTerm x <*> pure field
+resolveTerm (A.EExtr x (A.AIdent (Identifier (_,field)))) = Proj False <$> resolveTerm x <*> pure field
+resolveTerm (A.EApp f x)  = App Regu <$> resolveTerm f <*> resolveMulti Regu x
+resolveTerm (A.EAppP f x) = App Pred <$> resolveTerm f <*> resolveMulti Pred x
 resolveTerm (A.ESigma a b) = case a of
-   (A.EAnn vars a') -> do vs <- extractVars vars
-                          manyDep Sigma a' vs b
+   (A.EAnn vars colon a') -> do
+     vs <- extractVars vars
+     manyDep Regu (\i a b -> Sigma i (a!?nil) b) a' vs b
                           
    (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
-   (A.EAnn vars a') -> do vs <- extractVars vars
-                          manyDep (Pi o) a' vs b
+resolveTerm (A.EPi a (A.Arrow arrow) b) = case a of
+   (A.EAnn vars (A.Colon colon) a') -> do 
+     vs <- extractVars vars
+     manyDep o (Pi o) a' vs b
                           
    (A.EAbs _ _ _) -> throwError "cannot use lambda for type"
-   _              -> 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
+   _            -> Pi o (Irr dummyVar) <$> resolveMulti o a <*> local (insertVar dummyVar) (resolveTerm b)
+
+ where o = case arrow of
+             "->" -> Regu
+             "=>" -> Pred
+
+resolveTerm (A.EAbs ids _ 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) = 
    Pair (Irr i) <$> 
    (Ann <$> (OfParam (Irr i) <$> resolveTerm e) <*> resolveTerm t)
    <*> local (insertVar i) (resolveTerm rest)
 
-resolveTerm (A.EAnn e1 e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2
+resolveTerm (A.EAnn e1 _colon_ e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2
 
diff --git a/Basics.hs b/Basics.hs
--- a/Basics.hs
+++ b/Basics.hs
@@ -4,12 +4,12 @@
         module Control.Applicative,
         Irr(..), 
         Sort(..),
-        above, oneLev, zero,
         Ident, Identifier(..), DisplayContext,
         Position, dummyPosition, identPosition, 
         isDummyId, modId, synthId, dummyId, idString,
-        Relevance(..), arrow, colon,
-        Lattice(..)) where
+        Binder(..), arrow, colon, cross, appl, comm,
+        Lattice(..), above,
+        module Cubes) where
 
 import Display
 import qualified RawSyntax as A
@@ -17,16 +17,13 @@
 import Control.Applicative
 import Data.Monoid
 import Data.Sequence (Seq)
-
-
-(<>) :: Monoid a => a -> a -> a
-(<>) = mappend
+import Cubes
 
 -----------
 -- Irr
 
 newtype Irr a = Irr {fromIrr :: a}
-    deriving Show
+    deriving (Show,Monoid)
 
 instance Eq (Irr a) where
     x == y = True
@@ -39,14 +36,19 @@
 instance Pretty Identifier where
     pretty (Identifier (_,x)) = text x
 
+instance Monoid Identifier where
+  Identifier (p,t1) `mappend` Identifier (_,t2) = Identifier (p, t1 <> t2)
+  mempty = Identifier (fromIrr dummyPosition,"")
 
 type Ident = Irr Identifier
 
-isDummyId (Irr (Identifier (_,"_"))) = True
-isDummyId _ = False 
+isDummyIdS ('_':x) = True
+isDummyIdS _ = False
 
+isDummyId (Irr (Identifier (_,xs))) = isDummyIdS xs
+
 synthId :: String -> Ident
-synthId x = Irr (Identifier (fromIrr $ dummyPosition,x))
+synthId x = Irr (Identifier (fromIrr dummyPosition,x))
 
 dummyId = synthId "_"
 
@@ -67,51 +69,76 @@
 modId :: (String -> String) -> Ident -> Ident
 modId f (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,f x)))
 
-------------------
+-------
+-----------
 -- Sort
 
-instance Lattice Int where
-    (⊔) = max
 
-data Relevance = Re | Ir
-  deriving (Enum,Ord,Eq,Show)
+instance Lattice Int where -- Lattice is a misnomer here.
+    x ⊔ (-1) = (-1)
+    x ⊔ y = max x y
 
+data Binder = Pred | Regu
+  deriving (Ord,Eq,Show)
+                      
 class Lattice a where
     (⊔) :: a -> a -> a
 
+-- instance Ord Sort where
+--  compare (Sort x) (Sort y) = compare x y
 
-newtype Sort = Sort {sortLevel :: Int}
-  deriving (Eq,Num)
+data Sort = Sort {sortLevel :: Int,
+                  sortDimension :: Int}
+  deriving (Eq)
 
 instance Lattice Sort where
-  x ⊔ Sort (-1) = Sort (-1) -- is this a lattice? 
-  Sort x ⊔ Sort y = Sort (x ⊔ y)
+  Sort x m ⊔ Sort y n  = Sort (x ⊔ y) (min m n)
+  
 
 instance Show Sort where
     show s = render (pretty s)
 
 
-instance Pretty Relevance where
-    pretty (Re) = mempty
-    pretty (Ir) = "÷"
+instance Pretty Binder where
+    pretty = colon
 
 instance Pretty Sort where
-    pretty s = prettyLev s
-    
+    pretty (Sort s d) = showLev <> showDim
+
+     where showDim = case d of
+                       0 -> mempty
+                       _ -> superscriptPretty d
+           showLev = case s of
+                       (-1) -> "□"
+                       0    -> star
+                       l    -> star <> subscriptPretty l
+                       
+
+above (Sort s n) = Sort (s+1) n    
+
 star = "∗" -- ⋆★*∗
 
-prettyLev (Sort (-1) ) = "□"
-prettyLev (Sort 0    ) = star <> mempty
-prettyLev (Sort l    ) = star <> subscriptPretty l
 
-above (Sort l) = Sort (l + 1)
-oneLev = Sort 1
+arrow, colon, cross, comm, appl :: Binder -> Doc
 
-zero = Sort 0
+arrow Pred = "⇛"
+arrow Regu = "→"
+-- ⟴
 
-arrow Ir = "⇒"
-arrow Re = "→"
+colon Regu = text ":"
+colon Pred = text "::"
+-- :⋮∷∴∵
 
-colon Ir = text "÷"                  
-colon Re = text "∶"                  
+
+cross Regu = "×" 
+cross Pred  = "⋇" 
+-- ⊗⊠
+-- ⚔⤬⤫⨯
+
+comm Pred = "⍮"
+comm Regu = ","
+
+
+appl Regu = "" 
+appl Pred = "· " 
 
diff --git a/Display.hs b/Display.hs
--- a/Display.hs
+++ b/Display.hs
@@ -1,22 +1,26 @@
 {-# LANGUAGE PackageImports, GADTs, KindSignatures, StandaloneDeriving, EmptyDataDecls, FlexibleInstances, OverloadedStrings #-}
 
 module Display (Pretty(..), Doc, ($$), (<+>), text, hang, vcat, parensIf, sep, comma, nest, parens,
-                subscriptPretty, superscriptPretty, subscriptShow, render) where
+                subscriptPretty, superscriptPretty, subscriptShow, punctuate, render, module Data.Monoid, (Display.<>)) where
 
 import GHC.Exts( IsString(..) )
 
 import Prelude hiding (length, reverse)
-import Text.PrettyPrint.HughesPJ 
+import Text.PrettyPrint.HughesPJ hiding ((<>))
+import qualified Text.PrettyPrint.HughesPJ 
 import Numeric (showIntAtBase)
 import Control.Arrow (second)
-import "monads-fd" Control.Monad.Error
+import Control.Monad.Error
 import Data.Monoid
 import Data.Sequence hiding (empty)
 import Data.Foldable
 
+(<>) :: Monoid a => a -> a -> a
+(<>) = mappend
+
 instance Monoid Doc where
     mempty = empty
-    mappend = (<>)
+    mappend = (Text.PrettyPrint.HughesPJ.<>)
 
 class Pretty a where
     pretty :: a -> Doc
@@ -24,6 +28,9 @@
 instance Pretty x => Pretty [x] where
     pretty x = brackets $ sep $ punctuate comma (map pretty x)
 
+instance (Pretty a,Pretty b) => Pretty (a,b) where
+    pretty (a,b) = parens $ pretty a <> comma <+> pretty b 
+
 instance IsString Doc where
     fromString = text
 
@@ -44,8 +51,6 @@
 
 subscriptShow :: Int -> String
 subscriptShow     = scriptShow "-₀₁₂₃₄₅₆₇₈₉"
-
-
 
 parensIf :: Bool -> Doc -> Doc
 parensIf True  = parens
diff --git a/Main.hs b/Main.hs
--- a/Main.hs
+++ b/Main.hs
@@ -23,11 +23,11 @@
 import qualified Data.Sequence as S
 
 
-import Language.LBNF(Err(..))
+import Language.LBNF.Runtime (ParseMonad(..))
 
 -- type ParseFun a = [Token] -> Err a
 
-myLLexer = myLexer
+myLLexer = tokens -- myLexer
 
 type Verbosity = Int
 
@@ -61,7 +61,7 @@
     [] -> return ()
     _ -> putStrV 0 $ vcat info -- display constraints, etc.
   case checked of
-    Right (a,b) -> do 
+    Right (a,b,_) -> do 
        putStrV 0 $ "nf =" <+> pretty a
        putStrV 0 $ "ty =" <+> pretty b
 {-
diff --git a/Normal.hs b/Normal.hs
--- a/Normal.hs
+++ b/Normal.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, KindSignatures, OverloadedStrings, EmptyDataDecls, StandaloneDeriving, TypeSynonymInstances, TypeFamilies, MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs, KindSignatures, OverloadedStrings, EmptyDataDecls, StandaloneDeriving, TypeSynonymInstances, TypeFamilies, MultiParamTypeClasses, ViewPatterns, RankNTypes #-}
 module Normal where
 
 import Prelude hiding (length,elem,foldl)
@@ -8,6 +8,8 @@
 import Control.Arrow (first, second)
 import Data.Sequence hiding (zip,replicate,reverse)
 import Options
+import qualified Data.List as L
+import Permutation
 
 data No
 data Ne
@@ -18,42 +20,39 @@
 type Variable = Term Va
 type NF' = (NF, NF) -- value, type.
 
+data Role = Index | Thing deriving (Eq, Show)
+
+showRole Index = "?"
+showRole Thing = "!"
+
 data Term n :: * where
      Neu :: Neutral -> NF
      Var :: Variable -> Neutral
      
      Star :: Sort -> NF     
      
-     Pi  :: Relevance -> Ident -> NF -> NF -> NF
-     Lam :: Relevance -> Ident -> NF -> NF -> NF 
-     App :: Relevance -> Neutral -> NF -> Neutral -- The sort is that of the argument.
+     Pi  :: Binder -> Ident -> Cube NF -> NF -> NF
+     Lam :: Binder -> Ident -> Cube NF -> NF -> NF 
+     App :: Binder -> Neutral -> Cube 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 (only needed for
+     Sigma :: Binder -> Ident -> NF -> NF -> NF
+     Pair  :: Binder -> Ident -> NF -> NF -> NF  -- Pair does not bind any variable.
+     Proj  :: Binder -> -- ^ 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 
+              Ident -> Neutral 
      
      
-     OfParam :: Ident -> NF -> Neutral
+     -- OfParam :: Ident -> NF -> Neutral
 
-     Destr :: Int -> Variable -> Variable -- argument: depth where destruction occurs.
-     Param :: Variable -> Variable 
-     V :: Sort -> Int -> Variable -- shift, deBruijn 
+     -- Destr :: Int -> Variable -> Variable -- argument: depth where destruction occurs.
+     Swap :: Permutation -> Variable -> Variable
+     Param :: Role {-TODO: Maybe the swap should be merged into the role -} -> Variable -> Variable 
+     V :: BitVector -> 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]
+type Subst = [Cube NF]
 
 deriving instance Eq (Term n)
 deriving instance Show (Term n)
@@ -61,16 +60,16 @@
 var :: Int -> NF
 var x = Neu $ var' x
 
-var'' = V (Sort 0)
+var'' = V nil
 
-var' x = Var $ V (Sort 0) x
+var' x = Var $ V nil x
 
 
 -- | Hereditary substitution
-subst0 :: NF -> NF -> NF
-subst0 u = subst (u:map (var) [0..])  
+subst0 :: Cube NF -> NF -> NF
+subst0 u = subst (u:map (unit . var) [0..])  
 
-showShift (Sort l) = replicate l '^' 
+hole = Neu . Var . Hole
 
 subst :: Subst -> Term n -> NF
 subst f t = case t of
@@ -79,144 +78,65 @@
   
   Star x -> Star x
   
-  Lam o i ty bo -> Lam o i (s ty) (s' bo)
+  Lam o i ty bo -> Lam o i (fmap 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)
+  Pi o i a b -> Pi o i (fmap 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)
+  (App o a b) -> app o (s a) (fmap s b)
   (Proj o x k f) -> proj o (s x) k f
 
-  OfParam i x -> Neu (OfParam i (s x))
+--  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 x -> param (s x)
- where s' = subst (var 0 : map wk f)
+--  Destr d x -> destroy d (s x)
+  Hole x -> hole x
+  V bv x -> let fx = f!!x in
+            case cubeElems fx of 
+              [Neu (Var (V bv' y))] -> Neu $ Var $ V (bv' <> bv) y
+              _ | dim (f !! x) /= bvDim bv -> hole $ "error: variable access dim " ++ show (bvDim bv) ++ " expected " ++ show (dim (f!!x))
+              _  -> (f !! x) !? bv 
+  Param r x -> param r (s x)
+  Swap q x -> swap q (s x)
+ where s,s' :: forall n. Term n -> NF
+       s' = subst (unit (var 0) : map (cmap 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)
-  Var x -> Var (s x)
-  
-  Star x -> Star x
-  
-  Lam o i ty bo -> Lam o i (s ty) (s' o bo)
-  (Pair o i x y) -> Pair o i (s x) (s y)
-  Pi o i a b -> Pi o i (s a) (s' o b)
-  Sigma o i a b -> Sigma o i (s a) (s' o  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)
-  
-  Hole x -> Hole x
-  V s x -> shift s (fst $ f !! x)
-  Param (V s x) -> shift s (snd $ f !! x)
-  Param x -> Param (s x)
- where s' o = subst' (p f)
-       s  = subst' f
-       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 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 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 (modId (++showShift d) i) (s x)
-
-  Hole x -> Hole 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
-       s' = shift' (1 + n) d
-
-shift = shift' 0
-
 -----------------------------
 -- Hereditary operations
-  
-app :: Relevance -> NF -> NF -> NF 
+
+app :: Binder -> NF -> Cube NF -> NF 
+app Pred x u | dim u == 0 = x
 app _ (Lam _ i _ bo) u = subst0 u bo
 app o (Neu n)      u = Neu (App o n u)
 
-proj :: Relevance -> NF -> Bool -> Irr String -> NF
+-- TODO: merge App Pred's
+
+proj :: Binder -> NF -> Bool -> Ident -> NF
 proj _ (Pair _ _ x y) True f = x
 proj _ (Pair _ _ x y) False f = y
 proj o (Neu x) k f = Neu (Proj o x k f)
 
 
 wkn :: Int -> NF -> NF
-wkn n = subst (map var [n..])
+wkn = wkdn 0
 
 wkdn :: Int -> Int -> NF -> NF
-wkdn d n = subst (map var [0..d-1] ++ map var [d+n..])
+wkdn d n = subst (map (unit . var) [0..d-1] ++ map (unit . var) [d+n..])
 
 wk = wkn 1
-str = subst0 (Neu $ Var $ Hole "str: oops!")
+str = strn 1
+strn n = subst (replicate n (unit $ Neu $ Var $ Hole "str: oops!") ++ map (unit . var) [0..])
 
 wkv :: Int -> Variable -> Variable
-wkv n (Param x) = Param (wkv n x)
+wkv n (Param r x) = Param r (wkv n x)
+wkv n (Swap q x) = Swap q (wkv n x)
 wkv n (V s x) = V s (x + n)
 wkv n (Hole x) = Hole x
 
-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
+param :: Role -> NF -> NF
+param r = transNF r noAction
 
 
 -----------------------------------
@@ -224,206 +144,236 @@
 
 dec xs = [ x - 1 | x <- xs, x > 0]
 
+allFreeVars :: Cube (Term n) -> [Int]
+allFreeVars = L.concat . fmap freeVars . cubeElems
+
 freeVars :: Term n -> [Int]
 freeVars (Var x) = freeVars x
-freeVars (Destr _ x) = freeVars x
+--freeVars (Destr _ x) = freeVars x
 freeVars (Neu x) = freeVars x
-freeVars (Pi _ _ a b) = freeVars a <> (dec $ freeVars b)
+freeVars (Pi _ _ a b) = allFreeVars a <> (dec $ freeVars b)
 freeVars (Sigma _ _ a b) = freeVars a <> (dec $ freeVars b)
 freeVars (V _ x) = [x]
-freeVars (App _ a b) = freeVars a <> freeVars b
-freeVars (Lam _ _ ty b) = freeVars ty <> (dec $ freeVars b)
+freeVars (App _ a b) = freeVars a <> allFreeVars b
+freeVars (Lam _ _ ty b) = allFreeVars ty <> (dec $ freeVars b)
 freeVars (Star _) = mempty
 freeVars (Hole _) = mempty
 freeVars (Pair _ _ x y) = freeVars x <> freeVars y
 freeVars (Proj _ x _ _) = freeVars x
-freeVars (Param x) = freeVars x
-freeVars (OfParam _ x) = freeVars x
+freeVars (Param _ x) = freeVars x
+freeVars (Swap _ x) = freeVars x
+-- freeVars (OfParam _ x) = freeVars x
 
 iOccursIn :: Int -> Term n -> Bool
 iOccursIn x t = x `elem` (freeVars t)
 
+allocName :: DisplayContext -> Ident -> Ident
+allocName g s 
+  | fromIrr s `elem` (fmap fromIrr g) = allocName g (modId (++ "'") s)
+  | otherwise = s
+
+printIndex :: DisplayContext -> Int -> Doc
+printIndex ii k 
+  | k < 0 || k >= length ii  = text "<deBrujn index" <+> pretty k <+> text "out of range>"
+  | otherwise = pretty (ii `index` k)
+
 cPrint :: Int -> DisplayContext -> Term n -> Doc
+cPrint p ii (Swap q x) = cPrint p ii x <> "#" <> pretty q
 cPrint p ii (Var x) = cPrint p ii x
 cPrint p ii (Neu x) = cPrint p ii x
-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 p ii (Param r x) = cPrint p ii x <> text (showRole r)
+-- 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 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 = 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 (V bv k) = printIndex ii k <> (mconcat $ map subscriptPretty $ map b2i $ bits bv)
+cPrint p ii (Proj o x k (Irr f))     = cPrint p ii x <> (if k then "." <> pretty f else "/")
+cPrint p ii t@(App _ _ _)     = parensIf (p > 3) (cPrint 3 ii fct <+> sep [appl o <> printCube o 4 ii a | (o,a) <- args]) 
+    where (fct,args) = nestedApp 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 p ii (Pair o name x y) = parensIf (p > (-1)) (sep [pretty name <+> text "=" <+> cPrint 0 ii x <> comm o,
                                                           cPrint (-1) ii y])
 
-cross Ir = "⤬" -- ⚔⤬⤫⨯
-cross Re = "×" -- ×⨯
-
-nestedPis  :: NF -> ([(Ident,Bool,NF,Relevance)], NF)
+nestedPis  :: NF -> ([(Ident,Bool,Cube NF,Binder)], NF)
 nestedPis (Pi o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedPis b)
 nestedPis x = ([],x)
 
-nestedSigmas  :: NF -> ([(Ident,Bool,NF,Relevance)], NF)
-nestedSigmas (Sigma o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedSigmas b)
+nestedSigmas  :: NF -> ([(Ident,Bool,Cube NF,Binder)], NF)
+nestedSigmas (Sigma o i a b) = (first ([(i,0 `iOccursIn` b,unit a,o)] ++)) (nestedSigmas b)
 nestedSigmas x = ([],x)
 
-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 :: (Binder -> Doc) -> DisplayContext -> Seq Doc -> ([(Ident,Bool,Cube NF,Binder)], NF) -> Doc
+printBinders sep ii xs (((x,occurs,a,o):pis),b) = printBinders sep (i <| ii) (xs |> (printBind' ii i occurs a o <+> sep o)) (pis,b)
+        where i = allocName ii x
 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 <+> colon o <+> cPrint 0 ii ty)) c
+nestedLams ii xs (Lam o x ty c) = nestedLams (i <| ii) (xs |> parens (pretty i <+> colon o <+> printCube o 0 ii ty)) c
+                                  where i = allocName ii x
 nestedLams ii xs t         = (text "\\ " <> (sep $ toList $ (xs |> "->")) <+> nest 3 (cPrint 0 ii t))
 
+printCube :: Binder -> Int -> DisplayContext -> Cube (Term n) -> Doc
+printCube o p ii d | dim d == 0 = cPrint p ii (d !? nil)
+                   | otherwise = "{" <> sep (punctuate ";" [(if showIndices options then pretty i <> "↦" else mempty ) <>
+                                                            cPrint 0 ii x | (i,x) <- adjust $ cubeAssocs d]) <> "}"
+ where adjust = case o of
+                  Pred -> init
+                  Regu -> id
+
 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
+                  True -> parens $ pretty name <+> colon o <+> printCube o 0 ii d
+                  False -> printCube o 2 ii d
                   
-nestedApp :: Neutral -> (Neutral,[(Relevance, NF)])
+nestedApp :: Neutral -> (Neutral,[(Binder, Cube 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)
 
 
 instance Pretty (Term n) where
     pretty = prettyTerm mempty
 
+type Action = [(NF,NF)] -- TODO: use Seq
 
-mv :: Int -> Int -> Int
-mv d x | x < d     = (arity + 1) * x + idx
-       | otherwise = (x - d) + (arity + 1) * d
-                     -- x + arity * d
+paramv :: BitVector -> Role -> Int -> NF
+paramv bv Thing x = Neu $ Var $ Param Thing $ V bv x
+paramv bv Index x = Neu $ Var $               V bv x
 
-mv' :: Int -> Int -> (Variable, Variable)
-mv' d x | x < d     = let v = (arity + 1) * x 
-                      in (V zero $ v + idx, V zero v)
-        | otherwise = let v = V zero $ (x - d) + (arity + 1) * d 
-                      in (v, Hole "does not appear!")
-                          -- Param evil v)
+noAction = []
+wka = map (both wk)
+addAct1 as = (Neu $ Var $ V (zeros 1) 0, Neu $ Var $ V (ones 1) 0) : wka as
+addAct2 as = error "accessing crap" : wka as
 
--- 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))
+recVarName = synthId "°"
 
+scopeCheck c k | 0 `iOccursIn` c = error "swapTy: improperly scoped Sigma"
+               | otherwise = c
 
--- renam :: Int -> Int -> NF -> NF
--- renam d idx = id -- subst [var $ mv d $ x | x <- [0..]] 
+swap q = swapNF q 0
 
--- renam' d = subst' (map (mv' d) [0..])
+swapV :: Permutation  -> Variable -> Variable
+swapV q x | isIdentity q = x
+swapV q (V bv x) = Swap q $ V bv x
 
-re :: Ident -> Ident
-re (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,x++"°")))
+swapV q (Swap q' v) = swapV (q `after` q') v 
+swapV q v@(Param _ _) = power n (Param Thing) $ swapV (simplifyPerm n q) x
+    where (n,x) = countParam v
+swapV q (Hole s) = Hole (s ++ "#")
+swapV q x = Swap q x
 
-arity, idx :: Int
-arity = 1
-idx = 1
+power 0 f = id
+power n f = f . power (n-1) f
 
+(f *** g) (x,y) = (f x, g y)  
 
--- | Transform a term to its relational interpretation
-transV    :: Int -> Variable -> Variable
+-- FIXME: what about the role=Index? There should not be a (Param Index) in the syntax.
+countParam (Param _ x) = ((1+) *** id) (countParam x)
+countParam x = (0,x)
 
-transV  d (V o x) = Param $ V o x
-transV  d (Param x) = Param $ transV d x
-transV  d (Hole s) = Hole (s ++ "!")
+fullVarCube x = full (\i -> Neu $ Var $ V i x) 
 
-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)
+swapSubst :: Permutation -> NF -> NF
+swapSubst q = subst $ (apply (invert q) $ fullVarCube 0 $ permLength q) : map (unit . var) [1..]
 
-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
+swapNe :: Permutation -> Int -> Neutral -> Neutral
+swapNe q d (Var v) = Var $ swapV q v
+swapNe q d (App o f a) = App o (swapNe q d f) (swapCube q d a)
+swapNe q d (Proj o x k f) = Proj o (swapNe q d x) k f 
 
-trans'  d ty = Lam Ir (synthId "z") ty (zerInRel d ty)
+swapCube :: Permutation -> Int -> Cube NF -> Cube NF
+swapCube q0 d c = apply q . subAppl q (\p -> swapNF p d) $ c
+  where q = reducePerm q0 (dim c) -- FIXME: reduction should never be necessary
 
--- | Build the relation x ∈ ⟦ty⟧. (where 'x' is 0; but not bound in 'ty'.)
-zerInRel d ty = inTrans (d + 1) (wk ty) (var 0)
+swapBinder :: Permutation -> Int -> Cube NF -> Cube NF
+swapBinder = swapCube
 
--- | 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.
+swapNF :: Permutation -> Int -> NF -> NF
+swapNF q d (Neu v) = Neu $ swapNe q d v
+swapNF q d (Star x) = Star x
+-- swapNF q d (Pair  o i a b) = Pair  o i (swapBinder q d a) (swapNF q d b)
+swapNF q d (Lam   o i a b) = Lam   o i (swapBinder q d a) (swapSubst q $ swapNF q (d+1) b)
+swapNF q d (Pi    o i a b) = Pi    o i (swapBinder q d a) (swapSubst q $ swapNF q (d+1) b)
+-- swapNF q d (Sigma o i a b) = Sigma o i (swapBinder q d a) (swapNF q (d+1) b)
 
+getVar :: Variable -> Int
+getVar (Param _ x) = getVar x
+getVar (V _ x) = x
+getVar (Hole x) = (-1)
+getVar (Swap _ x) = getVar x
 
-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 z = app Ir (transNF d t) z
+getDepth :: Variable -> Int
+getDepth (Param _ x) = 1 + getDepth x
+getDepth (V _ x) = 0
+getDepth (Hole x) = 0
+getDepth (Swap _ x) = getDepth x
 
 
--- | 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 Re i a rest = binder Ir i a $ 
-                                 binder Re (re i) (zerInRel d a) $ 
-                                 subst2d 2 (var 1,var 0) $ wkn 2 rest
+-- | Transform a term to its relational interpretation
+transV :: Role -> Action -> Variable -> NF
+transV Thing d (Swap q x) = swap (extendPerm q) $ transV Thing d x
+transV Index d (Swap q x) = swap q $ transV Index d x
+transV r d (V bv x) | x < L.length d = Neu $ Var $ case r of Thing -> V (bv <> ones 1) x; Index -> V (bv <> zeros 1) x
+                    | otherwise = paramv bv r x
+-- transV r [] (Param r' x) = Neu $ Var $ Param r $ Param r' x 
+transV r d  (Param r' x) 
+            | getVar x < L.length d = maybeSwap $ param r' $ transV r d x -- the inner variable is known; go through 
+            | otherwise = Neu $ Var $ maybeParam $ Param r' x -- the inner variable is not known ~> stop here and forget about other variables
+              where maybeSwap = if r == Thing then swap (swap2 (n+2) (n+1) n) else id -- add a swap if we are doing "proper" parametricity
+                    maybeParam = if r == Thing then Param r else id -- keep only "proper" parametricity
+                    n = getDepth x
 
-transBind d binder Ir i a rest = binder Ir i a rest
+transV r d  (Hole s) = Neu $ Var $ Hole (s ++ showRole r)
 
--- Invariant: the whole term is not destroyed.
-destroy :: Int -> Term n -> Term n
-destroy d t = case t of
-  Var x -> Var $ pr x
-  Neu x -> Neu $ pr x
+transNe :: Role -> Action -> Neutral -> NF
+transNe r d (Var v)      = transV r d v
+transNe Thing d (App o f a)  = app o (transNe Thing d f) (extend d a)
+transNe Index d (App o f a)  = app o (transNe Index d f) (cmap (transNF Index d) a)
+transNe r d (Proj o x k f) = proj o (transNe r d x) k f
 
-  V o x -> V o x
-  Hole x -> Hole x
-  Destr d' t -> destroy (min d d') t -- coalesce
-  Param x | d == 0 -> x
-          | otherwise -> Destr d $ Param x 
+isLam :: Term n -> Bool
+isLam (Lam _ _ _ _) = True
+isLam _ = False
 
-  (Star o) -> Star o
-  (Pi o i a b)    -> mb Pi    o i a b 
-  (Sigma o i a b) -> mb Sigma o i a b 
-  (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' o a) (pr b) 
-  (App o a b)  -> case isDestroyed o of
-                   True -> pr a
-                   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 -- FIXME: hmmm, here we should probably use pr' (symmetry)
-  (OfParam n x) -> OfParam (modId (++ "%" ++ show d) n) $ pr x
-  
- where 
-   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' o  a) (pr b)
-   pr x = destroy d x
-   pr' Ir x = destroy (d-1) x
-   pr' Re x = pr x
+transNF :: Role -> Action -> NF -> NF
+transNF r d (Neu v) = transNe r d v
+transNF r d p@(Lam Pred i ty bo) = Lam Pred i (updateCube ix p $ extend d ty) (inTrans (addAct1 d) bo (Neu $ Var $ V ix 0))
+    where ix = ones (dim ty) <> zeros 1
+transNF r d (Lam o i ty bo)    = Lam o i (extend d ty) (transNF r (addAct1 d) bo)
+transNF r d (Pair o i x y)     = Pair o i (transNF r d x) (transNF r d y) 
+transNF Index d (Star x)       = Star x
+transNF Index d (Pi o i a b)    = Pi    o i (cmap (transNF Index d) a) (transNF Index d b)
+transNF Index d (Sigma o i a b) = Sigma o i ((transNF Index d) a) (transNF Index d b)
+transNF r d ty@(Star  _)       = trans' r d ty
+transNF r d ty@(Pi    _ _ _ _) = trans' r d ty
+transNF r d ty@(Sigma _ _ _ _) = trans' r d ty
+
+extend  d a  = cubeCons (cmap (transNF Index d) a) (cmap (transNF Thing d) a) 
+
+trans' :: Role -> Action -> NF -> NF
+trans' Index d ty = error $ "trans': Index: wrong arg: " ++ show ty
+trans' Thing d ty = Lam Pred (synthId "z") (pair (transNF Index d ty) (hole "⊘")) (zerInRel d ty)
+
+-- | Build the relation x ∈ ⟦ty⟧. (where 'x' is 0; but not bound in 'ty'.)
+zerInRel :: Action -> NF -> NF
+zerInRel d ty = inTrans (addAct2 d) (wk ty) (Neu $ Var $ V (zeros 1) 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 :: Action -> NF -> NF -> NF
+inTrans d (Neu (App Pred f a))  z = app Pred (transNe Thing d f) (updateCube (ones (dim a) <> zeros 1) z (extend d a))
+inTrans d (Star (Sort l δ))       z = (Pi Pred dummyId (pair z (hole "⊘")) (Star $ Sort l (δ+1)))
+inTrans d (Pi    Pred i a (Star (Sort l δ))) z = Pi Pred i (updateCube (ones (dim a) <> zeros 1) z (extend d a)) (Star $ Sort l (δ+1))
+inTrans d (Pi    o i a b) z = Pi o i (extend d a) (inTrans (addAct1 d) b (app o (wk z) (unit $ transNF Index (addAct1 d) $ var 0)))
+inTrans d (Sigma o i a b) z = Sigma o i (inTrans d a (proj o z True i))
+                                        (inTrans ((wk $ proj o z True i,var 0):wka d) b (proj o (wk z) False i))
+inTrans d ty z = app Pred (transNF Thing d ty) (pair z (hole "⊘"))
 
diff --git a/Options.hs b/Options.hs
--- a/Options.hs
+++ b/Options.hs
@@ -12,19 +12,22 @@
 data Args = 
   Args {verb :: Int,
         typeSystem :: TypeSystem,
-        showSorts :: Bool,
+        showIndices :: Bool,
         collapseRelevance :: Bool,
+        ignoreBinder :: Bool,
         files :: [String]
         } 
   deriving (Show, Data, Typeable)
            
 sample = cmdArgsMode $ 
          Args { verb = 0 &= help "verbosity" &= opt (0 :: Int),
-                typeSystem = enum [Predicative &= name "P" &= help "Agda (Predicative)", 
-                                   CCω &= name "I" &= help "CCω (Impredicative)"]
+                typeSystem = enum [CCω &= name "I" &= help "CCω (Impredicative)",
+                                   Predicative &= name "P" &= help "Martin-Löf (Predicative)"
+                                   ]
                                , -- &= opt (0 :: Int),
-                showSorts = False &= help "display sort annotations in normal forms",
+                showIndices = False &= help "show indices in cubes",
                 collapseRelevance  = False &= help "! (param) does not generate new relevance levels.",
+                ignoreBinder  = False &= help "ignore binder annotations.",
                 files = [] &= args &= typFile
               }
          
diff --git a/RawSyntax.hs b/RawSyntax.hs
--- a/RawSyntax.hs
+++ b/RawSyntax.hs
@@ -1,51 +1,61 @@
-{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE QuasiQuotes, TemplateHaskell #-}
 
 module RawSyntax where
 
 import Language.LBNF
 
-compile [$cf|
+bnfc [$lbnf|
 
 
 comment "--" ;
 comment "{-" "-}" ;
 
+token Colon (':')+ ;
+token Commas ','+ ;
+token Cross ';'+ ;
+
+token Natural digit+;
+-- token Index (('0'|'1')+);
+token Permutation '#' digit+;
+token Arrow {"->"}|{"=>"};
+
+position token Identifier ('!'|'['|']'|letter|'_'|'\'')(('*'|'['|']'|letter|digit|'-'|'_'|'\'')*) ;
+position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;
+
+position token Sort ('#' | '*' (digit*)) ('|' (digit+))?;
+
+
+EMulti.  Exp6 ::= "{" [Exp] "}" ;
 EHole.   Exp6 ::= Hole ;
 EVar.    Exp6 ::= AIdent ;
+EVarI.   Exp6 ::= AIdent Natural;
 ESet.    Exp6 ::= Sort ;
 EParam.  Exp4 ::= Exp4 "!";
+ESwap.   Exp4 ::= Exp4 Permutation;
 EUp.     Exp4 ::= Exp4 "^";
--- ELeft.   Exp4 ::= Exp4 "<";
-EDestr.  Exp4 ::= Exp4 "%" Natural ;
+-- EDestr.  Exp4 ::= Exp4 "%" Natural ;
 EProj.   Exp4 ::= Exp4 "." AIdent ;
 EExtr.   Exp4 ::= Exp4 "/" AIdent ;
 EApp.    Exp3 ::= Exp3 Exp4 ;
+EAppP.   Exp3 ::= Exp3 "@" Exp4 ;
 EPi.     Exp2  ::= Exp3 Arrow Exp2 ;
-ESigma.  Exp2  ::= Exp3 ";" Exp2 ;
+ESigma.  Exp2  ::= Exp3 ";;" Exp2 ;
 EAbs.    Exp2  ::= "\\" [Bind] Arrow Exp2 ;
-EAnn.    Exp1 ::= Exp2 ":" Exp1 ;
+EAnn.    Exp1 ::= Exp2 Colon Exp1 ;
 EPair.   Exp  ::= Decl "," Exp ;
 
 coercions Exp 6 ;
+separator Exp ";" ;
 
 Decl. Decl ::= AIdent "=" Exp1 ;
-PDecl. Decl ::= "param" AIdent "=" Exp1 "::" Exp2;
-terminator AIdent "" ;
-terminator Decl ";" ;
-
-token Arrow  ('-' '>') | ('=' '>') ;
+PDecl. Decl ::= "param" AIdent "=" Exp1 "ofErasedType" Exp2;
+-- terminator Decl ";" ;
 
 NoBind. Bind   ::= AIdent ; 
-Bind.   Bind   ::= "(" AIdent ":" Exp ")" ;
+Bind.   Bind   ::= "(" AIdent Colon Exp ")" ;
 AIdent. AIdent ::= Identifier ;
-terminator Bind "" ;
 
-token Natural digit+;
-
-position token Identifier ('!'|'['|']'|letter|digit|'-'|'_'|'\'')(('*'|'['|']'|letter|digit|'-'|'_'|'\'')*) ;
-
-position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;
+terminator Bind "" ;
 
-position token Sort ('#' | '*' (digit*));
 
 |]
diff --git a/Terms.hs b/Terms.hs
--- a/Terms.hs
+++ b/Terms.hs
@@ -16,21 +16,19 @@
 import Data.Sequence hiding (zip,replicate,reverse)
 import Control.Arrow (second)
 import Data.Foldable
+import Permutation
 
 data Term :: * where
      Hole :: Irr Position -> String -> Term -- placeholder
      Star :: Irr Position -> Sort -> Term -- sort
-     Bound :: Irr Position -> Int -> Term -- variable
-     Pi :: Relevance -> Ident -> Term -> Term -> Term 
+     Bound :: Irr Position -> BitVector -> Int -> Term -- variable
+     Pi :: Binder -> Ident -> Cube Term -> Term -> Term 
      Sigma :: Ident -> Term -> Term -> Term
-     Lam :: Ident -> Term -> Term -> Term 
+     Lam :: Binder -> Ident -> Cube Term -> Term -> Term 
      Pair :: Ident -> Term -> Term -> Term 
-     (:$:) :: Term -> Term -> Term
-     -- 1st projection.
-     Proj :: Term -> String -> Term     
-     -- 2nd projection.     FIXME: remove
-     Extr :: Term -> String -> Term 
-     
+     App :: Binder -> Term -> Cube Term -> Term
+     Proj :: Bool {- 1st projection? -} -> Term -> String -> Term     
+
      -- term such that its relational interpretation is its argument.
      OfParam :: Ident -> Term -> Term 
      
@@ -43,21 +41,22 @@
      -- relational interpretations and world destruction.  In normal
      -- form, arguments to these are either themselves or a variable.
      Param :: Term -> Term 
+     Swap :: Permutation -> Term -> Term 
      Destroy :: Int -> Term -> Term
 
 termPosition :: Term -> Irr Position 
 termPosition (Hole p _) = p
 termPosition (Star p _) = p
-termPosition (Bound p _) = p
+termPosition (Bound p _ _) = p
 termPosition (Pi _ i _ _) = identPosition i
 termPosition (Sigma i _ _) = identPosition i
-termPosition (Lam i _ _) = identPosition i
+termPosition (Lam _ i _ _) = identPosition i
 termPosition (Pair i _ _) = identPosition i
-termPosition (x :$: y) = termPosition x
-termPosition (Proj x _) = termPosition x
-termPosition (Extr x _) = termPosition x
+termPosition (App _ x y) = termPosition x
+termPosition (Proj _ x _) = termPosition x
 termPosition (Ann x _) = termPosition x
 termPosition (Param x) = termPosition x
+termPosition (Swap _ x) = termPosition x
 termPosition (OfParam _ x) = termPosition x
 termPosition (Shift _ x) = termPosition x
 termPosition (Destroy _ x) = termPosition x
@@ -69,7 +68,7 @@
 -- invariant: preserves normal forms 
 app :: Term -> Term -> Term 
 app (Lam i _ bo) u = subst0 u bo
-app neutral u = neutral :$: u
+app neutral u = neutral `App` u
 
 subst0 :: Term -> Term -> Term
 subst0 u = subst (u:map bound [0..])  
@@ -85,7 +84,7 @@
   Lam i ty bo -> Lam i (s ty) (s' bo)
   Pi i a b -> Pi i (s a) (s' b)
   Sigma i a b -> Sigma i (s a) (s' b)
-  (a :$: b) -> (s a) `app` (s b)
+  (a `App` b) -> (s a) `app` (s b)
   (Ann e t) -> Ann (s e) (s t)
   (Pair i x y) -> Pair i (s x) (s' y)
   (Proj x f) -> proj (s x) f
@@ -107,7 +106,7 @@
   Lam i ty bo -> Lam i (s ty) (s' bo)
   Pi i a b -> Pi i (s a) (s' b)
   Sigma i a b -> Sigma i (s a) (s' b)
-  (a :$: b) -> (s a) `app` (s b)
+  (a `App` b) -> (s a) `app` (s b)
   (Ann e t) -> Ann (s e) (s t)
   (Pair i x y) -> Pair i (s x) (s' y)
   (Proj x f) -> Proj (s x) f
@@ -145,19 +144,22 @@
 
 dec xs = [ x - 1 | x <- xs, x > 0]
 
+allFreeVars :: Cube Term -> [Int]
+allFreeVars = Prelude.concat . fmap freeVars . cubeElems
+
 freeVars :: Term -> [Int]
 freeVars (Ann a b) = freeVars a <> freeVars b
-freeVars (Pi _ _ a b) = freeVars a <> (dec $ freeVars b)
+freeVars (Pi _ _ a b) = allFreeVars a <> (dec $ freeVars b)
 freeVars (Sigma _ a b) = freeVars a <> (dec $ freeVars b)
-freeVars (Bound _ x) = [x]
-freeVars (a :$: b) = freeVars a <> freeVars b
-freeVars (Lam _ ty b) = freeVars ty <> (dec $ freeVars b)
+freeVars (Bound _ _ x) = [x]
+freeVars (App _ a b) = freeVars a <> allFreeVars b
+freeVars (Lam _ _ ty b) = allFreeVars ty <> (dec $ freeVars b)
 freeVars (Star _ _) = mempty
 freeVars (Hole _ _) = mempty
 freeVars (Pair _ x y) = freeVars x <> (dec $ freeVars y)
-freeVars (Proj x _) = freeVars x
-freeVars (Extr y _) = freeVars y
+freeVars (Proj _ x _) = freeVars x
 freeVars (Param x) = freeVars x
+freeVars (Swap _ x) = freeVars x
 freeVars (OfParam _ x) = freeVars x
 freeVars (Shift _ x) = freeVars x
 freeVars (Destroy _ x) = freeVars x
@@ -170,40 +172,43 @@
 
 cPrint :: Int -> DisplayContext -> Term -> Doc
 cPrint p ii (Destroy i x) = cPrint p ii x <> "%" <> pretty i
-cPrint p ii (Shift (Sort l) x) = cPrint 6 ii x <> text (replicate l '^') 
-                                   -- "⇧" <> 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 (Swap q x) = cPrint p ii x <> "#" <> pretty q
 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 (Bound _ k) 
+cPrint p ii (Bound _ bv k) 
   | k < 0 || k >= length ii  = text "<deBrujn index" <+> pretty k <+> text "out of range>"
-  | otherwise = pretty (ii `index` k)
-cPrint p ii (Proj x f)     = cPrint p ii x <> "#" <> text f
-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))
+  | otherwise = pretty (ii `index` k) <> subscriptPrettyBV bv
+cPrint p ii (Proj True x f)     = cPrint p ii x <> "#" <> text f
+cPrint p ii (Proj False x f)     = cPrint p ii x <> "/" <> text f
+cPrint p ii t@(App _ _ _)     = let (fct,args) = nestedApp t in 
+                                 parensIf (p > 3) (cPrint 3 ii fct <+> sep (map (cPrintCube 4 ii) args))
 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 (Sigma name d r) = parensIf (p > 1) (sep [printBind ii name (unit d) r <+> cross Regu,  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)
 cPrint p ii (Pair name (OfParam _ x) y) 
                             = parensIf (p > (-1)) (sep ["⟦"<>pretty name<>"⟧" <+> text "=" <+> cPrint 0 ii x <> comma, cPrint (-1) (name <| ii) y])
 cPrint p ii (Pair name x y) = parensIf (p > (-1)) (sep [pretty name <+> text "=" <+> cPrint 0 ii x <> comma, cPrint (-1) (name <| ii) y])
 
 nestedLams :: DisplayContext -> Seq Doc -> Term -> Doc
-nestedLams ii xs (Lam x (Hole _ _) c) = nestedLams (x <| ii) (xs |> pretty x) c
-nestedLams ii xs (Lam x ty c) = nestedLams (x <| ii) (xs |> parens (pretty x <+> ":" <+> cPrint 0 ii ty)) c
+-- nestedLams ii xs (Lam o x (Hole _ _) c) = nestedLams (x <| ii) (xs |> pretty x) c
+nestedLams ii xs (Lam o x ty c) = nestedLams (x <| ii) (xs |> parens (pretty x <+> colon o <+> cPrintCube 0 ii ty)) c
 nestedLams ii xs t         = (text "\\ " <> (sep $ toList $ xs) <+> text "->" <+> nest 3 (cPrint 0 ii t))
 
 printBind ii name d r = case not (isDummyId name) ||  0 `iOccursIn` r of
-                  True -> parens (pretty name <+> text ":" <+> cPrint 0 ii d)
-                  False -> cPrint 2 ii d
+                  True -> parens (pretty name <+> colon Regu <+> cPrintCube 0 ii d)
+                  False -> cPrintCube 2 ii d
 
-nestedApp :: Term -> (Term,[Term])
-nestedApp (f :$: a) = (second (++ [a])) (nestedApp f)
+cPrintCube p ii d | dim d == 0 = cPrint p ii (d !? nil)
+                 | otherwise = "{" <> sep (punctuate ";" [pretty i <> "↦" <> cPrint 0 ii x | (i,x) <- cubeAssocs d]) <> "}"
+
+nestedApp :: Term -> (Term,[Cube Term])
+nestedApp (App _ f a) = (second (++ [a])) (nestedApp f)
 nestedApp t = (t,[])
 
 prettyTerm = cPrint (-100)
@@ -221,7 +226,7 @@
   Lam i ty bo -> Lam i (s ty) (s bo)
   Pi i a b -> Pi i (s a) (s b)
   Sigma i a b -> Sigma i (s a) (s b)
-  (a :$: b) -> (s a) :$: (s b)
+  (a `App` b) -> (s a) `App` (s b)
   (Ann e t) -> Ann (s e) (s t)
   (Pair i x y) -> Pair i (s x) (s y)
   (Proj x f) -> Proj (s x) f
@@ -266,7 +271,7 @@
             (paramProg (map (\d -> Hole dummyPosition "pair not in nf!":map wk d) g) y)
      -- because the input is in normal form, the variable bound by the
      -- pair can never appear in y.
-  paramProg g (f :$: a) = foldl app (paramProg g f) [renam g idx a | idx <- [1..arity]] `app` paramProg g a
+  paramProg g (f `App` a) = foldl app (paramProg g f) [renam g idx a | idx <- [1..arity]] `app` paramProg g a
   paramProg g (Proj e f) = proj (paramProg g e) f
   paramProg g (Extr e f) = extr (paramProg g e) f
   paramProg g (Ann _ _) = error "Ann should not be in nf term"
@@ -334,9 +339,9 @@
   (Lam i ty bo)  -> mb d Lam i ty bo  
   (Pair i a b)  -> mb d Pair i a b 
   (Ann e t)  -> Ann <$> pr e <*> pr t 
-  (a :$: b)  -> case pr b of
+  (a `App` b)  -> case pr b of
                    Nothing -> pr a
-                   Just b' -> (:$: b') <$> pr a 
+                   Just b' -> (`App` b') <$> pr a 
   (Proj x f) -> (\x -> Proj x f) <$> pr x  
   (Extr x f) -> (\x -> Extr x f) <$> pr x  
   
diff --git a/TypeCheckerNF.hs b/TypeCheckerNF.hs
--- a/TypeCheckerNF.hs
+++ b/TypeCheckerNF.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PackageImports, TypeSynonymInstances, FlexibleInstances, GADTs #-}
+{-# LANGUAGE PackageImports, TypeSynonymInstances, FlexibleInstances, GADTs, PatternGuards, GeneralizedNewtypeDeriving #-}
 
 -- Type checker loosely based on 
 --
@@ -10,50 +10,57 @@
 --
 -- are also implemented.
 --
--- The ideas related to parametricity and erasure are developed in
---
--- "Realizability and Parametricity in Pure Type Systems", Bernardy, Lasson
---
 
 module TypeCheckerNF where
 
-import Prelude hiding (length)
+import Prelude hiding (length,sequence)
 import Basics
 import qualified Terms
 import Terms (Term (Ann))
 import Display
-import Control.Monad.Error
+import Control.Monad.Error hiding (sequence)
 import Data.Char
 import Data.Maybe (isJust)
 import Control.Monad.Trans.Error (ErrorT, runErrorT)
-import Control.Monad.Trans.Writer
+import Control.Monad.Writer.Class
+import Control.Monad.Writer hiding (sequence)
+import Control.Monad.Trans.State (StateT, execStateT, modify, get)
 import Data.Functor.Identity
 import Data.Sequence hiding (replicate)
-import Data.Foldable (toList)
+import Data.Foldable (toList,Foldable)
+import qualified Data.List as L
+import Data.Traversable
 import Normal hiding (Term)
+import qualified Normal
 import Options
+import Data.Array.IArray (assocs,array)
+import Data.Function
+import Debug.Trace
+import Permutation (permLength)
 
 instance Error (Term,Doc) where
   strMsg s = (Terms.Hole dummyPosition "strMsg: panic!",text s)
 
-type Result a = (ErrorT (Term,Doc)) -- term is used for position information
-                (WriterT [Doc] Identity) a
+newtype Result a = Result ((ErrorT (Term,Doc)) -- term is used for position information
+                          (WriterT [Doc] Identity) a)
+    deriving (Functor,Monad, MonadError (Term,Doc), MonadWriter [Doc])
 
 report :: Doc -> Result ()
-report x = lift $ tell [x]
+report x = tell [x]
 
 runChecker :: Result a -> (Either (Term,Doc) a,[Doc])
-runChecker x = runIdentity $ runWriterT $ runErrorT x
+runChecker (Result x) = runIdentity $ runWriterT $ runErrorT x
 
 data Definition = Abstract -- ^ lambda, pi, sigma bound
                 | Direct Value -- ^ pair bound
 
 type Value    = NF
 type Type     = Value
+type Dimension = Int
 data Bind     = Bind {entryIdent :: Ident, 
                       entryValue :: Definition, -- ^ Value for identifier. 
-                      entryType :: Type,    -- ^ Attention: context of the type does not contain the variable bound here.
-                      entryRelevance :: Relevance
+                      entryType :: Cube Type,    -- ^ Attention: context of the type does not contain the variable bound here.
+                      entryBinder :: Binder
                      }
 type Context  = Seq Bind
 
@@ -64,109 +71,138 @@
 displayT = Terms.prettyTerm . fmap entryIdent
 
 dispContext :: Context -> Doc
-dispContext ctx = case viewl ctx of
+dispContext ctx0 = case viewl ctx0 of
   EmptyL -> mempty
-  Bind x val typ o :< ctx' -> let di = display ctx' in (case val of
-    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), colon o <+> di typ]
-    ) $$ dispContext ctx'
-
--- FIXME: flag an error if impredicativity disabled and we use it anyway.
+  Bind x val typ o :< ctx0' -> (let ctx  = fmap entryIdent ctx0 
+                                    ctx' = fmap entryIdent ctx0'
+                                in case val of
+    Abstract   ->             pretty x <+>                                       colon o <+> printCube o 0 ctx' typ
+    Direct   v ->             pretty x <+> sep ["=" <+> parens (cPrint 0 ctx v), colon o <+> printCube o 0 ctx' typ]
+    ) $$ dispContext ctx0'
 
-hole = Neu . Var . Hole
+todo = Regu -- for now sigma types are always of the "complete" cube kind.
 
-todo = Re
+resurrect :: Binder -> Context -> Context
+resurrect _ = id
 
-resurrect :: Relevance -> Context -> Context
-resurrect Re = id
-resurrect Ir = fmap (\e -> e {entryRelevance = Re})
+subCubeAt' bv c = updateCube (ones $ dim c) (hole "⊘") $ subCubeAt bv c
 
-iType :: Context -> Term -> Result (Value,Type)
+iType :: Context -> Term -> Result (Value,Type,Dimension)
 iType g (Ann e tyt)
   =     do  (ty,o) <- iSort g tyt 
-            v <- cType g e ty
-            return (v,ty) -- annotations are removed
+            (v,d) <- cType g e ty
+            return (v,ty,d) -- annotations are removed
 iType g t@(Terms.Star p s)
-   =  return (Star s,Star $ above s)  
+   =  return (Star s,Star $ above s, 0)  
 iType g (Terms.Pi r1 ident tyt tyt')  
-   =  do  (ty ,s1) <- iSort (resurrect r1 g) tyt 
+   =  do  (ty ,s1) <- iSortCube r1 (resurrect Regu g) tyt 
           (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'
           let o = s1 ⊔ s2
-          return (Pi r1 ident ty ty', Star o)
+          return (Pi r1 ident ty ty', Star o, 0)
 iType g (Terms.Sigma ident tyt tyt')  
-   =  do  let r1 = todo
-          (ty,s1)  <- iSort (resurrect r1 g) tyt 
-          (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'
+   =  do  (ty,s1)  <- iSort (resurrect Regu g) tyt 
+          let r1 = todo
+          (ty',s2) <- iSort (Bind ident Abstract (unit ty) r1 <| g) tyt'
           let o = s1 ⊔ s2
-          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)
+          return (Sigma r1 ident ty ty', Star o, 0)
+iType g e@(Terms.Bound _ bv x) = do
+  when (bvDim bv /= dim typ0) $ 
+       throwError (e,"inexact cube access: expected dimension " <> pretty (dim typ0) )
+  return $ (val $ value, finalTyp, setBits bv)
   where val (Direct v) = wkn (x+1) v
-        val _ = var x -- etaExpand o (var' x) typ
-        Bind _ value typ o = g `index` x
+        val _ = Neu $ Var $ V bv x
+        typ = cubeAccess "iType var" typ0 bv
+        arg = updateCube (ones da) (hole "⊘") arg0
+        arg0 = subCubeAt bv $ fullVarCube x (dim typ0)
+        finalTyp = app Pred (wkn (x+1) typ) arg
+        da = dim arg0
+        Bind _ value typ0 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))
-iType g (e1 Terms.:$: e2)
-  =     do  (v1,si) <- iType g e1
-            case si of
+  return (hole x, hole ("type of " ++ x),0)
+iType g (Terms.App o' e1 e2)
+  =     do  (v1,ti,d) <- iType g e1
+            case ti of
               Pi o _ ty ty' -> do 
-                   v2 <- cType (resurrect o g) e2 ty
-                   return (app o v1 v2, subst0 v2 ty') 
+                   when (o /= o') $ throwError (e1,"application: non-matching binder kinds")
+                   v2 <- cTypeCube o (resurrect o g) e2 ty
+                   return (app o v1 v2, subst0 v2 ty',d)
               _             ->  throwError (e1,"invalid application")
-iType g (Terms.Proj e f) = do
-  (v,t) <- iType g e
+iType g (Terms.Proj isFirst e f) = do
+  (v,t,_) <- iType g e
   search v t
- where search :: NF -> NF -> Result (Value,Type)
-       search v (Sigma o (Irr (Identifier (_,f'))) ty ty') 
-              | f == f' = return (π1,ty)
-              | otherwise = search π2 (subst0 π1 ty')
+ where search :: NF -> NF -> Result (Value,Type,Dimension)
+       search v (Sigma o i ty ty') 
+              | f == f' = return $ if isFirst then (π1,ty,0) else (π2,subst0 (unit π1) ty',0)
+              | otherwise = search π2 (subst0 (unit π1) ty')
            where 
+                 f' = idString i
                  (π1,π2) = (case v of
                              Pair _ _ x y -> (x,y) -- substitution is useless if the pair is in normal form.
-                             _ -> (proj o v True (Irr f'),proj o v False (Irr f'))  -- This could not happen if eta-expansion were done.
+                             _ -> (proj o v True i,proj o v False i)  -- This could not happen if eta-expansion were done.
                              ) :: (NF,NF)
        search _ _ = throwError (e,"field not found")
 
 iType g (Terms.Pair ident e1 e2) = do
-  (v1,t1) <- iType g e1
+  (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)
+  (v2,t2,_) <- iType (Bind ident (Direct v1) (unit t1) r1 <| g) e2
+  return $ (Pair r1 ident v1 (str v2),Sigma r1 ident t1 t2,0)
 -- 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 _) <- 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 t@(Terms.Lam o x h e) 
+   | dim h == 0, (Terms.Hole _ _) <- h !? nil
+   = throwError (t,"cannot infer type for" <+> displayT g t)
+iType g (Terms.Lam o x ty e) = do
+    (vty,vs) <- iSortCube o (resurrect Regu g) ty
+    (ve,t,d) <- iType (Bind x Abstract vty o <| g) e
+    return $ (Lam o x vty ve, Pi o x vty t,min d (dim vty))
 
 iType g (Terms.Param e) = do
-  (v,t) <- iType g e
-  return (param v, app Ir (param t) v)
+  (v,t,d) <- iType g e
+--  report $ "param: " <> vcat [displayT g e, display g t, display g (param Thing t)]
+  return (param Thing v, inTrans [] t v,1+d)
 
-iType g (Terms.Shift f e) = do
-  (v,t) <- iType g e
-  return (shift f v, shift f t)
+iType g (Terms.Swap q e) = do
+  (v,t,d) <- iType g e
+  when (d /= permLength q) $ 
+    throwError (e,"swapped term has wrong dimension: " <> pretty d)
+  return (swap q v, swap q t,d)
 
-iType g x@(Terms.Destroy d e) = do
-  (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)
-    _ -> throwError (e,displayT g e <+> "is not a type")
+         return $ (hole h, Sort 1 0)
+    _ -> throwError (e,displayT g e <+> "is not a type. Instead: " <+> display g v)
 
+iSortCube' :: Int -> Context -> Term -> BitVector -> StateT (Cube Type) Result ()
+iSortCube' s g e i = do
+  types <- get
+  t <- fst <$> (lift $ cType g e (Pi Pred dummyId (subCubeAt i types) (Star $ Sort s $ setBits i)))
+  modify (updateCube i t)
+
+
+-- | Return the cube contents, stuff on the "lower" corner first. Top
+-- corner excluded if Pred cube.
+cubeContents :: Binder -> Cube a -> [(BitVector,a)]
+cubeContents o = L.sortBy (compare `on` (setBits . fst)) . tweak o . assocs
+
+iSortCube :: Binder -> Context -> Cube Term -> Result (Cube Type,Sort)
+iSortCube o g c = do
+  (t0,Sort l _) <- iSort g (c !? zeros (dim c))
+  
+  ts <- execStateT (sequence [iSortCube' l g a i | (i,a) <- L.drop 1 $ -- exclude the lower corner, as it's not a Pi here. (and already checked)
+                                                            cubeContents o c])
+                   (updateCube (zeros (dim c)) t0 $ full (const $ hole "⊘") (dim c))
+  return (ts,Sort l (dim c)) 
+ where d = dim c
+
 unify :: Context -> Term -> Type -> Type -> Result ()
 unify g e q q' =
          do let ii = length g
@@ -179,50 +215,73 @@
                        (throwError (e,hang "type mismatch: " 2 $ vcat 
                                              ["inferred:" <+> display g q',
                                               "expected:" <+> display g q ,
+                                              -- "q'" <+> text (show q'),
+                                              -- "q " <+> text (show q),
                                               "for:" <+> displayT g e ,
                                               "context:" <+> dispContext g]))
 
+unifyAll :: Binder -> Context -> Term -> Cube Type -> Cube Type -> Result ()
+unifyAll o g e q q' = do
+  when (dim q /= dim q') $ throwError (e,"non-matching dimensions")
+  -- FIXME: skip if Pred
+  sequence_ $ tweak o $ Prelude.zipWith (unify g e) (cubeElems q) (cubeElems q')
+
 -- Check the type and normalize
-cType :: Context -> Term -> Type -> Result Value
-cType g (Terms.Lam name (Terms.Hole _ _) e) (Pi o name' ty ty') = do
-        e' <- cType (Bind name Abstract ty o <| g) e ty'
-        return (Lam o name ty e') -- the type is filled in.
+cType :: Context -> Term -> Type -> Result (Value,Dimension)
+cType g (Terms.Lam _ name h e) (Pi o name' ty ty') | dim h == 0, (Terms.Hole _ _) <- h !? nil = do
+        (e',d) <- cType (Bind name Abstract ty o <| g) e ty'
+        return (Lam o name ty e',min d (dim ty)) -- the type and binder is filled in.
 
-cType g (Terms.Lam name ty0 e) (Pi o name' ty ty')
-  =     do (t,_o) <- iSort g ty0
-           unify g (Terms.Hole (identPosition name) (show name)) t ty
-           e' <- cType (Bind name Abstract ty o <| g) e ty'
-           return (Lam o name ty e')
+cType g e0@(Terms.Lam o' name ty0 e) (Pi o name' ty ty')
+  =     do when (o /= o') $ throwError (e0,"Unmatching flavours of quantification")
+           (t,_o) <- iSortCube o (resurrect o g) ty0
+           unifyAll o g (Terms.Hole (identPosition name) (show name)) t ty
+           (e',d) <- cType (Bind name Abstract ty o <| g) e ty'
+           return (Lam o name ty e',min d (dim ty))
 
 cType g (Terms.Pair name e1 e2) (Sigma o name' ty ty') = do
   -- note that names do not have to match.
-  v1 <- cType g e1 ty           
-  v2 <- cType (Bind name (Direct v1) ty o <| g) e2 (wk $ subst0 v1 ty') 
+  (v1,d1) <- cType g e1 ty           
+  (v2,d2) <- cType (Bind name (Direct v1) (unit ty) o <| g) e2 (wk $ subst0 (unit v1) ty') 
         -- The above weakening is there because:
         -- * the type contains no occurence of the bound variable after substitution, but
         -- * the context is extended anyway, to bind the name to its value.
-  return $ Pair o name' v1 (str v2)
+  return (Pair o name' v1 (str v2),min d1 d2)
   -- note that the pair must use the name of the sigma for the
   -- field. (The context will use the field name provided by the type)
-
+{-
 --  Γ ⊢ ⌊A⌋ : B
 cType g (Terms.OfParam i e) t = do
   -- Γ ⊢ A ⌊A⌋ : ⟦B⟧ ⌊A⌋
   -- Γ ⊢ A x   : ⟦B⟧ x
   -- Γ ⊢ A     : (x : ⌊B⌋) → ⟦B⟧ x
-  e' <- cType g e $ Pi Ir i t (zerInRel 0 t)
+  e' <- cType g e $ Pi Ty i t (zerInRel 0 t)
   return (Neu $ OfParam i e')
-
-cType g (Terms.Shift f e) t = do
-  shift f <$> cType g e (shift (negate f) t) 
-  -- there might be negative sorts in there, but that should be fine;
-  -- if they occur the type checker will simply reject the term
-  -- because it's impossible to create an inhabitant of a negative
-  -- sort.
+-}
 
 cType g e v 
-  =     do (e',v') <- iType g e
+  =     do (e',v',d) <- iType g e
            unify g e v v'
-           return e'
+           return (e',d)
 
 
+cTypeCube' :: Context -> Term -> Cube Type -> BitVector -> StateT (Cube Value) Result ()
+cTypeCube' g e t i = do
+  values <- get
+  v <- fst <$> (lift $ cType g e (app Pred (t !? i) (subCubeAt i values)))
+  modify (updateCube i v)
+             
+tweak Regu = id
+tweak Pred = init
+
+cTypeCube :: Binder -> Context -> Cube Term -> Cube Type -> Result (Cube Value)
+cTypeCube o g e t = do
+  when (dim e /= dim t) $ 
+       throwError (cubeFirstElemForErr e,"type cube: non-matching dimensions")
+  execStateT (sequence [cTypeCube' g a t i | (i,a) <- cubeContents o e])
+             (full (const $ hole "⊘") (dim e))
+
+
+cubeFirstElemForErr :: Cube Term -> Term
+cubeFirstElemForErr c = (cubeElems c ++ [error "empty cube!"]) !! 0
+  
diff --git a/tutorial/01-Module.ua b/tutorial/01-Module.ua
--- a/tutorial/01-Module.ua
+++ b/tutorial/01-Module.ua
@@ -43,11 +43,11 @@
 four = exp two (mul two two),
 
 -- The syntax for pairs is "first class", we can have them anywhere:
-somePair = (pi1 = two, plus two four) : (Nat ; Nat),
+somePair = (pi1 = two, plus two four) : (Nat ;; Nat),
 
 
 -- Dependent pairs can also be declared
-depPair  = (A = Nat, suc) : ((A : *1) ; A -> A),
+depPair  = (A = Nat, suc) : ((A : *1) ;; A -> A),
 
 -- fields named in the type can be extracted using .:
 extract = depPair.A,
diff --git a/tutorial/02.1-Relevance.ua b/tutorial/02.1-Relevance.ua
deleted file mode 100644
--- a/tutorial/02.1-Relevance.ua
+++ /dev/null
@@ -1,60 +0,0 @@
--- Relevance and erasure
--------------------------
-
--- 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.
-
--- 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 =>.
-
--- 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...
-
-
-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:
-      \(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 depth of irrelevancy to erase. 
-
-Nat-representation = Nat % 0,
-
--- The normal form of the above term reveals that the result is the
--- usual Church encoding for naturals.
-
-
-*
diff --git a/tutorial/03-Parametricity.ua b/tutorial/03-Parametricity.ua
--- a/tutorial/03-Parametricity.ua
+++ b/tutorial/03-Parametricity.ua
@@ -1,32 +1,34 @@
--- Parametricity, relevance and erasure
------------------------------------------
+-- Parametricity
+-----------------
 
--- In uAgda every term is assumed to be parametric.
+-- In uAgda every term is known to be parametric.
 -- hence for an arbitrary function f...
 \(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),
+fparam = f! : (x : {A ; A!}) -> B! @ {f (x 0)},
 
--- 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):
+-- Note here that we introduce the cube syntax.
+-- {A; A!}   is a 2-element cube; and 
+-- x 0       accesses the 1st component of the cube x.
 
-eraseType = ((x : A) => A! x -> B! (f x)) % 0,
+-- We also have an example of an incomplete cube: 
+-- {f (x 0)} 
 
+-- In the above, it is inferred to be incomplete thanks to the special
+-- application operator: 
 
--- Indeed, f!%0 = f.
-fAgain = fparam %0,
+-- @ (Relation membership test) 
 
+-- Finally, relation types can be formed using the double arrow:
+-- =>
 
--- We can get binary parametricity by combination of unary
--- parametricity and erasure. See the following reference for
--- the explanation:
+-- Note that, so far, there was no explicit mention of cubes, because
+-- a 1-element cube can be just written as its contents. That is, A
+-- really stands for {A} in a cube context.
 
--- http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466
+-- See the paper for a detailed explanation of the role of cubes.
 
-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,23 +1,58 @@
 -- let's use parametricity in a useful way: prove that any
 -- function of type (X : #) -> X -> X is the identity.
 
--- To simplify the example we use impredicativity here.
+-- To simplify the example we use impredicativity here; the impredicative sort is written #.
 
-Eq = \A a b -> (P : A => #) -> P a -> P b
-   : (A : #) -> A => A => #
+
+-------------------------
+-- Preliminaries
+
+-- Type of propositions, at dimension 1. (Optionally, the dimension of
+-- a sort is written after a pipe; otherwise it is 0)
+prop = #|1, 
+
+-- Truth
+Top = (A : #) -> A -> A
+    : #,
+
+-- ... and its inhabitant
+tt = \A x -> x
+   : Top,
+
+
+---------------------------------------------------
+-- Leibniz equality (modified to support cubes.)
+
+-- The regular definition for Leibniz equality is
+-- Eq = \A a b -> (P : A -> #) -> P a -> P b
+
+-- We face a number of superficial complications, because we want Eq A
+-- a b to be of dimension 1, instead of dimension 0.
+
+-- 1. we must use #|1 instead of #|0;
+-- 2. we have to extend quantifications in such a way that they are always over cubes of dimension 1.
+--    this is done by adding dummy arguments in cubes (# and Top below)
+
+Eq = \A a b -> (P : {# ; \t => (z : A) => prop} ) -> {Top ; \t => P 1 @ a} -> P 1 @ (b 0)
+   : (A : #) -> A -> A => prop
    ,
 
+refl = \A x P p -> p 1
+     : (A : #) -> (x : A) -> Eq A x @ x,
+
+-- The theorem is expressed as normal:
 Theorem = 
   (f : (A : #) -> A -> A) ->
   (A : #) ->
   (x : A) ->
-  Eq A x (f A x),
-
+  Eq A x @ (f A x),
 
+-- The proof follows the usual technique; see the paper for details.
 proof = \(f : (A : #) -> (a : A) -> A) ->
         \(A : #) ->
-        \(x : A) -> f! A (\y -> Eq A x y) x (\_ p -> p)
-      : Theorem
-,
+        \(x : A) -> f! {A ; \y => Eq A x @ (y 0) } {x ; refl A x}
+      : Theorem,
+
+
 # 
 
diff --git a/tutorial/04-Data.ua b/tutorial/04-Data.ua
deleted file mode 100644
--- a/tutorial/04-Data.ua
+++ /dev/null
@@ -1,75 +0,0 @@
--- Data
----------
-
--- In the Calculus of Constructions, it is possible to encode data via
--- Church-style encodings. However, it is then impossible to do
--- inductive reasoning on these. This led to the addition of inductive
--- constructions (CiC). Agda features inductive families as a native
--- construct.
-
--- Even though uAgda does not feature a native construction for data,
--- it is possible to encode data using parametricity, erasure and a
--- little bit of special sauce. The trick is that 
-
--- 1. The erasure of the induction principle for a given inductive
--- family is equal to its Church representation, and
-
--- 2. The relational interpretation of the representation yields back
--- the inductive principle.
-
--- More theoretical background can be found in Phil Wadler's "The
--- Girard-Reynolds isomorphism".
-
-
--- In uAgda, we proceed as follows. First define the appropriate
--- induction principle and the proof that the constructors respect
--- induction. (Note that these definitions are parameterised over an
--- arbitrary module "q" containing an *abstract* version of the stuff
--- we want to define (here with fields Nat, suc and zer).
-
-param Q = \ q -> (
-
-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),
-\ _ -> *)
-
-:: ((Nat : *1) ; (zer : Nat) ; (suc : Nat -> Nat) ; *1),
-
--- The keyword "param" and the double colon are special syntax to
--- construct a concrete representation (here "Q") that is
--- computationally equal to the erasure of the above, but whose
--- relational interpretation is the one given.
-
--- (The last component of the tuple is just noise, as usual).
-
-
--- From there we can do simple computations:
-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,
-
-
--- In particular, we can also inductive computation.  In that case,
--- because we work in a predicative type system, we need to apply the
--- induction on a copy of the natural lifted to a higher universe.
--- That's fine, because we also have an operator for that: postfix ^.
-
-lift = \n -> n^
-     : Q.Nat -> Q.Nat^,
-
-plus 
- = \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,17 +1,11 @@
 name:           uAgda
-version:        1.1.0.0
+version:        1.2.0.0
 category:       Dependent Types
 synopsis:       A simplistic dependently-typed language with parametricity.
 description:
 
         uAgda implements an experimental dependently-typed language
-        (and proof assistant by the Curry-Howard isomorphism). The
-        goal of the project is twofold:
-        .
-        1. Experiment with a minimalistic language that is strong enough to
-        program and reason in.
-        .
-        2. Give a simple implementation of its type-checker (ours is ~200 lines).
+        (and proof assistant by the Curry-Howard isomorphism), extended with support for parametricity.
         .
         See the share/tutorial directory for how to get started.
    
@@ -28,10 +22,8 @@
      tutorial/00-Start-Here.ua
      tutorial/01-Module.ua
      tutorial/02-Holes.ua
-     tutorial/02.1-Relevance.ua
      tutorial/03-Parametricity.ua
      tutorial/03.1-Parametricity-Use.ua
-     tutorial/04-Data.ua
 
 
 executable uAgda
@@ -50,11 +42,13 @@
      TypeCheckerNF
 
   build-depends: base==4.*
+  build-depends: array==0.3.*
   build-depends: cmdargs==0.6.*
-  build-depends: containers==0.3.*
+  build-depends: containers==0.4.*
   build-depends: pretty==1.0.*
   build-depends: parsec==2.1.*
-  build-depends: BNFC-meta==0.1.*
+  build-depends: BNFC-meta==0.3.*
   build-depends: transformers == 0.2.*
-  build-depends: monads-fd == 0.1.*
+  build-depends: mtl == 2.0.*
+  build-depends: split == 0.1.*