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/Pretty.idr b/src/Quox/Pretty.idr
index 31f5764..d6178ef 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -97,6 +97,25 @@ 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
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index 2a6f1f2..5e23ebe 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -174,6 +174,30 @@ prettyShift bnd by =
 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
diff --git a/src/Quox/Syntax/Subst.idr b/src/Quox/Syntax/Subst.idr
index f80dc6b..47f0b8c 100644
--- a/src/Quox/Syntax/Subst.idr
+++ b/src/Quox/Syntax/Subst.idr
@@ -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: