diff --git a/Normal.hs b/Normal.hs
--- a/Normal.hs
+++ b/Normal.hs
@@ -50,7 +50,7 @@
      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
+     Hole :: Irr String -> Variable
 
 type Subst = [Cube NF]
 
@@ -69,7 +69,7 @@
 subst0 :: Cube NF -> NF -> NF
 subst0 u = subst (u:map (unit . var) [0..])  
 
-hole = Neu . Var . Hole
+hole = Neu . Var . Hole . Irr
 
 subst :: Subst -> Term n -> NF
 subst f t = case t of
@@ -88,7 +88,7 @@
 --  OfParam i x -> Neu (OfParam i (s x))
   
 --  Destr d x -> destroy d (s x)
-  Hole x -> hole x
+  Hole (Irr 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
@@ -126,7 +126,7 @@
 
 wk = wkn 1
 str = strn 1
-strn n = subst (replicate n (unit $ Neu $ Var $ Hole "str: oops!") ++ map (unit . var) [0..])
+strn n = subst (replicate n (unit $ hole "str: oops!") ++ map (unit . var) [0..])
 
 wkv :: Int -> Variable -> Variable
 wkv n (Param r x) = Param r (wkv n x)
@@ -185,7 +185,7 @@
 -- 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 (Hole (Irr x)) = text x
 cPrint p ii (Star i) = pretty i
 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 "/")
@@ -262,19 +262,16 @@
 swapV q (V bv x) = Swap q $ V bv 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 v@(Param _ _) | isIdentity q' = v
+                      | otherwise = Swap (simplifyPerm n q) v
+    where n = countParam v
+          q' = simplifyPerm n q
+swapV q (Hole (Irr s)) = Hole $ Irr (s ++ "#")
 swapV q x = Swap q x
 
-power 0 f = id
-power n f = f . power (n-1) f
-
-(f *** g) (x,y) = (f x, g y)  
-
 -- 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)
+countParam (Param Thing x) = 1 + countParam x
+countParam x = 0
 
 fullVarCube x = full (\i -> Neu $ Var $ V i x) 
 
@@ -328,7 +325,7 @@
                     maybeParam = if r == Thing then Param r else id -- keep only "proper" parametricity
                     n = getDepth x
 
-transV r d  (Hole s) = Neu $ Var $ Hole (s ++ showRole r)
+transV r d  (Hole (Irr s)) = hole (s ++ showRole r)
 
 transNe :: Role -> Action -> Neutral -> NF
 transNe r d (Var v)      = transV r d v
@@ -357,7 +354,7 @@
 
 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)
+trans' Thing d ty = Lam Pred (synthId "z") (unit1 (transNF Index d ty)) (zerInRel d ty)
 
 -- | Build the relation x ∈ ⟦ty⟧. (where 'x' is 0; but not bound in 'ty'.)
 zerInRel :: Action -> NF -> NF
@@ -370,10 +367,11 @@
 
 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 (Star (Sort l δ))       z = (Pi Pred dummyId (unit1 z) (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 "⊘"))
+inTrans d ty z = app Pred (transNF Thing d ty) (unit1 z)
 
+unit1 z = (pair z (hole "⊘"))
diff --git a/TypeCheckerNF.hs b/TypeCheckerNF.hs
--- a/TypeCheckerNF.hs
+++ b/TypeCheckerNF.hs
@@ -73,11 +73,10 @@
 dispContext :: Context -> Doc
 dispContext ctx0 = case viewl ctx0 of
   EmptyL -> mempty
-  Bind x val typ o :< ctx0' -> (let ctx  = fmap entryIdent ctx0 
-                                    ctx' = fmap entryIdent ctx0'
+  Bind x val typ o :< ctx0' -> (let 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]
+    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'
 
 todo = Regu -- for now sigma types are always of the "complete" cube kind.
@@ -112,7 +111,7 @@
   where val (Direct v) = wkn (x+1) v
         val _ = Neu $ Var $ V bv x
         typ = cubeAccess "iType var" typ0 bv
-        arg = updateCube (ones da) (hole "⊘") arg0
+        arg = updateCube (ones da) (hole  "⊘") arg0
         arg0 = subCubeAt bv $ fullVarCube x (dim typ0)
         finalTyp = app Pred (wkn (x+1) typ) arg
         da = dim arg0
@@ -176,7 +175,7 @@
   (val,v,_) <- iType g e
   case v of 
     Star i -> return (val,i)
-    (Neu (Var (Hole h))) -> do 
+    (Neu (Var (Hole (Irr h)))) -> do 
          report $ text h <+> "must be a type"
          return $ (hole h, Sort 1 0)
     _ -> throwError (e,displayT g e <+> "is not a type. Instead: " <+> display g v)
diff --git a/tutorial/03.2-Nested-Parametricity.ua b/tutorial/03.2-Nested-Parametricity.ua
new file mode 100644
--- /dev/null
+++ b/tutorial/03.2-Nested-Parametricity.ua
@@ -0,0 +1,18 @@
+-- nested parametricity example from the paper.
+
+
+\(A : *) ->
+
+( 
+  parametricity = \(x:A) -> x!
+                : (x:A) -> A! @ {x},
+
+  nested = parametricity!
+         : (x : {A; A!}) -> A!! @ {x 0;x 1;x 0!},
+  
+  nestedNF = \ (x : {A; A!}) -> x 1 ! #10
+           :   (x : {A; A!}) -> A!! @ {x 0;x 1;x 0!},
+         
+
+*
+)
diff --git a/uAgda.cabal b/uAgda.cabal
--- a/uAgda.cabal
+++ b/uAgda.cabal
@@ -1,5 +1,5 @@
 name:           uAgda
-version:        1.2.0.0
+version:        1.2.0.1
 category:       Dependent Types
 synopsis:       A simplistic dependently-typed language with parametricity.
 description:
@@ -24,6 +24,7 @@
      tutorial/02-Holes.ua
      tutorial/03-Parametricity.ua
      tutorial/03.1-Parametricity-Use.ua
+     tutorial/03.2-Nested-Parametricity.ua
 
 
 executable uAgda