diff --git a/src/Quox.idr b/src/Quox.idr
index cd617fa..785cc8a 100644
--- a/src/Quox.idr
+++ b/src/Quox.idr
@@ -1,6 +1,6 @@
 module Quox
 
-import public Quox.Syntax.Term
+import public Quox.Syntax
 import public Quox.Pretty
 
 import Data.Nat
diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
new file mode 100644
index 0000000..a3c81b0
--- /dev/null
+++ b/src/Quox/Context.idr
@@ -0,0 +1,185 @@
+module Quox.Context
+
+import Quox.Syntax.Shift
+import Quox.Pretty
+
+import Data.DPair
+import Data.Nat
+import Data.SnocList
+import Control.Monad.Identity
+
+%default total
+
+
+infixl 5 :<
+||| a sequence of bindings under an existing context. each successive element
+||| has one more bound variable, which correspond to all previous elements
+||| as well as the global context.
+public export
+data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
+  Lin  : Telescope tm from from
+  (:<) : Telescope tm from to -> tm to -> Telescope tm from (S to)
+%name Telescope tel
+
+||| a global context is actually just a telescope over no existing bindings
+public export
+Context : (tm : Nat -> Type) -> (len : Nat) -> Type
+Context tm len = Telescope tm 0 len
+
+export
+toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
+toSnocList [<]        = [<]
+toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
+
+private
+toList' : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
+toList' [<]        acc = acc
+toList' (tel :< t) acc = toList' tel (Evidence _ t :: acc)
+
+export %inline
+toList : Telescope tm _ _ -> List (Exists tm)
+toList tel = toList' tel []
+
+
+infixl 9 .
+public export
+(.) : Telescope tm from mid -> Telescope tm mid to -> Telescope tm from to
+tel1 . [<]         = tel1
+tel1 . (tel2 :< s) = (tel1 . tel2) :< s
+
+
+export
+getWith : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
+getWith (ctx :< t) VZ     th = t // drop1 th
+getWith (ctx :< t) (VS i) th = getWith ctx i (drop1 th)
+
+infixl 8 !!
+export %inline
+(!!) : CanShift tm => Context tm len -> Var len -> tm len
+ctx !! i = getWith ctx i SZ
+
+
+||| a triangle of bindings. each type binding in a context counts the ues of
+||| others in its type, and all of these together form a triangle.
+public export
+Triangle : (tm : Nat -> Type) -> (len : Nat) -> Type
+Triangle = Context . Context
+
+
+export
+0 telescopeLTE : Telescope _ from to -> from `LTE` to
+telescopeLTE [<]        = reflexive {rel=LTE}
+telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
+
+export
+(from `GT` to) => Uninhabited (Telescope _ from to) where
+  uninhabited tel = void $ LTEImpliesNotGT (telescopeLTE tel) %search
+
+export %hint
+0 succGT : S n `GT` n
+succGT = LTESucc $ reflexive {rel=LTE}
+
+export %inline
+absurd0 : (0 _ : Uninhabited a) => (0 _ : a) -> x
+absurd0 x = void $ absurd x
+
+
+parameters {auto _ : Applicative f}
+  export
+  traverse : (forall n. tm1 n -> f (tm2 n)) ->
+             Telescope tm1 from to -> f (Telescope tm2 from to)
+  traverse f [<]        = pure [<]
+  traverse f (tel :< x) = [|traverse f tel :< f x|]
+
+  infixl 3 `app`
+  ||| like `(<*>)` but with effects
+  export
+  app : Telescope (\n => tm1 n -> f (tm2 n)) from to ->
+        Telescope tm1 from to -> f (Telescope tm2 from to)
+  app [<]         [<]         = pure [<]
+  app (ftel :< f) (xtel :< x) = [|app ftel xtel :< f x|]
+  app [<]         (xtel :< _) = absurd0 xtel
+  app (ftel :< _) [<]         = absurd0 ftel
+
+  export %inline
+  sequence : Telescope (f . tm) from to -> f (Telescope tm from to)
+  sequence = traverse id
+
+export %inline
+map : (forall n. tm1 n -> tm2 n) ->
+      Telescope tm1 from to -> Telescope tm2 from to
+map f = runIdentity . traverse (pure . f)
+
+infixr 4 <$>
+export %inline
+(<$>) : (forall n. tm1 n -> tm2 n) ->
+        Telescope tm1 from to -> Telescope tm2 from to
+(<$>) = map
+
+infixl 3 <*>
+export %inline
+(<*>) : Telescope (\n => tm1 n -> tm2 n) from to ->
+        Telescope tm1 from to -> Telescope tm2 from to
+ftel <*> xtel = runIdentity $ (pure .) <$> ftel `app` xtel
+-- ...but can't write pure without `from,to` being relevant,
+-- so no idiom brackets ☹
+
+export %inline
+zipWith : (forall n. tm1 n -> tm2 n -> tm3 n) ->
+          Telescope tm1 from to -> Telescope tm2 from to ->
+          Telescope tm3 from to
+zipWith f tel1 tel2 = f <$> tel1 <*> tel2
+
+export %inline
+zipWith3 : (forall n. tm1 n -> tm2 n -> tm3 n -> tm4 n) ->
+           Telescope tm1 from to ->
+           Telescope tm2 from to ->
+           Telescope tm3 from to ->
+           Telescope tm4 from to
+zipWith3 f tel1 tel2 tel3 = f <$> tel1 <*> tel2 <*> tel3
+
+
+export
+lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
+lengthPrf [<]        = Element 0 Refl
+lengthPrf (tel :< _) =
+  let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
+
+public export %inline
+length : Telescope {} -> Nat
+length = fst . lengthPrf
+
+
+parameters {0 acc : Nat -> Type}
+  export
+  foldl : (forall m, n. acc m -> tm n -> acc (S m)) ->
+          acc 0 -> (tel : Telescope tm from to) -> acc (length tel)
+  foldl f z [<]        = z
+  foldl f z (tel :< t) = f (foldl f z tel) t
+
+parameters {auto _ : Monoid a}
+  export %inline
+  foldMap : (forall n. tm n -> a) -> Telescope tm from to -> a
+  foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
+
+  export %inline
+  fold : Telescope (\x => a) from to -> a
+  fold = foldMap id
+
+  ||| like `fold` but calculate the elements only when actually appending
+  export %inline
+  foldLazy : Telescope (\x => Lazy a) from to -> a
+  foldLazy = foldMap force
+
+
+export
+(forall n. Eq (tm n)) => Eq (Telescope tm from to) where
+  (==) = fold @{All} .: zipWith (==)
+
+export
+(forall n. Ord (tm n)) => Ord (Telescope tm from to) where
+  compare = foldLazy .: zipWith (delay .: compare)
+
+export
+(forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
+  prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)
diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
new file mode 100644
index 0000000..ba1e892
--- /dev/null
+++ b/src/Quox/Eval.idr
@@ -0,0 +1,30 @@
+module Quox.Eval
+
+-- todo list:
+-- - understand nbe and use it
+-- - take a proof of well-typedness as an argument
+
+import Quox.Syntax
+
+import Data.DPair
+
+%default total
+
+
+public export Exists2 : (ty1 -> ty2 -> Type) -> Type
+Exists2 t = Exists (\a => Exists (\b => t a b))
+
+public export SomeTerm : Type
+SomeTerm = Exists2 Term
+
+public export SomeElim : Type
+SomeElim = Exists2 Elim
+
+public export SomeDim : Type
+SomeDim = Exists Dim
+
+private some : {0 t : ty -> Type} -> t a -> Exists t
+some t = Evidence ? t
+
+private some2 : {0 t : ty1 -> ty2 -> Type} -> t a b -> Exists2 t
+some2 t = some $ some t
diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index a9296ba..d6178ef 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -87,16 +87,35 @@ hlF' : Functor f => HL -> f (Doc HL) -> f (Doc HL)
 hlF' = map . hl'
 
 
-export
+export %inline
 parens : Doc HL -> Doc HL
 parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
 
-export
+export %inline
 parensIf : Bool -> Doc HL -> Doc HL
 parensIf True  = parens
 parensIf False = id
 
 
+export
+separate' : Doc a -> List (Doc a) -> List (Doc a)
+separate' s []        = []
+separate' s [x]       = [x]
+separate' s (x :: xs) = x <+> s :: separate' s xs
+
+export %inline
+separate : Doc a -> List (Doc a) -> Doc a
+separate s = sep . separate' s
+
+export %inline
+hseparate : Doc a -> List (Doc a) -> Doc a
+hseparate s = hsep . separate' s
+
+export %inline
+vseparate : Doc a -> List (Doc a) -> Doc a
+vseparate s = vsep . separate' s
+
+
 public export
 record PrettyEnv where
   constructor MakePrettyEnv
@@ -112,21 +131,21 @@ record PrettyEnv where
 public export %inline HasEnv : (Type -> Type) -> Type
 HasEnv = MonadReader PrettyEnv
 
-export
+export %inline
 ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
 ifUnicode uni asc = if (!ask).unicode then [|uni|] else [|asc|]
 
-export
+export %inline
 parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
 parensIfM d doc = pure $ parensIf ((!ask).prec > d) doc
 
-export
+export %inline
 withPrec : HasEnv m => PPrec -> m a -> m a
 withPrec d = local {prec := d}
 
 public export data BinderSort = T | D
 
-export
+export %inline
 under : HasEnv m => BinderSort -> Name -> m a -> m a
 under s x = local $
   {prec := Outer} .
@@ -161,7 +180,7 @@ export PrettyHL BaseName where prettyM = pure . pretty . baseStr
 export PrettyHL Name     where prettyM = pure . pretty . toDots
 
 
-export
+export %inline
 prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String
 prettyStr {unicode} =
   let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in
@@ -180,7 +199,7 @@ termHL Qty     = color BrightMagenta <+> bold
 termHL Free    = color BrightWhite
 termHL Syntax  = color BrightBlue
 
-export
+export %inline
 prettyTerm : {default True color, unicode : Bool} -> PrettyHL a => a -> IO Unit
 prettyTerm x {color, unicode} =
   let reann = if color then map termHL else unAnnotate in
diff --git a/src/Quox/Syntax.idr b/src/Quox/Syntax.idr
new file mode 100644
index 0000000..505f9b0
--- /dev/null
+++ b/src/Quox/Syntax.idr
@@ -0,0 +1,9 @@
+module Quox.Syntax
+
+import public Quox.Syntax.Dim
+import public Quox.Syntax.Qty
+import public Quox.Syntax.Shift
+import public Quox.Syntax.Subst
+import public Quox.Syntax.Term
+import public Quox.Syntax.Universe
+import public Quox.Syntax.Var
diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
index 90c0783..3cec218 100644
--- a/src/Quox/Syntax/Qty.idr
+++ b/src/Quox/Syntax/Qty.idr
@@ -35,20 +35,33 @@ prettyQtyBinds =
 
 
 public export
-(+) : Qty -> Qty -> Qty
-Zero + rh   = rh
-pi   + Zero = pi
-_    + _    = Any
+plus : Qty -> Qty -> Qty
+plus Zero rh   = rh
+plus pi   Zero = pi
+plus _    _    = Any
 
 public export
-(*) : Qty -> Qty -> Qty
-Zero * _    = Zero
-_    * Zero = Zero
-One  * rh   = rh
-pi   * One  = pi
-Any  * Any  = Any
+times : Qty -> Qty -> Qty
+times Zero _    = Zero
+times _    Zero = Zero
+times One  rh   = rh
+times pi   One  = pi
+times Any  Any  = Any
 
 infix 6 <=.
 public export
-(<=.) : Qty -> Qty -> Bool
-pi <=. rh = rh == Any || pi == rh
+compat : Qty -> Qty -> Bool
+compat pi rh = rh == Any || pi == rh
+
+
+public export
+interface IsQty q where
+  zero, one : q
+  (+),  (*) : q -> q -> q
+  (<=.)     : q -> q -> Bool
+
+public export
+IsQty Qty where
+  zero  = Zero; one = One
+  (+)   = plus; (*) = times
+  (<=.) = compat
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index 471f13f..5e23ebe 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -172,3 +172,35 @@ prettyShift bnd by =
 
 ||| prints using the `TVar` highlight for variables
 export PrettyHL (Shift from to) where prettyM = prettyShift TVar
+
+
+||| Drops the innermost variable from the input scope.
+public export
+drop1 : Shift (S from) to -> Shift from to
+drop1 SZ      = SS SZ
+drop1 (SS by) = SS (drop1 by)
+
+private
+drop1ViaNat : Shift (S from) to -> Shift from to
+drop1ViaNat by =
+  rewrite shiftDiff by in
+  rewrite sym $ plusSuccRightSucc by.nat from in
+  fromNat (S by.nat)
+
+private
+0 drop1ViaNatCorrect : (by : Shift (S from) to) -> drop1ViaNat by = drop1 by
+drop1ViaNatCorrect SZ = Refl
+drop1ViaNatCorrect (SS by) =
+  rewrite plusSuccRightSucc by.nat from in
+  rewrite sym $ shiftDiff by in
+  cong SS $ drop1ViaNatCorrect by
+
+%transform "Shift.drop1" drop1 by = drop1ViaNat by
+
+
+infixl 8 //
+public export
+interface CanShift f where
+  (//) : f from -> Shift from to -> f to
+
+export CanShift Var where i // by = shift by i
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index 34b5b34..47f0b8c 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -1,6 +1,6 @@
 module Quox.Syntax.Subst
 
-import Quox.Syntax.Shift
+import public Quox.Syntax.Shift
 import Quox.Syntax.Var
 import Quox.Name
 import Quox.Pretty
@@ -35,7 +35,7 @@ export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr
 infixl 8 //
 public export
 interface FromVar env => CanSubst env term where
-  (//) : term from -> Subst env from to -> term to
+  (//) : term from -> Lazy (Subst env from to) -> term to
 
 public export
 CanSubst1 : (Nat -> Type) -> Type
@@ -84,6 +84,11 @@ public export %inline
 push : CanSubst1 f => Subst f from to -> Subst f (S from) (S to)
 push th = fromVar VZ ::: (th . shift 1)
 
+public export
+drop1 : Subst f (S from) to -> Subst f from to
+drop1 (Shift by) = Shift $ drop1 by
+drop1 (t ::: th) = th
+
 
 ||| `prettySubst pr bnd op cl unicode th` pretty-prints the substitution `th`,
 ||| with the following arguments:
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 3c0c576..00a5836 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -187,11 +187,12 @@ export FromVar (Term d) where fromVar = E . fromVar
 ||| - otherwise, wraps in a new closure
 export
 CanSubst (Elim d) (Elim d) where
-  F x       // _        = F x
-  B i       // th       = th !! i
-  CloE e ph // th       = CloE e $ assert_total $ ph . th
-  e         // Shift SZ = e
-  e         // th       = CloE e th
+  F x       // _  = F x
+  B i       // th = th !! i
+  CloE e ph // th = assert_total CloE e $ ph . th
+  e         // th = case force th of
+                         Shift SZ => e
+                         th       => CloE e th
 
 ||| does the minimal reasonable work:
 ||| - deletes the closure around an atomic constant like `TYPE`
@@ -201,11 +202,18 @@ CanSubst (Elim d) (Elim d) where
 ||| - otherwise, wraps in a new closure
 export
 CanSubst (Elim d) (Term d) where
-  TYPE l    // _        = TYPE l
-  E e       // th       = E $ e // th
-  CloT s ph // th       = CloT s $ ph . th
-  s         // Shift SZ = s
-  s         // th       = CloT s th
+  TYPE l    // _  = TYPE l
+  E e       // th = E $ e // th
+  CloT s ph // th = CloT s $ ph . th
+  s         // th = case force th of
+                         Shift SZ => s
+                         th       => CloT s th
+
+export CanSubst Var (Term d) where s // th = s // map (B {d}) th
+export CanSubst Var (Elim d) where e // th = e // map (B {d}) th
+
+export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)}
+export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)}
 
 
 infixl 8 ///
@@ -253,27 +261,27 @@ comp' th ps ph = map (/// th) ps . ph
 
 ||| true if an elimination has a closure or dimension closure at the top level
 public export %inline
-isCloE : Elim d n -> Bool
-isCloE (CloE  _ _) = True
-isCloE (DCloE _ _) = True
-isCloE _           = False
+topCloE : Elim d n -> Bool
+topCloE (CloE  _ _) = True
+topCloE (DCloE _ _) = True
+topCloE _           = False
 
 ||| true if a term has a closure or dimension closure at the top level,
 ||| or is `E` applied to such an elimination
 public export %inline
-isCloT : Term d n -> Bool
-isCloT (CloT  _ _) = True
-isCloT (DCloT _ _) = True
-isCloT (E e)       = isCloE e
-isCloT _           = False
+topCloT : Term d n -> Bool
+topCloT (CloT  _ _) = True
+topCloT (DCloT _ _) = True
+topCloT (E e)       = topCloE e
+topCloT _           = False
 
 ||| an elimination which is not a top level closure
 public export NotCloElim : Nat -> Nat -> Type
-NotCloElim d n = Subset (Elim d n) $ So . not . isCloE
+NotCloElim d n = Subset (Elim d n) $ So . not . topCloE
 
 ||| a term which is not a top level closure
 public export NotCloTerm : Nat -> Nat -> Type
-NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
+NotCloTerm d n = Subset (Term d n) $ So . not . topCloT
 
 
 mutual