diff --git a/Setup.hs b/Setup.hs
index 9a994af..09e11ce 100644
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,2 +1,4 @@
+
 import Distribution.Simple
+
 main = defaultMain
diff --git a/cubical.cabal b/cubical.cabal
index bef1588..deeb799 100644
--- a/cubical.cabal
+++ b/cubical.cabal
@@ -20,6 +20,7 @@ executable cubical
 
   build-depends:       base       ^>= 4.14
                      , mtl        ^>= 2.2
+                     , syb        ^>= 0.7
                      , text       ^>= 1.2
                      , array      ^>= 0.5
                      , containers ^>= 0.6
diff --git a/intro.tt b/intro.tt
index aa896d3..233fd4c 100644
--- a/intro.tt
+++ b/intro.tt
@@ -59,18 +59,18 @@ inot : I -> I
 
 -- The type PathP generalises this to dependent products (i : I) -> A i.
 
-PathP : (A : I -> Pretype) -> A i0 -> A i1 -> Type
+PathP : (A : I -> Type) -> A i0 -> A i1 -> Type
 {-# PRIMITIVE PathP #-}
 
 -- By taking the first argument to be constant we get the equality type
 -- Path.
 
-Path : {A : Pretype} -> A -> A -> Type
+Path : {A : Type} -> A -> A -> Type
 Path {A} = PathP (\i -> A)
 
 -- reflexivity is given by constant paths
 
-refl : {A : Pretype} {x : A} -> Path x x
+refl : {A : Type} {x : A} -> Path x x
 refl {A} {x} i = x
 
 -- Symmetry (for dpeendent paths) is given by inverting the argument to the path, such that
@@ -78,18 +78,18 @@ refl {A} {x} i = x
 --   sym p i1 = p (inot i1) = p i0
 -- This has the correct endpoints.
 
-sym : {A : I -> Pretype} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x
+sym : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x
 sym p i = p (inot i)
 
 id : {A : Type} -> A -> A
 id x = x
 
-the : (A : Pretype) -> A -> A
+the : (A : Type) -> A -> A
 the A x = x
 
 -- The eliminator for the interval says that if you have x : A i0 and y : A i1,
 -- and x ≡ y, then you can get a proof A i for every element of the interval.
-iElim : {A : I -> Pretype} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i
+iElim : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i
 iElim p i = p i
 
 -- This corresponds to the elimination principle for the HIT
@@ -268,6 +268,7 @@ transp A x = comp A (\i [ ]) (inS x)
 fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> (i : I) -> A i
 fill A {phi} u a0 i =
     comp (\j -> A (iand i j))
+         {ior phi (inot i)}
          (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])
          (inS (outS a0))
 
@@ -293,4 +294,38 @@ transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path
 transpFun p q f = refl
 
 -- When considering the more general case of a composition respecing sides,
--- the outer transport becomes a composition.
\ No newline at end of file
+-- the outer transport becomes a composition.
+
+-- Glueing and Univalence
+-------------------------
+
+fiber : {A : Type} {B : Type} -> (A -> B) -> B -> Type
+fiber f y = (x : A) * Path (f x) y
+
+isEquiv : {A : Type} {B : Type} -> (A -> B) -> Type
+isEquiv {A} {B} f = (y : B) -> isContr (fiber f y)
+
+Equiv : (A : Type) (B : Type) -> Type
+Equiv A B = (f : A -> B) * isEquiv f
+
+primGlue : (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
+{-# PRIMITIVE Glue primGlue #-}
+prim'Glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> (e o).1 (t o)) -> primGlue A T e
+{-# PRIMITIVE glue prim'Glue #-}
+primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> primGlue A {phi} T e -> A
+{-# PRIMITIVE unglue primUnglue #-}
+
+Glue : (A : Type) {phi : I} -> Partial phi ((X : Type) * Equiv X A) -> Type
+Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2)
+
+idEquiv : {A : Type} -> isEquiv (id {A})
+idEquiv y = ((y, \i -> y), \u i -> (u.2 (inot i), \j -> u.2 (ior (inot i) j)))
+
+univalence : {A : Type} {B : Type} -> Equiv A B -> Path A B
+univalence {A} {B} equiv i = Glue B (\[ (i = i0) -> (A, equiv), (i = i1) -> (B, the B, idEquiv {B}) ]) 
+
+A, B : Type
+f : Equiv A B
+x : A
+line : I -> Type
+line i = univalence {A} {B} f i
\ No newline at end of file
diff --git a/src/Elab.hs b/src/Elab.hs
index 1210c26..e719da7 100644
--- a/src/Elab.hs
+++ b/src/Elab.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -7,6 +8,7 @@ import Control.Monad.Reader
 import Control.Exception
 
 import qualified Data.Map.Strict as Map
+import qualified Data.Set as Set
 import Data.Traversable
 import Data.Typeable
 import Data.Foldable
@@ -20,9 +22,8 @@ import qualified Presyntax.Presyntax as P
 
 import Prettyprinter
 
-import Syntax
 import Syntax.Pretty
-import qualified Data.Text as T
+import Syntax
 
 infer :: P.Expr -> ElabM (Term, NFType)
 infer (P.Span ex a b) = withSpan a b $ infer ex
@@ -72,23 +73,23 @@ check :: P.Expr -> NFType -> ElabM Term
 check (P.Span ex a b) ty = withSpan a b $ check ex ty
 
 check (P.Lam p var body) (VPi p' dom (Closure _ rng)) | p == p' =
-  assume (Bound var) dom $
-    Lam p var <$> check body (rng (VVar (Bound var)))
+  assume (Bound var 0) dom $ \name ->
+    Lam p name <$> check body (rng (VVar name))
 
 check tm (VPi P.Im dom (Closure var rng)) =
-  assume (Bound var) dom $
-    Lam P.Im var <$> check tm (rng (VVar (Bound var)))
+  assume var dom $ \name ->
+    Lam P.Im name <$> check tm (rng (VVar name))
 
 check (P.Lam p v b) ty = do
   porp <- isPiType p =<< forceIO ty
   case porp of
     It'sProd d r wp ->
-      assume (Bound v) d $
-        wp . Lam p v <$> check b (r (VVar (Bound v)))
+      assume (Bound v 0) d $ \name ->
+        wp . Lam p name <$> check b (r (VVar name))
 
     It'sPath li le ri wp -> do
-      tm <- assume (Bound v) VI $
-        Lam P.Ex v <$> check b (force (li (VVar (Bound v))))
+      tm <- assume (Bound v 0) VI $ \var ->
+        Lam P.Ex var <$> check b (force (li (VVar var)))
 
       tm_nf <- eval tm
 
@@ -101,12 +102,12 @@ check (P.Lam p v b) ty = do
       pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
 
     It'sPartial phi a wp ->
-      assume (Bound v) (VIsOne phi) $
-        wp . Lam p v <$> check b a
+      assume (Bound v 0) (VIsOne phi) $ \var ->
+        wp . Lam p var <$> check b a
 
     It'sPartialP phi a wp ->
-      assume (Bound v) (VIsOne phi) $
-        wp . Lam p v <$> check b (a @@ VVar (Bound v))
+      assume (Bound v 0) (VIsOne phi) $ \var ->
+        wp . Lam p var <$> check b (a @@ VVar var)
 
 check (P.Pair a b) ty = do
   (d, r, wp) <- isSigmaType =<< forceIO ty
@@ -119,17 +120,17 @@ check (P.Pi p s d r) ty = do
   isSort ty
   d <- check d ty
   d_nf <- eval d
-  assume (Bound s) d_nf $ do
+  assume (Bound s 0) d_nf \var -> do
     r <- check r ty
-    pure (Pi p s d r)
+    pure (Pi p var d r)
 
 check (P.Sigma s d r) ty = do
   isSort ty
   d <- check d ty
   d_nf <- eval d
-  assume (Bound s) d_nf $ do
+  assume (Bound s 0) d_nf \var -> do
     r <- check r ty
-    pure (Sigma s d r)
+    pure (Sigma var d r)
 
 check (P.LamSystem bs) ty = do
   (extent, dom) <- isPartialType ty
@@ -138,34 +139,34 @@ check (P.LamSystem bs) ty = do
     phi <- checkFormula (P.condF formula)
     rhses <-
         case P.condV formula of
-          Just t -> assume (Bound t) (VIsOne phi) $ do
+          Just t -> assume (Bound t 0) (VIsOne phi) $ \var -> do
             env <- ask
             for (truthAssignments phi (getEnv env)) $ \e -> do
               let env' = env{ getEnv = e }
-              check rhs (eval' env' dom_q)
+              (Just var,) <$> check rhs (eval' env' dom_q)
           Nothing -> do
             env <- ask
             for (truthAssignments phi (getEnv env)) $ \e -> do
               let env' = env{ getEnv = e }
-              check rhs (eval' env' dom_q)
-    pure (n, (phi, (P.condV formula, head rhses)))
+              (Nothing,) <$> check rhs (eval' env' dom_q)
+    pure (n, (phi, head rhses))
 
   unify extent (foldl ior VI0 (map (fst . snd) eqns))
 
   for_ eqns $ \(n, (formula, (binding, rhs))) -> do
     let
       k = case binding of
-        Just v -> assume (Bound v) (VIsOne formula)
+        Just v -> assume v (VIsOne formula) . const
         Nothing -> id
     k $ for_ eqns $ \(n', (formula', (binding, rhs'))) -> do
       let
         k = case binding of
-          Just v -> assume (Bound v) (VIsOne formula)
+          Just v -> assume v (VIsOne formula) . const
           Nothing -> id
         truth = possible mempty (iand formula formula')
         add [] = id
-        add ((~(HVar x), True):xs) = define x VI VI1 . add xs
-        add ((~(HVar x), False):xs) = define x VI VI0 . add xs
+        add ((~(HVar x), True):xs) = redefine x VI VI1 . add xs
+        add ((~(HVar x), False):xs) = redefine x VI VI0 . add xs
       k $ when ((n /= n') && fst truth) . add (Map.toList (snd truth)) $ do
         vl <- eval rhs
         vl' <- eval rhs'
@@ -180,7 +181,7 @@ check (P.LamSystem bs) ty = do
   let
     mkB name (Just v, b) = App P.Ex (Lam P.Ex v b) (Ref name)
     mkB _ (Nothing, b) = b
-  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, mkB (Bound name) y)) eqns))))
+  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, mkB name y)) eqns))))
 
 check exp ty = do
   (tm, has) <- switch $ infer exp
@@ -204,10 +205,11 @@ checkFormula (P.FIs1 x) = do
   pure (VVar nm)
 
 isSort :: NFType -> ElabM ()
-isSort VType                = pure ()
-isSort VTypeω               = pure ()
-isSort vt@(VNe HMeta{} _)   = unify vt VType
-isSort vt = throwElab $ NotEqual vt VType
+isSort t = isSort (force t) where
+  isSort VType              = pure ()
+  isSort VTypeω             = pure ()
+  isSort vt@(VNe HMeta{} _) = unify vt VType
+  isSort vt = throwElab $ NotEqual vt VType
 
 data ProdOrPath
   = It'sProd { prodDmn  :: NFType
@@ -229,45 +231,48 @@ data ProdOrPath
                  }
 
 isPiType :: P.Plicity -> NFType -> ElabM ProdOrPath
-isPiType p (VPi p' d (Closure _ k)) | p == p' = pure (It'sProd d k id)
-isPiType P.Ex (VPath li le ri) = pure (It'sPath (li @@) le ri id)
-isPiType P.Ex (VPartial phi a) = pure (It'sPartial phi a id)
-isPiType P.Ex (VPartialP phi a) = pure (It'sPartialP phi a id)
-
-isPiType P.Ex (VPi P.Im d (Closure _ k)) = do
-  meta <- newMeta d
-  porp <- isPiType P.Ex (k meta)
-  pure $ case porp of
-    It'sProd d r w -> It'sProd d r (\f -> w (App P.Im f (quote meta)))
-    It'sPath l x y w -> It'sPath l x y (\f -> w (App P.Im f (quote meta)))
-    It'sPartial phi a w -> It'sPartial phi a (\f -> w (App P.Im f (quote meta)))
-    It'sPartialP phi a w -> It'sPartialP phi a (\f -> w (App P.Im f (quote meta)))
-isPiType p t = do
-  dom <- newMeta VType
-  name <- newName
-  assume (Bound name) dom $ do
-    rng <- newMeta VType
-    wp <- isConvertibleTo t (VPi p dom (Closure name (const rng)))
-    pure (It'sProd dom (const rng) wp)
+isPiType p x = isPiType p (force x) where
+  isPiType p (VPi p' d (Closure _ k)) | p == p' = pure (It'sProd d k id)
+  isPiType P.Ex (VPath li le ri) = pure (It'sPath (li @@) le ri id)
+  isPiType P.Ex (VPartial phi a) = pure (It'sPartial phi a id)
+  isPiType P.Ex (VPartialP phi a) = pure (It'sPartialP phi a id)
+
+  isPiType P.Ex (VPi P.Im d (Closure _ k)) = do
+    meta <- newMeta d
+    porp <- isPiType P.Ex (k meta)
+    pure $ case porp of
+      It'sProd d r w -> It'sProd d r (\f -> w (App P.Im f (quote meta)))
+      It'sPath l x y w -> It'sPath l x y (\f -> w (App P.Im f (quote meta)))
+      It'sPartial phi a w -> It'sPartial phi a (\f -> w (App P.Im f (quote meta)))
+      It'sPartialP phi a w -> It'sPartialP phi a (\f -> w (App P.Im f (quote meta)))
+  isPiType p t = do
+    dom <- newMeta VType
+    name <- newName
+    assume name dom $ \name -> do
+      rng <- newMeta VType
+      wp <- isConvertibleTo t (VPi p dom (Closure name (const rng)))
+      pure (It'sProd dom (const rng) wp)
 
 isSigmaType :: NFType -> ElabM (Value, NFType -> NFType, Term -> Term)
-isSigmaType (VSigma d (Closure _ k)) = pure (d, k, id)
-isSigmaType t = do
-  dom <- newMeta VType
-  name <- newName
-  assume (Bound name) dom $ do
-    rng <- newMeta VType
-    wp <- isConvertibleTo t (VSigma dom (Closure name (const rng)))
-    pure (dom, const rng, wp)
+isSigmaType t = isSigmaType (force t) where
+  isSigmaType (VSigma d (Closure _ k)) = pure (d, k, id)
+  isSigmaType t = do
+    dom <- newMeta VType
+    name <- newName
+    assume name dom $ \name -> do
+      rng <- newMeta VType
+      wp <- isConvertibleTo t (VSigma dom (Closure name (const rng)))
+      pure (dom, const rng, wp)
 
 isPartialType :: NFType -> ElabM (NFEndp, Value)
-isPartialType (VPartial phi a) = pure (phi, a)
-isPartialType (VPartialP phi a) = pure (phi, a)
-isPartialType t = do
-  phi <- newMeta VI
-  dom <- newMeta (VPartial phi VType)
-  unify t (VPartial phi dom)
-  pure (phi, dom)
+isPartialType t = isPartialType (force t) where
+  isPartialType (VPartial phi a) = pure (phi, a)
+  isPartialType (VPartialP phi a) = pure (phi, a)
+  isPartialType t = do
+    phi <- newMeta VI
+    dom <- newMeta (VPartial phi VType)
+    unify t (VPartial phi dom)
+    pure (phi, dom)
 
 checkStatement :: P.Statement -> ElabM a -> ElabM a
 checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
@@ -275,23 +280,23 @@ checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
 checkStatement (P.Decl name ty) k = do
   ty <- check ty VTypeω
   ty_nf <- eval ty
-  assumes (Defined <$> name) ty_nf k
+  assumes (flip Defined 0 <$> name) ty_nf (const k)
 
 checkStatement (P.Defn name rhs) k = do
-  ty <- asks (Map.lookup (Defined name) . getEnv)
+  ty <- asks (Map.lookup name . nameMap)
   case ty of
     Nothing -> do
       (tm, ty) <- infer rhs
       tm_nf <- eval tm
-      define (Defined name) ty tm_nf k
-    Just (ty_nf, nm) -> do
-      case nm of
-        VVar (Defined n') | n' == name -> pure ()
-        _ -> throwElab $ Redefinition (Defined name)
+      define (Defined name 0) ty tm_nf (const k)
+    Just nm -> do
+      ty_nf <- getNfType nm
+      t <- asks (Set.member nm . definedNames)
+      when t $ throwElab (Redefinition (Defined name 0))
 
       rhs <- check rhs ty_nf
       rhs_nf <- eval rhs
-      define (Defined name) ty_nf rhs_nf k
+      define (Defined name 0) ty_nf rhs_nf (const k)
 
 checkStatement (P.Builtin winame var) k = do
   wi <-
@@ -311,7 +316,7 @@ checkStatement (P.Builtin winame var) k = do
   liftIO $
     runElab check env `catch` \(_ :: NotInScope) -> pure ()
 
-  define (Defined var) (wiType wi) (wiValue wi) k
+  define (Defined var 0) (wiType wi) (wiValue wi) (const k)
 
 checkStatement (P.ReplNf e) k = do
   (e, _) <- infer e
diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs
index dbe50fe..60b2886 100644
--- a/src/Elab/Eval.hs
+++ b/src/Elab/Eval.hs
@@ -22,6 +22,8 @@ import Data.Maybe
 import Elab.Eval.Formula
 import Elab.Monad
 
+import GHC.Stack
+
 import Presyntax.Presyntax (Plicity(..))
 
 import Prettyprinter
@@ -32,17 +34,20 @@ import Syntax
 import System.IO.Unsafe
 
 import {-# SOURCE #-} Elab.WiredIn
-import GHC.Stack
 
 eval :: Term -> ElabM Value
 eval t = asks (flip eval' t)
 
 forceIO :: MonadIO m => Value -> m Value
-forceIO mv@(VNe (HMeta (MV id cell)) args) = do
+forceIO mv@(VNe (HMeta (MV _ cell)) args) = do
   solved <- liftIO $ readIORef cell
   case solved of
     Just vl -> forceIO $ foldl applProj vl args
     Nothing -> pure mv
+forceIO vl@(VSystem fs) =
+  case Map.lookup VI1 fs of
+    Just x -> forceIO x
+    Nothing -> pure vl
 forceIO (VComp line phi u a0) = comp line <$> forceIO phi <*> pure u <*> pure a0
 forceIO x = pure x
 
@@ -73,6 +78,7 @@ zonkIO (VNe hd sp) = do
     zonkSp (POuc a phi u) = POuc <$> zonkIO a <*> zonkIO phi <*> zonkIO u
     zonkSp PProj1 = pure PProj1
     zonkSp PProj2 = pure PProj2
+
 zonkIO (VLam p (Closure s k)) = pure $ VLam p (Closure s (zonk . k))
 zonkIO (VPi p d (Closure s k)) = VPi p <$> zonkIO d <*> pure (Closure s (zonk . k))
 zonkIO (VSigma d (Closure s k)) = VSigma <$> zonkIO d <*> pure (Closure s (zonk . k))
@@ -107,6 +113,10 @@ zonkIO (VSub a b c) = VSub <$> zonkIO a <*> zonkIO b <*> zonkIO c
 zonkIO (VInc a b c) = VInc <$> zonkIO a <*> zonkIO b <*> zonkIO c
 zonkIO (VComp a b c d) = comp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d
 
+zonkIO (VGlueTy a phi ty e)   = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e
+zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x
+zonkIO (VUnglue a phi ty e x) = unglue   <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO x
+
 mkVSystem :: Map.Map Value Value -> Value
 mkVSystem map =
   case Map.lookup VI1 map of
@@ -120,22 +130,22 @@ eval' :: ElabEnv -> Term -> Value
 eval' env (Ref x) =
   case Map.lookup x (getEnv env) of
     Just (_, vl) -> vl
-    _ -> VVar x
+    _ -> VNe (HVar x) mempty
 eval' env (App p f x) = vApp p (eval' env f) (eval' env x)
 
 eval' env (Lam p s t) =
   VLam p $ Closure s $ \a ->
-    eval' env { getEnv = Map.insert (Bound s) (error "type of abs", a) (getEnv env) } t
+    eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
 
 eval' env (Pi p s d t) =
   VPi p (eval' env d) $ Closure s $ \a ->
-    eval' env { getEnv = (Map.insert (Bound s) (error "type of abs", a) (getEnv env))} t
+    eval' env { getEnv = (Map.insert s (error "type of abs", a) (getEnv env))} t
 
 eval' _ (Meta m) = VNe (HMeta m) mempty
 
 eval' env (Sigma s d t) =
   VSigma (eval' env d) $ Closure s $ \a ->
-    eval' env { getEnv = Map.insert (Bound s) (error "type of abs", a) (getEnv env) } t
+    eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
 
 eval' e (Pair a b) = VPair (eval' e a) (eval' e b)
 
@@ -171,29 +181,33 @@ eval' e (Ouc a phi u x) = outS (eval' e a) (eval' e phi) (eval' e u) (eval' e x)
 
 eval' e (Comp a phi u a0) = comp (eval' e a) (eval' e phi) (eval' e u) (eval' e a0)
 
+eval' e (GlueTy a phi tys f) = glueType (eval' e a) (eval' e phi) (eval' e tys) (eval' e f)
+eval' e (Glue a phi tys eqvs t x) = glueElem (eval' e a) (eval' e phi) (eval' e tys) (eval' e eqvs) (eval' e t) (eval' e x)
+eval' e (Unglue a phi tys f x) = unglue (eval' e a) (eval' e phi) (eval' e tys) (eval' e f) (eval' e x)
+
 vApp :: HasCallStack => Plicity -> Value -> Value -> Value
 vApp p (VLam p' k) arg
   | p == p'   = clCont k arg
   | otherwise = error $ "wrong plicity " ++ show p ++ " vs " ++ show p' ++ " in app " ++ show (App p (quote (VLam p' k)) (quote arg))
-vApp p (VNe h sp) arg  = VNe h (sp Seq.:|> PApp p arg)
+vApp p (VNe h sp) arg   = VNe h (sp Seq.:|> PApp p arg)
 vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs)
-vApp _ x _             = error $ "can't apply " ++ show x
+vApp _ x _             = error $ "can't apply " ++ show (prettyTm (quote x))
 
 (@@) :: HasCallStack => Value -> Value -> Value
 (@@) = vApp Ex
 infixl 9 @@
 
-vProj1 :: Value -> Value
+vProj1 :: HasCallStack => Value -> Value
 vProj1 (VPair a _) = a
 vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1)
 vProj1 (VSystem fs) = VSystem (fmap vProj1 fs)
-vProj1 x = error $ "can't proj1 " ++ show x
+vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x))
 
-vProj2 :: Value -> Value
+vProj2 :: HasCallStack => Value -> Value
 vProj2 (VPair _ b) = b
 vProj2 (VNe h sp)  = VNe h (sp Seq.:|> PProj2)
 vProj2 (VSystem fs) = VSystem (fmap vProj2 fs)
-vProj2 x = error $ "can't proj2 " ++ show x
+vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))
 
 data NotEqual = NotEqual Value Value
   deriving (Show, Typeable, Exception)
@@ -206,7 +220,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VNe x a) (VNe x' a')
     | x == x', length a == length a' =
       traverse_ (uncurry unify'Spine) (Seq.zip a a')
-    | x == HVar (Bound (T.pack "y")), x' == HVar (Bound (T.pack "A")) = error "what"
 
   go lhs@(VNe _hd (_ Seq.:|> PIElim _l x y i)) rhs =
     case force i of
@@ -225,23 +238,23 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
         _ -> fail
 
   go (VLam p (Closure _ k)) vl = do
-    t <- VVar . Bound <$> newName
+    t <- VVar <$> newName
     unify' (k t) (vApp p vl t)
 
   go vl (VLam p (Closure _ k)) = do
-    t <- VVar . Bound <$> newName
+    t <- VVar <$> newName
     unify' (vApp p vl t) (k t)
 
   go (VPair a b) vl = unify' a (vProj1 vl) *> unify' b (vProj2 vl)
   go vl (VPair a b) = unify' (vProj1 vl) a *> unify' (vProj2 vl) b
 
   go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do
-    t <- VVar . Bound <$> newName
+    t <- VVar <$> newName
     unify' d d'
     unify' (k t) (k' t)
 
   go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do
-    t <- VVar . Bound <$> newName
+    t <- VVar <$> newName
     unify' d d'
     unify' (k t) (k' t)
 
@@ -256,11 +269,11 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     unify' y y'
 
   go (VLine l x y p) p' = do
-    n <- VVar . Bound <$> newName
+    n <- VVar <$> newName
     unify (p @@ n) (ielim l x y p' n)
 
   go p' (VLine l x y p) = do
-    n <- VVar . Bound <$> newName
+    n <- VVar <$> newName
     unify (ielim l x y p' n) (p @@ n)
 
   go (VIsOne x) (VIsOne y) = unify' x y
@@ -282,6 +295,15 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VComp a phi u a0) (VComp a' phi' u' a0') =
     traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
 
+  go (VGlueTy _ VI1 u _0) rhs = unify' (u @@ VItIsOne) rhs
+  go lhs (VGlueTy _ VI1 u _0) = unify' lhs (u @@ VItIsOne)
+
+  go (VGlueTy a phi u a0) (VGlueTy a' phi' u' a0') =
+    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+
+  go (VGlue a phi u a0 t x) (VGlue a' phi' u' a0' t' x') =
+    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, x')]
+
   go (VSystem sys) rhs = goSystem unify' sys rhs
   go rhs (VSystem sys) = goSystem (flip unify') sys rhs
 
@@ -321,29 +343,30 @@ unify :: HasCallStack => Value -> Value -> ElabM ()
 unify a b = unify' a b `catchElab` \(_ :: NotEqual) -> liftIO $ throwIO (NotEqual a b)
 
 isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
-VPi Im d (Closure _v k) `isConvertibleTo` ty = do
-  meta <- newMeta d
-  cont <- k meta `isConvertibleTo` ty
-  pure (\f -> cont (App Im f (quote meta)))
-VType `isConvertibleTo` VTypeω = pure id
-
-VPi p d (Closure _ k) `isConvertibleTo` VPi p' d' (Closure _ k') | p == p' = do
-  wp <- d' `isConvertibleTo` d
-  n <- newName
-  wp_n <- eval (Lam Ex n (wp (Ref (Bound n))))
+isConvertibleTo a b = isConvertibleTo (force a) (force b) where
+  VPi Im d (Closure _v k) `isConvertibleTo` ty = do
+    meta <- newMeta d
+    cont <- k meta `isConvertibleTo` ty
+    pure (\f -> cont (App Im f (quote meta)))
+  VType `isConvertibleTo` VTypeω = pure id
 
-  wp' <- k (VVar (Bound n)) `isConvertibleTo` k' (wp_n @@ VVar (Bound n))
-  pure (\f -> Lam p n (wp' (App p f (wp (Ref (Bound n))))))
+  VPi p d (Closure _ k) `isConvertibleTo` VPi p' d' (Closure _ k') | p == p' = do
+    wp <- d' `isConvertibleTo` d
+    n <- newName
+    wp_n <- eval (Lam Ex n (wp (Ref n)))
 
-isConvertibleTo a b = do
-  unify' a b
-  pure id
+    wp' <- k (VVar n) `isConvertibleTo` k' (wp_n @@ VVar n)
+    pure (\f -> Lam p n (wp' (App p f (wp (Ref n)))))
+
+  isConvertibleTo a b = do
+    unify' a b
+    pure id
 
 newMeta :: Value -> ElabM Value
 newMeta _dom = do
   n <- newName
   c <- liftIO $ newIORef Nothing
-  let m = MV n c
+  let m = MV (getNameText n) c
 
   env <- asks getEnv
 
@@ -354,10 +377,10 @@ newMeta _dom = do
 
   pure (VNe (HMeta m) (Seq.fromList (catMaybes t)))
 
-newName :: MonadIO m => m T.Text
+newName :: MonadIO m => m Name
 newName = liftIO $ do
   x <- atomicModifyIORef _nameCounter $ \x -> (x + 1, x + 1)
-  pure (T.pack (show x))
+  pure (Bound (T.pack (show x)) x)
 
 _nameCounter :: IORef Int
 _nameCounter = unsafePerformIO $ newIORef 0
@@ -367,7 +390,7 @@ solveMeta :: MV -> Seq Projection -> Value -> ElabM ()
 solveMeta m@(MV _ cell) sp rhs = do
   env <- ask
   names <- checkSpine Set.empty sp
-  checkScope (Set.fromList (Bound <$> names)) rhs
+  checkScope (Set.fromList names) rhs
     `withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)]
   let tm = quote rhs
       lam = eval' env $ foldr (Lam Ex) tm names
@@ -393,15 +416,15 @@ checkScope scope (VNe h sp) =
     checkProj PProj2 = pure ()
 
 checkScope scope (VLam _ (Closure n k)) =
-  checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n)))
+  checkScope (Set.insert n scope) (k (VVar n))
 
 checkScope scope (VPi _ d (Closure n k)) = do
   checkScope scope d
-  checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n)))
+  checkScope (Set.insert n scope) (k (VVar n))
 
 checkScope scope (VSigma d (Closure n k)) = do
   checkScope scope d
-  checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n)))
+  checkScope (Set.insert n scope) (k (VVar n))
 
 checkScope s (VPair a b) = traverse_ (checkScope s) [a, b]
 
@@ -433,10 +456,14 @@ checkScope s (VSub a b c) = traverse_ (checkScope s) [a, b, c]
 checkScope s (VInc a b c) = traverse_ (checkScope s) [a, b, c]
 checkScope s (VComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0]
 
-checkSpine :: Set Name -> Seq Projection -> ElabM [T.Text]
-checkSpine scope (PApp Ex (VVar n@(Bound t)) Seq.:<| xs)
+checkScope s (VGlueTy a phi ty eq) = traverse_ (checkScope s) [a, phi, ty, eq]
+checkScope s (VGlue a phi ty eq inv x) = traverse_ (checkScope s) [a, phi, ty, eq, inv, x]
+checkScope s (VUnglue a phi ty eq vl) = traverse_ (checkScope s) [a, phi, ty, eq, vl]
+
+checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
+checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
   | n `Set.member` scope = throwElab $ NonLinearSpine n
-  | otherwise = (t:) <$> checkSpine scope xs
+  | otherwise = (n:) <$> checkSpine scope xs
 checkSpine _     (p Seq.:<| _) = throwElab $ SpineProj p
 checkSpine _     Seq.Empty = pure []
 
@@ -444,4 +471,4 @@ newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
   deriving (Show, Typeable, Exception)
 
 newtype SpineProjection = SpineProj { getSpineProjection :: Projection }
-  deriving (Show, Typeable, Exception)
\ No newline at end of file
+  deriving (Show, Typeable, Exception)
diff --git a/src/Elab/Eval/Formula.hs b/src/Elab/Eval/Formula.hs
index 274f422..ae95e7a 100644
--- a/src/Elab/Eval/Formula.hs
+++ b/src/Elab/Eval/Formula.hs
@@ -56,7 +56,7 @@ possible sc VI1 = (True, sc)
 possible sc _ = (False, sc)
 
 truthAssignments :: NFEndp -> Map Name (NFType, NFEndp) -> [Map Name (NFType, NFEndp)]
-truthAssignments VI0 m = []
+truthAssignments VI0 _ = []
 truthAssignments VI1 m = pure m
 truthAssignments (VIOr x y) m = truthAssignments x m ++ truthAssignments y m
 truthAssignments (VIAnd x y) m = truthAssignments x =<< truthAssignments y m
diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs
index 438f19a..eafe2a2 100644
--- a/src/Elab/Monad.hs
+++ b/src/Elab/Monad.hs
@@ -12,11 +12,11 @@ import qualified Data.Map.Strict as Map
 import Data.Text.Prettyprint.Doc
 import Data.Map.Strict (Map)
 import Data.Text (Text)
+import Data.Set (Set)
 import Data.Typeable
 
 import qualified Presyntax.Presyntax as P
 
-import Syntax.Pretty (getNameText)
 import Syntax
 
 data ElabEnv =
@@ -28,6 +28,7 @@ data ElabEnv =
 
           , currentSpan :: Maybe (P.Posn, P.Posn)
           , whereBound  :: Map Name (P.Posn, P.Posn)
+          , definedNames :: Set Name
           }
 
 newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
@@ -35,25 +36,45 @@ newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
     via ReaderT ElabEnv IO
 
 emptyEnv :: ElabEnv
-emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing mempty
+emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing mempty mempty
 
-assume :: Name -> Value -> ElabM a -> ElabM a
-assume nm ty = local go where
-  go x = x { getEnv = Map.insert nm (ty, VVar nm) (getEnv x)
-           , nameMap = Map.insert (getNameText nm) nm (nameMap x)
-           , whereBound = maybe (whereBound x) (flip (Map.insert nm) (whereBound x)) (currentSpan x)
-           }
+assume :: Name -> Value -> (Name -> ElabM a) -> ElabM a
+assume nm ty k = defineInternal nm ty VVar k
 
-assumes :: [Name] -> Value -> ElabM a -> ElabM a
-assumes nm ty = local go where
-  go x = x { getEnv = Map.union (Map.fromList (map (\v -> (v, (ty, VVar v))) nm)) (getEnv x)
-           , nameMap = Map.union (Map.fromList (map ((,) <$> getNameText <*> id) nm)) (nameMap x)
-           , whereBound = maybe (whereBound x) (\l -> Map.union (Map.fromList (zip nm (repeat l))) (whereBound x)) (currentSpan x)
-           }
+define :: Name -> Value -> Value -> (Name -> ElabM a) -> ElabM a
+define nm vty val = defineInternal nm vty (const val)
+
+assumes :: [Name] -> Value -> ([Name] -> ElabM a) -> ElabM a
+assumes nms ty k = do
+  let
+    go acc [] k = k acc
+    go acc (x:xs) k = assume x ty $ \n -> go (n:acc) xs k
+   in go [] nms  k
 
-define :: Name -> Value -> Value -> ElabM a -> ElabM a
-define nm ty vl = local go where
-  go x = x { getEnv = Map.insert nm (ty, vl) (getEnv x), nameMap = Map.insert (getNameText nm) nm (nameMap x) }
+defineInternal :: Name -> Value -> (Name -> Value) -> (Name -> ElabM a) -> ElabM a
+defineInternal nm vty val k =
+  do
+    env <- ask
+    let (env', name') = go env
+    local (const env') (k name')
+  where
+    go x =
+      let
+        nm' = case Map.lookup (getNameText nm) (nameMap x) of
+          Just name -> incName nm name
+          Nothing -> nm
+      in ( x { getEnv     = Map.insert nm' (vty, val nm') (getEnv x)
+             , nameMap    = Map.insert (getNameText nm) nm' (nameMap x)
+             , whereBound = maybe (whereBound x) (flip (Map.insert nm') (whereBound x)) (currentSpan x)
+             }
+         , nm')
+
+redefine :: Name -> Value -> Value -> ElabM a -> ElabM a
+redefine nm vty val = local go where
+  go x = x { getEnv     = Map.insert nm (vty, val) (getEnv x)
+           , nameMap    = Map.insert (getNameText nm) nm (nameMap x)
+           , whereBound = maybe (whereBound x) (flip (Map.insert nm) (whereBound x)) (currentSpan x)
+           }
 
 getValue :: Name -> ElabM Value
 getValue nm = do
@@ -74,7 +95,7 @@ getNameFor x = do
   vl <- asks (Map.lookup x . nameMap)
   case vl of
     Just v -> pure v
-    Nothing -> liftIO . throwIO $ NotInScope (Bound x)
+    Nothing -> liftIO . throwIO $ NotInScope (Bound x 0)
 
 switch :: ElabM a -> ElabM a
 switch k =
@@ -135,3 +156,7 @@ tryElab k = do
 
 throwElab :: Exception e => e -> ElabM a
 throwElab = liftIO . throwIO
+
+incName :: Name -> Name -> Name
+incName (Bound x _) n = Bound x (getNameNum n + 1)
+incName (Defined x k) n = Defined x (getNameNum n + 1)
diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs
index 36ed945..5e36794 100644
--- a/src/Elab/WiredIn.hs
+++ b/src/Elab/WiredIn.hs
@@ -6,16 +6,22 @@
 {-# LANGUAGE ViewPatterns #-}
 module Elab.WiredIn where
 
-import Syntax
+import Control.Exception
+
+import qualified Data.Map.Strict as Map
+import qualified Data.Sequence as Seq
+import qualified Data.Text as T
 import Data.Map.Strict (Map)
 import Data.Text (Text)
-import qualified Data.Map.Strict as Map
-import Control.Exception
 import Data.Typeable
-import qualified Presyntax.Presyntax as P
+
 import Elab.Eval
-import qualified Data.Sequence as Seq
-import qualified Data.Text as T
+
+import qualified Presyntax.Presyntax as P
+
+import Syntax
+
+import System.IO.Unsafe
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -28,7 +34,7 @@ wiType WiI1       = VI
 wiType WiIAnd     = VI ~> VI ~> VI
 wiType WiIOr      = VI ~> VI ~> VI
 wiType WiINot     = VI ~> VI
-wiType WiPathP    = dprod (VI ~> VTypeω) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
+wiType WiPathP    = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
 
 wiType WiIsOne    = VI ~> VTypeω
 wiType WiItIsOne  = VIsOne VI1
@@ -39,10 +45,17 @@ wiType WiPartial  = VI ~> VType ~> VTypeω
 wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω
 
 wiType WiSub      = dprod VType \a -> dprod VI \phi -> VPartial phi a ~> VTypeω
-wiType WiInS      = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (VLam P.Ex (Closure "x" (const u)))
+wiType WiInS      = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (fun (const u))
 wiType WiOutS     = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a) \u -> VSub a phi u ~> a
 
-wiType WiComp     = dprod (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
+wiType WiComp     = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
+-- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
+wiType WiGlue     = dprod' "A" VType \a -> forAll' "phi" VI \phi -> dprod' "T" (VPartial phi VType) \t -> VPartialP phi (fun \o -> equiv (t @@ o) a) ~> VType
+-- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
+wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \eqv ->
+  dprod' "t" (VPartialP phi ty) \t -> VSub a phi (fun \o -> vProj1 (eqv @@ o) @@ (t @@ o)) ~> VGlueTy a phi ty eqv
+-- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
+wiType WiUnglue = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \e -> VGlueTy a phi ty e ~> a
 
 wiValue :: WiredIn -> Value
 wiValue WiType     = VType
@@ -67,24 +80,41 @@ wiValue WiPartialP = fun \phi -> fun \r -> VPartialP phi r
 wiValue WiSub      = fun \a -> fun \phi -> fun \u -> VSub a phi u
 wiValue WiInS      = forallI \a -> forallI \phi -> fun \u -> VInc a phi u
 wiValue WiOutS     = forallI \a -> forallI \phi -> forallI \u -> fun \x -> outS a phi u x
--- wiValue WiComp     = forAll (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
 wiValue WiComp     = fun \a -> forallI \phi -> fun \u -> fun \x -> comp a phi u x
 
+wiValue WiGlue     = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a phi t e
+wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y
+wiValue WiUnglue   = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> unglue a phi ty eqv x
+
 (~>) :: Value -> Value -> Value
-a ~> b = VPi P.Ex a (Closure "_" (const b))
+a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b))
 infixr 7 ~>
 
-fun :: (Value -> Value) -> Value
-fun k = VLam P.Ex $ Closure "x" (k . force)
+fun, line :: (Value -> Value) -> Value
+fun k = VLam P.Ex $ Closure (Bound "x" 0) (k . force)
+line k = VLam P.Ex $ Closure (Bound "i" 0) (k . force)
 
 forallI :: (Value -> Value) -> Value
-forallI k = VLam P.Im $ Closure "x" (k . force)
+forallI k = VLam P.Im $ Closure (Bound "x" 0) (k . force)
+
+dprod' :: String -> Value -> (Value -> Value) -> Value
+dprod' t a b = VPi P.Ex a (Closure (Bound (T.pack t) 0) b)
 
 dprod :: Value -> (Value -> Value) -> Value
-dprod a b = VPi P.Ex a (Closure "x" b)
+dprod = dprod' "x"
+
+exists' :: String -> Value -> (Value -> Value) -> Value
+exists' s a b = VSigma a (Closure (Bound (T.pack s) 0) b)
+
+exists :: Value -> (Value -> Value) -> Value
+exists = exists' "x"
+
+forAll' :: String -> Value -> (Value -> Value) -> Value
+forAll' n a b = VPi P.Im a (Closure (Bound (T.pack n) 0) b)
 
 forAll :: Value -> (Value -> Value) -> Value
-forAll a b = VPi P.Im a (Closure "x" b)
+forAll = forAll' "x"
+
 
 wiredInNames :: Map Text WiredIn
 wiredInNames = Map.fromList
@@ -97,7 +127,7 @@ wiredInNames = Map.fromList
   , ("ior",  WiIOr)
   , ("inot", WiINot)
   , ("PathP", WiPathP)
-  
+
   , ("IsOne", WiIsOne)
   , ("itIs1", WiItIsOne)
   , ("isOneL", WiIsOne1)
@@ -110,6 +140,9 @@ wiredInNames = Map.fromList
   , ("outS", WiOutS)
 
   , ("comp", WiComp)
+  , ("Glue", WiGlue)
+  , ("glue", WiGlueElem)
+  , ("unglue", WiUnglue)
   ]
 
 newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
@@ -157,20 +190,24 @@ ielim _line _left _right fn i =
   case force fn of
     VLine _ _ _ fun -> fun @@ i
     VNe n sp -> VNe n (sp Seq.:|> PIElim _line _left _right i)
+    VSystem (Map.toList -> []) -> VSystem (Map.fromList [])
     _ -> error $ "can't ielim " ++ show fn
 
 outS :: NFSort -> NFEndp -> Value -> Value -> Value
 outS _ (force -> VI1) u _  = u @@ VItIsOne
-outS _ _phi _ (VInc _ _ x) = x 
-outS a phi u  (VNe x sp)   = VNe x (sp Seq.:|> POuc a phi u)
-outS _ _ _ v               = error $ "can't outS " ++ show v
+
+outS _ _phi _ (VInc _ _ x) = x
+outS _ VI0 _  x            = x
+
+outS a phi u  (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
+outS _ _ _ v             = error $ "can't outS " ++ show v
 
 -- Composition
 comp :: NFLine -> NFEndp -> Value -> Value -> Value
 comp _ VI1 u _ = u @@ VI1 @@ VItIsOne
-comp a phi u (VInc _ _ a0) =
-  case a @@ VNe (HVar (Bound (T.pack "x"))) Seq.empty of
-    VPi{} -> 
+comp a psi@phi u (outS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
+  case force $ a @@ VVar (Bound (T.pack "neutral composition") 0) of
+    VPi{} ->
       let
         plic i = let VPi p _ _ = a @@ i in p
         dom  i = let VPi _ d _ = a @@ i in d
@@ -178,7 +215,7 @@ comp a phi u (VInc _ _ a0) =
 
         y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i
         ybar i y = y' (inot i) y
-       in VLam (plic VI1) . Closure "x" $ \arg ->
+       in VLam (plic VI1) . Closure (Bound "x" 0) $ \arg ->
               comp (fun \i -> rng i (ybar i arg))
                    phi
                    (system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg))
@@ -193,6 +230,7 @@ comp a phi u (VInc _ _ a0) =
         c2 = comp (fun (($ w VI1) . rng)) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (rng VI0 (dom VI0)) phi (vProj2 a0))
        in
          VPair c1 c2
+
     VPath{} ->
       let
         a' i = let VPath a _ _ = a @@ i in a
@@ -207,8 +245,45 @@ comp a phi u (VInc _ _ a0) =
                                                         , (inot j, u' i)]))
             (VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
 
+    VGlueTy{} ->
+      let
+        b = u
+        b0 = a0
+        fam = a
+      in
+      let
+        base i    = let VGlueTy base _ _ _   = fam @@ i in base
+        phi i     = let VGlueTy _ phi  _ _   = fam @@ i in phi
+        types i   = let VGlueTy _ _ types _  = fam @@ i in types
+        equivs i  = let VGlueTy _ _ _ equivs = fam @@ i in equivs
+
+        a i = fun \u -> unglue (base i) (phi i) (types i @@ u) (equivs i @@ u) (b @@ i @@ u)
+        a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
+
+        del = faceForall phi
+        a1' = comp (line base) psi (line a) (VInc undefined undefined a0)
+        t1' = comp (line types) psi (line (b @@)) (VInc undefined undefined b0)
+
+        (omega_st, omega_t, omega_rep) = pres types base equivs psi (b @@) b0
+        omega = outS omega_t psi omega_rep omega_st
+
+        (t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1 @@ VItIsOne) (equivs VI1 @@ VItIsOne) (del `ior` psi) (fun ts) (fun ps) a1'
+        t1alpha = outS t1a_t (del `ior` psi) t1a_rep t1alpha_st
+
+        (t1, alpha) = (vProj1 t1alpha, vProj2 t1alpha)
+
+        ts isone = mkVSystem . Map.fromList $ [(del, t1'), (psi, (b @@ VI1 @@ isone))]
+        ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))]
+
+        a1 = comp
+          (fun (const (base VI1 @@ VItIsOne)))
+          (phi VI1 `ior` psi)
+          (system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VItIsOne)) alpha j)
+                                                  , (psi, a VI1)]))
+          a1'
+        b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1
+       in b1
     _ -> VComp a phi u a0
-comp a phi u a0 = VComp a phi u a0
 
 system :: (Value -> Value -> Value) -> Value
 system k = fun \i -> fun \isone -> k i isone
@@ -219,4 +294,71 @@ fill a phi u a0 j =
        (phi `ior` inot j)
        (fun \i -> fun \isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone)
                                                         , (inot j, a0)]))
-       a0
\ No newline at end of file
+       a0
+
+glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
+glueType a phi tys eqvs = VGlueTy a phi tys eqvs
+
+glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
+glueElem _a VI1 _tys _eqvs t _vl = t @@ VItIsOne
+glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
+
+unglue   :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
+unglue _a VI1 _tys eqvs x = vProj1 (eqvs @@ VItIsOne) @@ x
+unglue _a _phi _tys _eqvs (VGlue _ _ _ _ _ vl) = vl
+unglue _ _ _ _ (VSystem (Map.toList -> [])) = VSystem (Map.fromList [])
+unglue a phi tys eqvs vl = VUnglue a phi tys eqvs vl
+
+-- Definition of equivalences
+
+faceForall :: (NFEndp -> NFEndp) -> Value
+faceForall phi = T.length (getNameText name) `seq` go (phi (VVar name)) where
+  {-# NOINLINE name #-}
+  name = unsafePerformIO newName
+
+  go x@(VVar n)
+    | n == name = VI0
+    | otherwise = x
+  go x@(VINot (VVar n))
+    | n == name = VI0
+    | otherwise = x
+  go (VIAnd x y) = iand (go x) (go y)
+  go (VIOr x y) = ior (go x) (go y)
+  go (VINot x) = inot (go x)
+  go vl = vl
+
+isContr :: Value -> Value
+isContr a = exists' "x" a \x -> dprod' "y" a \y -> VPath (line (const a)) x y
+
+fiber :: NFSort -> NFSort -> Value -> Value -> Value
+fiber a b f y = exists' "x" a \x -> VPath (line (const b)) (f @@ x) y
+
+isEquiv :: NFSort -> NFSort -> Value -> Value
+isEquiv a b f = dprod' "y" b \y -> isContr (fiber a b f y)
+
+equiv :: NFSort -> NFSort -> Value
+equiv a b = exists' "f" (a ~> b) \f -> isEquiv a b f
+
+pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value)
+pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), pathT, fun $ \u -> VLine (fun (const (tyA VI1))) c1 c2 (fun (const (f VI1 @@ (t VI1 @@ u))))) where
+  pathT = VPath (fun (const (tyA VI1))) c1 c2
+  c1 = comp (fun tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0))
+  c2 = f VI1 @@ comp (fun tyT) phi (system \i u -> t i @@ u) t0
+
+  a0 = f VI0 @@ t0
+  v = fill (fun tyT) phi (system \i u -> t i @@ u) t0
+
+  path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) a0
+
+opEquiv :: Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
+opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
+  fn = vProj1 f
+  ty  = exists' "f" tT \x -> VPath (line (const aT)) a (fn @@ x)
+  v   = contr ty (vProj2 f @@ a) phi (\u -> VPair (t @@ u) (p @@ u))
+
+contr :: Value -> Value -> NFEndp -> (Value -> Value) -> Value
+contr a aC phi u =
+  comp (line (const a))
+    phi
+    (system \i is1 -> ielim (line (const a)) a (vProj1 (u is1)) (vProj2 (u is1)) i)
+    (vProj1 aC)
diff --git a/src/Elab/WiredIn.hs-boot b/src/Elab/WiredIn.hs-boot
index 20a5b57..b3b6545 100644
--- a/src/Elab/WiredIn.hs-boot
+++ b/src/Elab/WiredIn.hs-boot
@@ -10,4 +10,8 @@ inot      :: NFEndp -> NFEndp
 ielim     :: NFSort -> Value -> Value -> Value -> NFEndp -> Value
 
 outS :: NFSort -> NFEndp -> Value -> Value -> Value
-comp :: NFLine -> NFEndp -> Value -> Value -> Value
\ No newline at end of file
+comp :: NFLine -> NFEndp -> Value -> Value -> Value
+
+glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
+glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
+unglue   :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
\ No newline at end of file
diff --git a/src/Main.hs b/src/Main.hs
index afaf45c..9140b90 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -3,7 +3,10 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 module Main where
 
+import Control.Monad.IO.Class
+import Control.Monad.Reader
 import Control.Exception
+import Control.Monad
 
 import qualified Data.ByteString.Lazy as Bsl
 import qualified Data.Text.Encoding as T
@@ -14,23 +17,23 @@ import Data.Text ( Text )
 import Data.Foldable
 
 import Elab.Monad hiding (switch)
+import Elab.WiredIn
 import Elab.Eval
 import Elab
 
+import Options.Applicative
+
 import Presyntax.Presyntax (Posn(Posn))
 import Presyntax.Parser
 import Presyntax.Lexer
 
-import System.Exit
+import Prettyprinter
+
 import Syntax.Pretty
-import Elab.WiredIn
-import Options.Applicative
-import Control.Monad
 import Syntax
-import Prettyprinter
-import Control.Monad.IO.Class
-import Control.Monad.Reader
+
 import System.Console.Haskeline
+import System.Exit
 
 main :: IO ()
 main = do
@@ -80,7 +83,7 @@ checkFiles files = runElab (go files ask) emptyEnv where
 
 dumpEnv :: Map.Map Name (NFType, Value) -> IO ()
 dumpEnv env = for_ (Map.toList env) $ \(name, (nft, _)) ->
-  T.putStrLn $ render (pretty name <+> colon <+> prettyTm (quote (zonk nft)))
+  T.putStrLn $ render (pretty name <+> align (nest (negate 1) (colon <+> prettyTm (quote (zonk nft)))))
 
 parser :: ParserInfo Opts
 parser = info (subparser (load <> check) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
@@ -152,4 +155,4 @@ squiggleUnder (Posn l c) (Posn l' c') file
       squiggle = T.replicate c " " <> T.pack "\x1b[1;31m" <> T.replicate (c' - c) "~" <> T.pack "\x1b[0m"
 
      in T.unlines [ padding, line, padding <> squiggle ]
-  | otherwise = T.pack (show (Posn l c, Posn l' c'))
\ No newline at end of file
+  | otherwise = T.pack (show (Posn l c, Posn l' c'))
diff --git a/src/Presyntax/Presyntax.hs b/src/Presyntax/Presyntax.hs
index 581cef3..39b20fc 100644
--- a/src/Presyntax/Presyntax.hs
+++ b/src/Presyntax/Presyntax.hs
@@ -1,11 +1,12 @@
+{-# LANGUAGE DeriveDataTypeable #-}
 module Presyntax.Presyntax where
 
-
 import Data.Text (Text)
+import Data.Data
 
 data Plicity
   = Im | Ex
-  deriving (Eq, Show, Ord)
+  deriving (Eq, Show, Ord, Data)
 
 data Expr
   = Var Text
@@ -53,4 +54,4 @@ data Posn
   = Posn { posnLine :: {-# UNPACK #-} !Int
          , posnColm :: {-# UNPACK #-} !Int
          }
-  deriving (Eq, Show, Ord)
\ No newline at end of file
+  deriving (Eq, Show, Ord)
diff --git a/src/Presyntax/Tokens.hs b/src/Presyntax/Tokens.hs
index 07e6222..2f32aa4 100644
--- a/src/Presyntax/Tokens.hs
+++ b/src/Presyntax/Tokens.hs
@@ -1,7 +1,7 @@
 module Presyntax.Tokens where
 
-import Data.Text (Text)
 import qualified Data.Text as T
+import Data.Text (Text)
 
 data TokenClass
   = TokVar Text
@@ -75,4 +75,4 @@ data Token
           , tokStartLine :: !Int
           , tokStartCol  :: !Int
           }
-  deriving (Eq, Show, Ord)
\ No newline at end of file
+  deriving (Eq, Show, Ord)
diff --git a/src/Syntax.hs b/src/Syntax.hs
index b3d98e2..899c0bb 100644
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@@ -1,18 +1,20 @@
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE DeriveDataTypeable #-}
 module Syntax where
 
+import qualified Data.Map.Strict as Map
+import qualified Data.Sequence as Seq
+import qualified Data.Set as Set
+import qualified Data.Text as T
+import Data.Map.Strict (Map)
+import Data.Sequence (Seq)
 import Data.Function (on)
+import Data.IORef (IORef)
 import Data.Text (Text)
+import Data.Set (Set)
+import Data.Data
 
 import Presyntax.Presyntax (Plicity(..))
-import qualified Data.Text as T
-import Data.IORef (IORef)
-import Data.Set (Set)
-import qualified Data.Set as Set
-import Data.Sequence (Seq)
-import qualified Data.Sequence as Seq
-import Data.Map.Strict (Map)
-import qualified Data.Map.Strict as Map
 
 data WiredIn
   = WiType
@@ -40,18 +42,22 @@ data WiredIn
   | WiComp  --    {A : I -> Type} {phi : I}
             -- -> ((i : I) -> Partial phi (A i)
             -- -> (A i0)[phi -> u i0] -> (A i1)[phi -> u i1]
+
+  | WiGlue      -- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
+  | WiGlueElem  -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
+  | WiUnglue    -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
   deriving (Eq, Show, Ord)
 
 data Term
   = Ref  Name
   | App  Plicity Term Term
-  | Lam  Plicity Text Term
-  | Pi   Plicity Text Term Term
+  | Lam  Plicity Name Term
+  | Pi   Plicity Name Term Term
   | Meta MV
   | Type
   | Typeω
 
-  | Sigma Text Term Term
+  | Sigma Name Term Term
   | Pair Term Term
   | Proj1 Term
   | Proj2 Term
@@ -85,7 +91,11 @@ data Term
   | Ouc Term Term Term Term
 
   | Comp Term Term Term Term
-  deriving (Eq, Show, Ord)
+
+  | GlueTy Term Term Term Term
+  | Glue Term Term Term Term Term Term
+  | Unglue Term Term Term Term Term
+  deriving (Eq, Show, Ord, Data)
 
 data MV =
   MV { mvName :: Text
@@ -99,15 +109,22 @@ instance Ord MV where
 instance Show MV where
   show = ('?':) . T.unpack . mvName
 
+instance Data MV where
+  toConstr _   = error "toConstr"
+  gunfold _ _  = error "gunfold"
+  dataTypeOf _ = mkNoRepType "MV"
+
+
 data Name
-  = Bound   Text
-  | Defined Text
-  deriving (Eq, Show, Ord)
+  = Bound   {getNameText :: Text, getNameNum :: !Int}
+  | Defined {getNameText :: Text, getNameNum :: !Int}
+  deriving (Eq, Show, Ord, Data)
 
 type NFType = Value
 type NFEndp = Value
 type NFLine = Value
 type NFSort = Value
+type NFPartial = Value
 
 data Value
   = VNe    Head (Seq Projection)
@@ -140,12 +157,16 @@ data Value
   | VInc NFSort NFEndp Value
 
   | VComp NFSort NFEndp Value Value
+
+  | VGlueTy NFSort NFEndp NFPartial NFPartial
+  | VGlue   NFSort NFEndp NFPartial NFPartial NFPartial Value
+  | VUnglue NFSort NFEndp NFPartial NFPartial Value
   deriving (Eq, Show, Ord)
 
 pattern VVar :: Name -> Value
 pattern VVar x = VNe (HVar x) Seq.Empty
 
-quoteWith :: Set Text -> Value -> Term
+quoteWith :: Set Name -> Value -> Term
 quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
   goHead (HVar v) = Ref v
   goHead (HMeta m) = Meta m
@@ -158,15 +179,15 @@ quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
 
 quoteWith names (VLam p (Closure n k)) =
   let n' = refresh Nothing names n
-   in Lam p n' (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
+   in Lam p n' (quoteWith (Set.insert n' names) (k (VVar n')))
 
 quoteWith names (VPi p d (Closure n k)) =
   let n' = refresh (Just d) names n
-   in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
+   in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
 
 quoteWith names (VSigma d (Closure n k)) =
   let n' = refresh (Just d) names n
-   in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
+   in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
 
 quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
 quoteWith _ VType = Type
@@ -194,32 +215,36 @@ quoteWith names (VSub a b c) = Sub (quoteWith names a) (quoteWith names b) (quot
 quoteWith names (VInc a b c) = Inc (quoteWith names a) (quoteWith names b) (quoteWith names c)
 quoteWith names (VComp a phi u a0) = Comp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
 
-refresh :: Maybe Value -> Set Text -> Text -> Text
-refresh (Just VI) n _ = refresh Nothing n (T.pack "phi")
+quoteWith names (VGlueTy a phi t e)    = GlueTy (quoteWith names a) (quoteWith names phi) (quoteWith names t) (quoteWith names e)
+quoteWith names (VGlue a phi ty e t x) = Glue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names t) (quoteWith names x)
+quoteWith names (VUnglue a phi ty e x) = Unglue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names x)
+
+refresh :: Maybe Value -> Set Name -> Name -> Name
+refresh (Just VI) n _ = refresh Nothing n (Bound (T.pack "phi") 0)
 refresh x s n
-  | T.singleton '_' == n = n
+  | T.singleton '_' == getNameText n = n
   | n `Set.notMember` s = n
-  | otherwise = refresh x s (n <> T.singleton '\'')
+  | otherwise = refresh x s (Bound (getNameText n <> T.singleton '\'') 0)
 
 quote :: Value -> Term
 quote = quoteWith mempty
 
 data Closure
   = Closure
-    { clArgName :: Text
+    { clArgName :: Name
     , clCont    :: Value -> Value
     }
 
 instance Show Closure where
-  show (Closure n c) = "Closure \\" ++ show n ++ " -> " ++ show (c (VVar (Bound n)))
+  show (Closure n c) = "Closure \\" ++ show n ++ " -> " ++ show (c (VVar n))
 
 instance Eq Closure where
   Closure _ k == Closure _ k' =
-    k (VVar (Bound (T.pack "_"))) == k' (VVar (Bound (T.pack "_")))
+    k (VVar (Bound (T.pack "_") 0)) == k' (VVar (Bound (T.pack "_") 0))
 
 instance Ord Closure where
   Closure _ k <= Closure _ k' =
-    k (VVar (Bound (T.pack "_"))) <= k' (VVar (Bound (T.pack "_")))
+    k (VVar (Bound (T.pack "_") 0)) <= k' (VVar (Bound (T.pack "_") 0))
 
 data Head
   = HVar Name
@@ -231,5 +256,5 @@ data Projection
   | PIElim Value Value Value NFEndp
   | PProj1
   | PProj2
-  | POuc   NFSort NFEndp Value 
-  deriving (Eq, Show, Ord)
\ No newline at end of file
+  | POuc   NFSort NFEndp Value
+  deriving (Eq, Show, Ord)
diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs
index 60e083d..12874e2 100644
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@@ -4,9 +4,12 @@ module Syntax.Pretty where
 
 import Control.Arrow (Arrow(first))
 
+import qualified Data.Map.Strict as Map
 import qualified Data.Text.Lazy as L
 import qualified Data.Text as T
+import Data.Map.Strict (Map)
 import Data.Text (Text)
+import Data.Generics
 
 import Presyntax.Presyntax (Plicity(..))
 
@@ -14,72 +17,81 @@ import Prettyprinter.Render.Terminal
 import Prettyprinter
 
 import Syntax
-import Data.Map.Strict (Map)
-import qualified Data.Map.Strict as Map
 
 instance Pretty Name where
-  pretty (Bound x)     = pretty x
-  pretty (Defined x)   = pretty x
+  pretty (Bound x _)   = pretty x
+  pretty (Defined x _) = pretty x
 
 prettyTm :: Term -> Doc AnsiStyle
-prettyTm (Ref v) =
-  case T.uncons (getNameText v) of
-    Just ('.', w) -> keyword (pretty w)
-    _ -> pretty v
+prettyTm = prettyTm . everywhere (mkT beautify) where
+  prettyTm (Ref v) =
+    case T.uncons (getNameText v) of
+      Just ('.', w) -> keyword (pretty w)
+      _ -> pretty v
 
-prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x)
-prettyTm (App Ex f x) = parenFun f <+> parenArg x
+  prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x)
+  prettyTm (App Ex f x) = parenFun f <+> parenArg x
 
-prettyTm (Pair x y) = parens $ prettyTm x <> operator comma <+> prettyTm y
-prettyTm (Proj1 x) = prettyTm x <> operator (pretty ".1")
-prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
+  prettyTm (Pair x y) = parens $ prettyTm x <> operator comma <+> prettyTm y
+  prettyTm (Proj1 x) = prettyTm x <> operator (pretty ".1")
+  prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
 
-prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> prettyTm bod where
-  unwindLam (Lam p x y) = first ((p, x):) (unwindLam y)
-  unwindLam (PathIntro _ _ _ (Lam p x y)) = first ((p, x):) (unwindLam y)
-  unwindLam t = ([], t)
+  prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> prettyTm bod where
+    unwindLam (Lam p x y) = first ((p, x):) (unwindLam y)
+    unwindLam (PathIntro _ _ _ (Lam p x y)) = first ((p, x):) (unwindLam y)
+    unwindLam t = ([], t)
 
-  (al, bod) = unwindLam l
+    (al, bod) = unwindLam l
 
-  prettyArgList (Ex, v) = pretty v
-  prettyArgList (Im, v) = braces (pretty v)
+    prettyArgList (Ex, v) = pretty v
+    prettyArgList (Im, v) = braces (pretty v)
 
-prettyTm (Meta x) = keyword $ pretty '?' <> pretty (mvName x)
-prettyTm Type{}  = keyword $ pretty "Type"
-prettyTm Typeω{} = keyword $ pretty "Typeω"
-prettyTm I{}     = keyword $ pretty "I"
-prettyTm I0{}    = keyword $ pretty "i0"
-prettyTm I1{}    = keyword $ pretty "i1"
+  prettyTm (Meta x) = keyword $ pretty '?' <> pretty (mvName x)
+  prettyTm Type{}  = keyword $ pretty "Type"
+  prettyTm Typeω{} = keyword $ pretty "Typeω"
+  prettyTm I{}     = keyword $ pretty "I"
+  prettyTm I0{}    = keyword $ pretty "i0"
+  prettyTm I1{}    = keyword $ pretty "i1"
 
-prettyTm (Pi Ex (T.unpack -> "_") d r) = prettyDom d <+> pretty "->" <+> prettyTm r
-prettyTm (Pi Im v d r)                 = braces (pretty v <+> colon <+> prettyTm d) <+> pretty "->" <+> prettyTm r
-prettyTm (Pi Ex v d r)                 = parens (pretty v <+> colon <+> prettyTm d) <+> pretty "->" <+> prettyTm r
+  prettyTm (Pi Ex (T.unpack . getNameText -> "_") d r) = prettyDom d <+> pretty "->" <+> prettyTm r
+  prettyTm (Pi Im v d r)                 = group (braces (pretty v <+> colon <+> prettyTm d)) <> softline <> pretty "->" <+> prettyTm r
+  prettyTm (Pi Ex v d r)                 = group (parens (pretty v <+> colon <+> prettyTm d)) <> softline <> pretty "->" <+> prettyTm r
 
-prettyTm (Sigma (T.unpack -> "_") d r) = prettyDom d <+> pretty "*" <+> prettyTm r
-prettyTm (Sigma v d r)                 = parens (pretty v <+> colon <+> prettyTm d) <+> pretty "*" <+> prettyTm r
+  prettyTm (Sigma (T.unpack . getNameText -> "_") d r) = prettyDom d <+> pretty "*" <+> prettyTm r
+  prettyTm (Sigma v d r)                 = parens (pretty v <+> colon <+> prettyTm d) <+> pretty "*" <+> prettyTm r
 
-prettyTm (IAnd x y) = parens $ prettyTm x <+> operator (pretty "&&") <+> prettyTm y
-prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y
-prettyTm (INot x) = operator (pretty '~') <> prettyTm x
+  prettyTm (IAnd x y) = parens $ prettyTm x <+> operator (pretty "&&") <+> prettyTm y
+  prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y
+  prettyTm (INot x) = operator (pretty '~') <> prettyTm x
 
-prettyTm (PathP l x y) = keyword (pretty "PathP") <+> parenArg l <+> parenArg x <+> parenArg y
-prettyTm (IElim _ _ _ f i) = prettyTm (App Ex f i)
-prettyTm (PathIntro _ _ _ f) = prettyTm f
+  prettyTm (System xs) = braces (mempty <+> hsep (punctuate comma (map go (Map.toList xs))) <+> mempty) where
+    go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
 
-prettyTm (IsOne phi)  = prettyTm (App Ex (Ref (Bound (T.pack ".IsOne"))) phi)
-prettyTm ItIsOne      = keyword (pretty "1=1")
-prettyTm (IsOne1 phi) = prettyTm (App Ex (Ref (Bound (T.pack ".isOne1"))) phi)
-prettyTm (IsOne2 phi) = prettyTm (App Ex (Ref (Bound (T.pack ".isOne2"))) phi)
+  prettyTm x = error (show x)
 
-prettyTm (Partial phi a)   = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".Partial"))) [phi, a]
-prettyTm (PartialP phi a)  = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".PartialP"))) [phi, a]
-prettyTm (Comp a phi u a0) = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".comp"))) [a, phi, u, a0]
-prettyTm (Sub a phi u)     = prettyTm a <> brackets (prettyTm phi <+> operator (pretty "->") <+> prettyTm u)
-prettyTm (Inc _ _ u)       = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".inS"))) [u]
-prettyTm (Ouc _ _ _ u)     = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".outS"))) [u]
+  beautify (PathP l x y)       = toFun "PathP" [l, x, y]
+  beautify (IElim _ _ _ f i)   = App Ex f i
+  beautify (PathIntro _ _ _ f) = f
 
-prettyTm (System xs) = braces (mempty <+> hsep (punctuate comma (map go (Map.toList xs))) <+> mempty) where
-  go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
+  beautify (IsOne phi)  = toFun "IsOne" [phi]
+  beautify ItIsOne      = Ref (Bound (T.pack ".1=1") 0)
+  beautify (IsOne1 phi) = toFun "isOne1" [phi]
+  beautify (IsOne2 phi) = toFun "isOne2" [phi]
+
+  beautify (Partial phi a)   = toFun "Partial" [phi, a]
+  beautify (PartialP phi a)  = toFun "PartialP" [phi, a]
+  beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0]
+  beautify (Sub a phi u)     = toFun "Sub" [a, phi, u]
+  beautify (Inc _ _ u)       = toFun "inS" [u]
+  beautify (Ouc _ phi u0 u)  = toFun "outS" [phi, u0, u]
+
+  beautify (GlueTy a I1 _ _)    = a
+  beautify (GlueTy a b c d)     = toFun "Glue"   [a,b,c,d]
+  beautify (Glue a b c d e f)   = toFun "glue"   [a,b,c,d,e,f]
+  beautify (Unglue a b c d e)   = toFun "unglue" [a,b,c,d,e]
+  beautify x = x
+
+  toFun s a = foldl (App Ex) (Ref (Bound (T.pack ('.':s)) 0)) a
 
 keyword :: Doc AnsiStyle -> Doc AnsiStyle
 keyword = annotate (color Magenta)
@@ -115,15 +127,11 @@ parenFun x@PathIntro{} = parens $ prettyTm x
 parenFun x = prettyTm x
 
 render :: Doc AnsiStyle -> Text
-render = L.toStrict . renderLazy . layoutPretty defaultLayoutOptions
+render = L.toStrict . renderLazy . layoutSmart defaultLayoutOptions
 
 showValue :: Value -> String
-showValue = L.unpack . renderLazy . layoutPretty defaultLayoutOptions . prettyTm . quote
+showValue = L.unpack . renderLazy . layoutSmart defaultLayoutOptions . prettyTm . quote
 
 showFace :: Map Head Bool -> Doc AnsiStyle
 showFace = hsep . map go . Map.toList where
   go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
-
-getNameText :: Name -> Text
-getNameText (Bound x) = x
-getNameText (Defined x) = x
\ No newline at end of file