diff --git a/src/Quox.idr b/src/Quox.idr
index 4e1b620..785cc8a 100644
--- a/src/Quox.idr
+++ b/src/Quox.idr
@@ -11,11 +11,11 @@ export
 tm : Term 1 2
 tm =
   (Pi Zero One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
-    `DCloT` (K One ::: id))
+    `DCloT` (DOne ::: id))
     `CloT`  (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
 
 main : IO Unit
 main = do
   prettyTerm tm
   prettyTerm $ pushSubstsT tm
-  putStrLn "\n:qtuwu:"
+  putStrLn ":qtuwu:"
diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 07c2f45..dc66a8b 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -22,7 +22,7 @@ data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
 %name Telescope tel
 
 public export
-Telescope' : (a : Type) -> (from, to : Nat) -> Type
+Telescope' : Type -> (from, to : Nat) -> Type
 Telescope' a = Telescope (\_ => a)
 
 ||| a global context is actually just a telescope over no existing bindings
@@ -31,30 +31,30 @@ Context : (tm : Nat -> Type) -> (len : Nat) -> Type
 Context tm len = Telescope tm 0 len
 
 public export
-Context' : (a : Type) -> (len : Nat) -> Type
+Context' : Type -> (len : Nat) -> Type
 Context' a = Context (\_ => a)
 
 
 export
-toSnocList : Telescope {tm, _} -> SnocList (Exists tm)
+toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
 toSnocList [<]        = [<]
 toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
 
 private
-toListAcc : Telescope {tm, _} -> List (Exists tm) -> List (Exists tm)
+toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
 toListAcc [<]        acc = acc
 toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
 
 export %inline
-toList : Telescope {tm, _} -> List (Exists tm)
+toList : Telescope tm _ _ -> List (Exists tm)
 toList tel = toListAcc tel []
 
 export %inline
-toSnocList' : Telescope' {a, _} -> SnocList a
+toSnocList' : Telescope' a _ _ -> SnocList a
 toSnocList' = map snd . toSnocList
 
 export %inline
-toList' : Telescope' {a, _} -> List a
+toList' : Telescope' a _ _ -> List a
 toList' = map snd . toList
 
 
@@ -65,20 +65,15 @@ tel1 . [<]         = tel1
 tel1 . (tel2 :< s) = (tel1 . tel2) :< s
 
 
-public export
-getShift : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
-getShift (ctx :< t) VZ     by = t // drop1 by
-getShift (ctx :< t) (VS i) by = getShift ctx i (drop1 by)
+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 !!
-public export %inline
+export %inline
 (!!) : CanShift tm => Context tm len -> Var len -> tm len
-ctx !! i = getShift ctx i SZ
-
-infixl 8 !?
-public export %inline
-(!?) : Context' tm len -> Var len -> tm
-ctx !? i = (ctx !! i) @{Const}
+ctx !! i = getWith ctx i SZ
 
 
 ||| a triangle of bindings. each type binding in a context counts the ues of
@@ -93,7 +88,7 @@ Triangle' a = Context $ Context (\_ => a)
 
 export
 0 telescopeLTE : Telescope _ from to -> from `LTE` to
-telescopeLTE [<]        = reflexive {rel=Nat.LTE}
+telescopeLTE [<]        = reflexive {rel=LTE}
 telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
 
 export
@@ -102,7 +97,7 @@ export
 
 export %hint
 0 succGT : S n `GT` n
-succGT = LTESucc $ reflexive {rel=Nat.LTE}
+succGT = LTESucc $ reflexive {rel=LTE}
 
 
 parameters {auto _ : Applicative f}
@@ -178,41 +173,36 @@ zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
 
 
 export
-lengthPrf : Telescope _ from to -> (len : Nat ** len + from = to)
-lengthPrf [<]        = (0 ** Refl)
-lengthPrf (tel :< _) =
-  let len = lengthPrf tel in (S len.fst ** cong S len.snd)
-
-export
-lengthPrf0 : Context _ to -> (len : Nat ** len = to)
-lengthPrf0 ctx =
-  let (len ** prf) = lengthPrf ctx in
-  (len ** rewrite sym $ plusZeroRightNeutral len in prf)
+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
 
 
-export
-foldl : {0 acc : Nat -> Type} ->
-        (f : forall n. acc n -> tm (n + from) -> acc (S n)) ->
-        (z : acc 0) -> (tel : Telescope tm from to) -> acc (length tel)
-foldl f z [<]        = z
-foldl f z (tel :< t) = f (foldl f z tel) (rewrite (lengthPrf tel).snd in t)
+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
 
-export %inline
-foldMap : Monoid a => (forall n. tm n -> a) -> Telescope tm from to -> a
-foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
+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 : Monoid a => Telescope' a from to -> a
-fold = foldMap id
+  export %inline
+  fold : Telescope' a from to -> a
+  fold = foldMap id
 
-||| like `fold` but calculate the elements only when actually appending
-export %inline
-foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
-foldLazy = foldMap force
+  ||| like `fold` but calculate the elements only when actually appending
+  export %inline
+  foldLazy : Telescope' (Lazy a) from to -> a
+  foldLazy = foldMap force
 
 
 export %inline
diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr
index 2175057..bbe8b0f 100644
--- a/src/Quox/Error.idr
+++ b/src/Quox/Error.idr
@@ -12,8 +12,8 @@ import Control.Monad.RWS
 %default total
 
 
-||| a representation of a list's length. this is used in `implyAll` to transform
-||| the constraints one by one
+||| a representation of a list's length. this is used in the `Ord` instance to
+||| transform the `Ord` constraints into `Eq`s
 public export
 data Spine : List a -> Type where
   NIL  : Spine []
@@ -37,12 +37,13 @@ Uninhabited (OneOf []) where uninhabited x = uninhabited x.elem
 
 export %inline
 inj : ty `Elem` tys => ty -> OneOf tys
-inj @{elem} value = One {elem, value}
+inj value = One %search value
 
 ||| `All p types` computes a constraint for `p a` for each `a` in `types`
 public export
 All : (Type -> Type) -> List Type -> Type
-All p = foldr (,) () . map p
+All p []      = ()
+All p (x::xs) = (p x, All p xs)
 
 
 private
@@ -50,28 +51,24 @@ eq : All Eq types => OneOf types -> OneOf types -> Bool
 eq (One Here      x) (One Here      y) = x == y
 eq (One (There p) x) (One (There q) y) = eq (One p x) (One q y)
 eq (One Here      _) (One (There _) _) = False
-eq (One (There _) _) (One Here      _) = False
+eq (One (There z) x) (One Here      y) = False
 
 export %inline
 All Eq types => Eq (OneOf types) where (==) = eq
 
 
-export
-implyAll : (0 c, d : Type -> Type) ->
-           (forall a. c a -> d a) => Spine types => All c types => All d types
-implyAll c d @{q} @{spine} @{ps} = go spine ps where
-  go : forall types. Spine types -> All c types -> All d types
-  go NIL       _       = ()
-  go (CONS tl) (p, ps) = (q p, go tl ps)
-
+private
+ordsToEqs : Spine types => All Ord types => All Eq types
+ordsToEqs @{NIL}     = ()
+ordsToEqs @{CONS tl} = (%search, ordsToEqs @{tl})
 
 private %inline
 [eqOrds] (Spine types, All Ord types) => Eq (OneOf types) where
-  (==) = eq @{implyAll Ord Eq}
+  (==) = eq @{ordsToEqs}
 
 
 private
-cmp : All Ord types => (x, y : OneOf types) -> Ordering
+cmp : All Ord types => OneOf types -> OneOf types -> Ordering
 cmp (One Here      x) (One Here      y) = compare x y
 cmp (One Here      _) (One (There _) _) = LT
 cmp (One (There _) _) (One Here      _) = GT
@@ -82,12 +79,11 @@ export %inline
   compare = cmp
 
 
-export %inline
-All Show types => Show (OneOf types) where
-  showPrec d = go where
-    go : forall types. All Show types => OneOf types -> String
-    go (One Here      value) = showPrec d value
-    go (One (There p) value) = go $ One p value
+private shw : All Show types => Prec -> OneOf types -> String
+shw d (One Here      value) = showPrec d value
+shw d (One (There p) value) = shw d $ One p value
+
+export %inline All Show types => Show (OneOf types) where showPrec = shw
 
 
 public export
@@ -126,7 +122,7 @@ without' (y :: xs) (There p) = y :: without' xs p
 infix 9 `without`
 export %inline
 without : (xs : List a) -> (x : a) -> x `Elem` xs => List a
-(xs `without` x) @{e} = without' xs e
+xs `without` x = without' {x} xs %search
 
 
 private
@@ -139,7 +135,7 @@ get' (There y) (One (There p) x) = mapSnd {elem $= There} $ get' y (One p x)
 export %inline
 get : (0 err : Type) -> err `Elem` errs =>
       OneOf errs -> Either err (OneOf (errs `without` err))
-get _ @{e} = get' e
+get _ = get' %search
 
 
 export %inline
@@ -157,12 +153,14 @@ data Embed : List a -> List a -> Type where
   (::) : x `Elem` ys -> Embed xs ys -> Embed (x::xs) ys
 
 
+private
+embedElem' : Embed xs ys -> x `Elem` xs -> x `Elem` ys
+embedElem' (e :: _)  Here      = e
+embedElem' (_ :: es) (There p) = embedElem' es p
+
 export %inline
 embedElem : Embed xs ys => x `Elem` xs -> x `Elem` ys
-embedElem @{emb} = go emb where
-  go : forall xs. Embed xs ys -> x `Elem` xs -> x `Elem` ys
-  go (e :: _)  Here      = e
-  go (_ :: es) (There p) = go es p
+embedElem = embedElem' %search
 
 
 export %inline
@@ -207,7 +205,7 @@ implementation
   (Monad m, Embed errs1 errs2) =>
   MonadEmbed (ErrorT errs1 m) (ErrorT errs2 m)
 where
-  embed (MkErrorT act) = MkErrorT $ act <&> mapFst {elem $= embedElem}
+  embed (MkErrorT act) = MkErrorT $ mapFst {elem $= embedElem} <$> act
 
 
 export %inline
diff --git a/src/Quox/Eval.idr b/src/Quox/Eval.idr
new file mode 100644
index 0000000..0e3e878
--- /dev/null
+++ b/src/Quox/Eval.idr
@@ -0,0 +1,130 @@
+module Quox.Eval
+
+-- todo list:
+-- - understand nbe and use it
+-- - take a proof of well-typedness as an argument,
+--   to reduce the number of eithers
+-- - remove the either if possible (should be???)
+
+import Quox.Syntax
+import Quox.Context
+
+import Data.DPair
+import Data.SortedMap
+
+%default total
+
+
+public export
+record Global where
+  constructor G
+  val : forall d, n. NotCloElim d n
+
+public export Globals : Type
+Globals = SortedMap Name Global
+
+export (!!) : Globals -> Name -> Maybe (Elim d n)
+gs !! x = map (\g => g.val.fst) $ lookup x gs
+  -- just `map (fst . val)` fails?
+
+
+mutual
+  public export isValue : Term d n -> Bool
+  isValue (TYPE {})          = True
+  isValue (Pi {arg, res, _}) = isValue arg && isValue res
+  isValue (Lam {body, _})    = isValue body
+  isValue (E e)              = isNeutral e
+  isValue (CloT  {})         = False
+  isValue (DCloT {})         = False
+
+  public export isNeutral : Elim d n -> Bool
+  isNeutral (F {})       = False
+  isNeutral (B {})       = True
+  isNeutral (fun :@ arg) = isNeutral fun && isValue arg
+  isNeutral (_ :# _)     = False
+  isNeutral (CloE {})    = False
+  isNeutral (DCloE {})   = False
+
+public export IsValue : Term d n -> Type
+IsValue = So . isValue
+
+public export IsNeutral : Elim d n -> Type
+IsNeutral = So . isNeutral
+
+public export Value : Nat -> Nat -> Type
+Value d n = Subset (Term d n) IsValue
+
+public export Neutral : Nat -> Nat -> Type
+Neutral d n = Subset (Elim d n) IsNeutral
+
+public export valT : (t : Term d n) -> (0 _ : IsValue t) => Value d n
+valT t = Element t %search
+
+public export neuE : (e : Elim d n) -> (0 _ : IsNeutral e) => Neutral d n
+neuE e = Element e %search
+
+
+data EvalError =
+    NotInScope Name
+  | NonFunction SomeElim
+
+
+parameters (globals : Globals)
+  mutual
+    export covering %inline
+    evalT : Term d n -> Either EvalError (Value d n)
+    evalT = uncurry evalT' . pushSubstsT
+
+    export covering %inline
+    evalE : Elim d n -> Either EvalError (Neutral d n)
+    evalE = uncurry evalE' . pushSubstsE
+
+    export covering
+    evalT' : (t : Term d n) -> (0 prf : IsNotCloT t) ->
+             Either EvalError (Value d n)
+
+    export covering
+    evalE' : (e : Elim d n) -> (0 prf : IsNotCloE e) ->
+             Either EvalError (Neutral d n)
+
+
+public export
+data AlphaResult =
+    Ok
+  | Clash  SomeTerm SomeTerm
+  | DClash SomeDim  SomeDim
+  | QClash Qty      Qty
+
+export
+Semigroup AlphaResult where
+  Ok  <+> res = res
+  res <+> _   = res
+
+export Monoid AlphaResult where neutral = Ok
+
+private %inline clash : Term d1 n1 -> Term d2 n2 -> AlphaResult
+clash s t = Clash (some2 s) (some2 t)
+
+
+||| check two quantities are exactly equal and fail if not
+export %inline
+alphaQ : (pi, rh : Qty) -> AlphaResult
+alphaQ pi rh = if pi == rh then Ok else QClash pi rh
+
+export %inline
+alphaD : (al, be : Dim d) -> AlphaResult
+alphaD al be = if al == be then Ok else DClash (some al) (some be)
+
+mutual
+  private
+  alphaT : (s, t : Term d n) -> AlphaResult
+
+  private
+  alphaE : (e, f : Elim d n) -> AlphaResult
+
+
+export %inline alphaV : (u, v : Value d n) -> AlphaResult
+alphaV u v = alphaT u.fst v.fst
+
+export %inline alphaN : (p, q : Neutral d n) -> AlphaResult
+alphaN p q = alphaE p.fst q.fst
diff --git a/src/Quox/Syntax.idr b/src/Quox/Syntax.idr
index 5cfd888..505f9b0 100644
--- a/src/Quox/Syntax.idr
+++ b/src/Quox/Syntax.idr
@@ -1,7 +1,6 @@
 module Quox.Syntax
 
 import public Quox.Syntax.Dim
-import public Quox.Syntax.DimEq
 import public Quox.Syntax.Qty
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst
diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr
index 6dd0e90..e58e98d 100644
--- a/src/Quox/Syntax/Dim.idr
+++ b/src/Quox/Syntax/Dim.idr
@@ -7,44 +7,26 @@ import Quox.Pretty
 %default total
 
 
-public export
-data DimConst = Zero | One
-%name DimConst e
-
-private DCRepr : Type
-DCRepr = Nat
-
-private %inline dcrepr : DimConst -> DCRepr
-dcrepr e = case e of Zero => 0; One => 1
-
-export Eq  DimConst where (==) = (==) `on` dcrepr
-export Ord DimConst where compare = compare `on` dcrepr
-
-
 public export
 data Dim : Nat -> Type where
-  K : DimConst -> Dim d
-  B : Var d -> Dim d
+  DZero, DOne : Dim d
+  DBound : Var d -> Dim d
 %name Dim.Dim p, q
 
 private DRepr : Type
 DRepr = Nat
 
 private %inline drepr : Dim n -> DRepr
-drepr p = case p of K i => dcrepr i; B i => 2 + i.nat
+drepr d = case d of DZero => 0; DOne => 1; DBound i => 2 + i.nat
 
 export Eq  (Dim n) where (==) = (==) `on` drepr
 export Ord (Dim n) where compare = compare `on` drepr
 
-export
-PrettyHL DimConst where
-  prettyM Zero = hl Dim <$> ifUnicode "𝟬" "0"
-  prettyM One  = hl Dim <$> ifUnicode "𝟭" "1"
-
 export
 PrettyHL (Dim n) where
-  prettyM (K e) = prettyM e
-  prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i
+  prettyM DZero      = hl Dim <$> ifUnicode "𝟬" "0"
+  prettyM DOne       = hl Dim <$> ifUnicode "𝟭" "1"
+  prettyM (DBound i) = prettyVar DVar DVarErr (!ask).dnames i
 
 
 public export
@@ -59,14 +41,10 @@ prettyDSubst th =
     !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
 
 
-export FromVar Dim where fromVar = B
-
-export
-CanShift Dim where
-  K e // _  = K e
-  B i // by = B (i // by)
+export FromVar Dim where fromVar = DBound
 
 export
 CanSubst Dim Dim where
-  K e // _  = K e
-  B i // th = th !! i
+  DZero    // _  = DZero
+  DOne     // _  = DOne
+  DBound i // th = th !! i
diff --git a/src/Quox/Syntax/DimEq.idr b/src/Quox/Syntax/DimEq.idr
deleted file mode 100644
index e6edbd5..0000000
--- a/src/Quox/Syntax/DimEq.idr
+++ /dev/null
@@ -1,135 +0,0 @@
-module Quox.Syntax.DimEq
-
-import public Quox.Syntax.Var
-import public Quox.Syntax.Dim
-import public Quox.Syntax.Subst
-import public Quox.Context
-
-import Data.Maybe
-import Data.Nat
-import Data.DPair
-
-%default total
-
-
-public export
-DimEq' : Nat -> Type
-DimEq' = Context (Maybe . Dim)
-
-
-public export
-data DimEq : Nat -> Type where
-  ZeroIsOne : DimEq d
-  C         : (eqs : DimEq' d) -> DimEq d
-
-%name DimEq eqs
-
-
-export
-new' : (d : Nat) -> DimEq' d
-new' 0     = [<]
-new' (S d) = new' d :< Nothing
-
-export
-new : (d : Nat) -> DimEq d
-new d = C (new' d)
-
-
-export
-get : DimEq' d -> Dim d -> Dim d
-get _   (K e) = K e
-get eqs (B i) = fromMaybe (B i) $ (eqs !! i) @{Compose}
-
-export
-equal : DimEq d -> (p, q : Dim d) -> Bool
-equal ZeroIsOne p q = True
-equal (C eqs)   p q = get eqs p == get eqs q
-
-
-infixl 5 :<?
-export
-(:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d)
-ZeroIsOne :<? d = ZeroIsOne
-C eqs     :<? d = C $ eqs :< d
-
-private
-checkConst : (e, f : DimConst) -> (eqs : Lazy (DimEq' d)) -> DimEq d
-checkConst Zero Zero eqs = C eqs
-checkConst One  One  eqs = C eqs
-checkConst _    _    _   = ZeroIsOne
-
-
-export
-setConst : Var d -> DimConst -> DimEq' d -> DimEq d
-setConst VZ e (eqs :< Nothing)    = C $ eqs :< Just (K e)
-setConst VZ e (eqs :< Just (K f)) = checkConst e f $ eqs :< Just (K f)
-setConst VZ e (eqs :< Just (B i)) = setConst i e eqs :<? Just (K e)
-setConst (VS i) e (eqs :< x) =
-  setConst i e eqs :<? (if x == Just (B i) then Just (K e) else x)
-
-mutual
-  private
-  setVar' : (i, j : Var d) -> i `LT` j -> DimEq' d -> DimEq d
-  setVar' VZ (VS i) LTZ (eqs :< Nothing)    = C $ eqs :< Just (B i)
-  setVar' VZ (VS i) LTZ (eqs :< Just (K e)) = setConst i e eqs :<? Just (K e)
-  setVar' VZ (VS i) LTZ (eqs :< Just (B j)) = setVar i j eqs :<? Just (B (max i j))
-  setVar' (VS i) (VS j) (LTS lt) (eqs :< p) =
-    setVar' i j lt eqs :<? map (\k => if k == B i then B j else k) p
-
-  export
-  setVar : (i, j : Var d) -> DimEq' d -> DimEq d
-  setVar i j eqs =
-    case compareP i j of
-      IsLT lt => setVar' i j lt eqs
-      IsEQ    => C eqs
-      IsGT gt => setVar' j i gt eqs
-
-
-export
-set : (p, q : Dim d) -> DimEq d -> DimEq d
-set _ _ ZeroIsOne = ZeroIsOne
-set (K e) (K f) (C eqs) = checkConst e f eqs
-set (K e) (B i) (C eqs) = setConst i e eqs
-set (B i) (K e) (C eqs) = setConst i e eqs
-set (B i) (B j) (C eqs) = setVar   i j eqs
-
-
-export
-setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
-setSelf p ZeroIsOne = Refl
-setSelf (K Zero) (C eqs) = Refl
-setSelf (K One)  (C eqs) = Refl
-setSelf (B i)    (C eqs) with (compareP i i)
-  _ | IsLT lt = absurd lt
-  _ | IsEQ    = Refl
-  _ | IsGT gt = absurd gt
-
-
-
-public export
-Split : Nat -> Type
-Split d = (DimEq' d, DSubst (S d) d)
-
-export
-split1 : DimConst -> DimEq' (S d) -> Maybe (Split d)
-split1 e eqs = case setConst VZ e eqs of
-  ZeroIsOne    => Nothing
-  C (eqs :< _) => Just (eqs, K e ::: id)
-
-export
-split : DimEq' (S d) -> List (Split d)
-split eqs = toList (split1 Zero eqs) <+> toList (split1 One eqs)
-
-
-export
-splits' : DimEq' d -> List (DSubst d 0)
-splits' [<] = [id]
-splits' eqs@(_ :< _) = do
-  (eqs, th) <- split eqs
-  ph <- splits' eqs
-  pure $ th . ph
-
-export
-splits : DimEq d -> List (DSubst d 0)
-splits ZeroIsOne = []
-splits (C eqs) = splits' eqs
diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
index f27643f..3cec218 100644
--- a/src/Quox/Syntax/Qty.idr
+++ b/src/Quox/Syntax/Qty.idr
@@ -27,16 +27,11 @@ PrettyHL Qty where
       One  => ifUnicode "𝟭" "1"
       Any  => ifUnicode "𝛚" "*"
 
-private
-commas : List (Doc HL) -> List (Doc HL)
-commas [] = []
-commas [x] = [x]
-commas (x::xs) = (x <+> hl Delim ",") :: commas xs
-
 export %inline
 prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
 prettyQtyBinds =
-  map ((hl Delim "@" <++>) . align . sep . commas) . traverse pretty0M
+  map (align . sep) .
+  traverse (\pi => [|pretty0M pi <++> pure (hl Delim "|")|])
 
 
 public export
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index d491ddb..5e23ebe 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -59,9 +59,9 @@ export
                by.nat + i.nat `LT` to
 shiftVarLT by i =
   rewrite plusSuccRightSucc by.nat i.nat in
-  transitive {rel=Nat.LTE}
+  transitive {rel=LTE}
     (plusLteMonotoneLeft by.nat (S i.nat) from (toNatLT i))
-    (replace {p=(`LTE` to)} (shiftDiff by) $ reflexive {rel=Nat.LTE})
+    (replace {p=(\n => LTE n to)} (shiftDiff by) $ reflexive {rel=LTE})
 
 
 public export
@@ -204,11 +204,3 @@ interface CanShift f where
   (//) : f from -> Shift from to -> f to
 
 export CanShift Var where i // by = shift by i
-
-namespace CanShift
-  export
-  [Compose] (Functor f, CanShift tm) => CanShift (f . tm) where
-    x // by = map (// by) x
-
-  export
-  [Const] CanShift (\_ => a) where x // _ = x
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 598bbf6..b1441c5 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -34,7 +34,7 @@ mutual
     TYPE : (l : Universe) -> Term d n
 
     ||| function type
-    Pi  : (qtm, qty : Qty) -> (x : Name) ->
+    Pi  : (qty, qtm : Qty) -> (x : Name) ->
           (arg : Term d n) -> (res : Term d (S n)) -> Term d n
     ||| function term
     Lam : (x : Name) -> (body : Term d (S n)) -> Term d n
@@ -126,9 +126,9 @@ mutual
   PrettyHL (Term d n) where
     prettyM (TYPE l) =
       parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
-    prettyM (Pi qtm qty x s t) =
+    prettyM (Pi qty qtm x s t) =
       parensIfM Outer $ hang 2 $
-        !(prettyBinder [qtm, qty] x s) <++> !arrowD
+        !(prettyBinder [qty, qtm] x s) <++> !arrowD
           <//> !(under T x $ prettyM t)
     prettyM (Lam x t) =
       parensIfM Outer $
@@ -172,9 +172,8 @@ mutual
   prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
   prettyBinder pis x a =
     pure $ parens $ hang 2 $
-      hsep [hl TVar !(prettyM x),
-            sep [!(prettyQtyBinds pis),
-                 hsep [colonD, !(withPrec Outer $ prettyM a)]]]
+      !(prettyQtyBinds pis) <//>
+      hsep [hl TVar !(prettyM x), colonD, !(withPrec Outer $ prettyM a)]
 
 
 export FromVar (Elim d) where fromVar = B
@@ -305,57 +304,47 @@ ncloE e = Element e %search
 mutual
   ||| if the input term has any top-level closures, push them under one layer of
   ||| syntax
-  export %inline
+  export
   pushSubstsT : Term d n -> NotCloTerm d n
-  pushSubstsT s = pushSubstsTWith id id s
+  pushSubstsT s = pushSubstsT' id id s
 
   ||| if the input elimination has any top-level closures, push them under one
   ||| layer of syntax
-  export %inline
+  export
   pushSubstsE : Elim d n -> NotCloElim d n
-  pushSubstsE e = pushSubstsEWith id id e
+  pushSubstsE e = pushSubstsE' id id e
 
   private
-  pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
-                    Term dfrom from -> NotCloTerm dto to
-  pushSubstsTWith th ph (TYPE l) =
+  pushSubstsT' : DSubst dfrom dto -> TSubst dto from to ->
+                 Term dfrom from -> NotCloTerm dto to
+  pushSubstsT' th ph (TYPE l) =
     ncloT $ TYPE l
-  pushSubstsTWith th ph (Pi qtm qty x a b) =
-    ncloT $ Pi qtm qty x (subs a th ph) (subs b th (push ph))
-  pushSubstsTWith th ph (Lam x t) =
+  pushSubstsT' th ph (Pi qty qtm x a b) =
+    ncloT $ Pi qty qtm x (subs a th ph) (subs b th (push ph))
+  pushSubstsT' th ph (Lam x t) =
     ncloT $ Lam x $ subs t th $ push ph
-  pushSubstsTWith th ph (E e) =
-    let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
-  pushSubstsTWith th ph (CloT  s ps) =
-    pushSubstsTWith th (comp' th ps ph) s
-  pushSubstsTWith th ph (DCloT s ps) =
-    pushSubstsTWith (ps . th) ph s
+  pushSubstsT' th ph (E e) =
+    let Element e _ = pushSubstsE' th ph e in ncloT $ E e
+  pushSubstsT' th ph (CloT  s ps) =
+    pushSubstsT' th (comp' th ps ph) s
+  pushSubstsT' th ph (DCloT s ps) =
+    pushSubstsT' (ps . th) ph s
 
   private
-  pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
-                    Elim dfrom from -> NotCloElim dto to
-  pushSubstsEWith th ph (F x) =
+  pushSubstsE' : DSubst dfrom dto -> TSubst dto from to ->
+                 Elim dfrom from -> NotCloElim dto to
+  pushSubstsE' th ph (F x) =
     ncloE $ F x
-  pushSubstsEWith th ph (B i) =
+  pushSubstsE' th ph (B i) =
     assert_total pushSubstsE $ ph !! i
-  pushSubstsEWith th ph (f :@ s) =
+  pushSubstsE' th ph (f :@ s) =
     ncloE $ subs f th ph :@ subs s th ph
-  pushSubstsEWith th ph (s :# a) =
+  pushSubstsE' th ph (s :# a) =
     ncloE $ subs s th ph :# subs a th ph
-  pushSubstsEWith th ph (CloE  e ps) =
-    pushSubstsEWith th (comp' th ps ph) e
-  pushSubstsEWith th ph (DCloE e ps) =
-    pushSubstsEWith (ps . th) ph e
-
-
-public export %inline
-pushSubstsT' : Term d n -> Term d n
-pushSubstsT' s = (pushSubstsT s).fst
-
-
-public export %inline
-pushSubstsE' : Elim d n -> Elim d n
-pushSubstsE' e = (pushSubstsE e).fst
+  pushSubstsE' th ph (CloE  e ps) =
+    pushSubstsE' th (comp' th ps ph) e
+  pushSubstsE' th ph (DCloE e ps) =
+    pushSubstsE' (ps . th) ph e
 
 
 parameters {auto _ : Alternative f}
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 9f5742a..ca5747b 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -133,82 +133,3 @@ public export
 interface FromVar f where %inline fromVar : Var n -> f n
 
 public export FromVar Var where fromVar = id
-
-
-public export
-data LT : Var n -> Var n -> Type where
-  LTZ : VZ `LT` VS i
-  LTS : i `LT` j -> VS i `LT` VS j
-%builtin Natural Var.LT
-%name Var.LT lt
-
-public export %inline
-GT : Var n -> Var n -> Type
-i `GT` j = j `LT` i
-
-export
-Transitive (Var n) LT where
-  transitive LTZ     (LTS _) = LTZ
-  transitive (LTS p) (LTS q) = LTS $ transitive p q {rel=Var.LT}
-
-export Uninhabited (i    `Var.LT` i)  where uninhabited (LTS p) = uninhabited p
-export Uninhabited (VS i `LT`     VZ) where uninhabited _ impossible
-
-export
-isLT : (i, j : Var n) -> Dec (i `LT` j)
-isLT VZ     VZ     = No uninhabited
-isLT VZ     (VS j) = Yes LTZ
-isLT (VS i) VZ     = No uninhabited
-isLT (VS i) (VS j) with (isLT i j)
-  _ | Yes prf   = Yes (LTS prf)
-  _ | No contra = No  (\case LTS p => contra p)
-
-
-public export
-data Compare : (i, j : Var n) -> Type where
-  IsLT : (lt : i `LT` j) -> Compare i j
-  IsEQ :                    Compare i i
-  IsGT : (gt : i `GT` j) -> Compare i j
-%name Compare cmp
-
-export
-compareS : Compare i j -> Compare (VS i) (VS j)
-compareS (IsLT lt) = IsLT (LTS lt)
-compareS IsEQ      = IsEQ
-compareS (IsGT gt) = IsGT (LTS gt)
-
-export
-compareP : (i, j : Var n) -> Compare i j
-compareP VZ     VZ     = IsEQ
-compareP VZ     (VS j) = IsLT LTZ
-compareP (VS i) VZ     = IsGT LTZ
-compareP (VS i) (VS j) = compareS $ compareP i j
-
-
-public export
-data LTE : Var n -> Var n -> Type where
-  LTEZ : VZ `LTE` j
-  LTES : i  `LTE` j -> VS i `LTE` VS j
-
-export
-Reflexive (Var n) LTE where
-  reflexive {x = VZ}   = LTEZ
-  reflexive {x = VS i} = LTES $ reflexive {x=i}
-
-export
-Transitive (Var n) LTE where
-  transitive LTEZ     q        = LTEZ
-  transitive (LTES p) (LTES q) = LTES $ transitive p q {rel=Var.LTE}
-
-export
-Antisymmetric (Var n) LTE where
-  antisymmetric LTEZ     LTEZ     = Refl
-  antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q {rel=Var.LTE}
-
-export
-splitLTE : {j : Var n} -> i `Var.LTE` j -> Either (i = j) (i `Var.LT` j)
-splitLTE {j = VZ}   LTEZ     = Left Refl
-splitLTE {j = VS _} LTEZ     = Right LTZ
-splitLTE            (LTES p) with (splitLTE p)
-  _ | (Left  eq) = Left $ cong VS eq
-  _ | (Right lt) = Right $ LTS lt
diff --git a/src/Quox/Typecheck.idr b/src/Quox/Typecheck.idr
new file mode 100644
index 0000000..7d0454f
--- /dev/null
+++ b/src/Quox/Typecheck.idr
@@ -0,0 +1,152 @@
+module Quox.Typecheck
+
+import Quox.Syntax
+import Quox.Error
+import Quox.Context
+
+import Data.Nat
+import Control.Monad.Reader
+import Control.Monad.State
+
+
+%default total
+
+public export
+DContext : Nat -> Type
+DContext = Context Dim
+
+public export
+TContext : Nat -> Nat -> Type
+TContext d = Context (Term d)
+
+public export
+QContext : Nat -> Type
+QContext = Triangle' Qty
+
+public export
+QOutput : Nat -> Type
+QOutput = Context' Qty
+
+
+namespace TContext
+  export
+  pushD : TContext d n -> TContext (S d) n
+  pushD tel = map (/// shift 1) tel
+
+
+namespace Zero
+  public export
+  data IsZero : QOutput n -> Type where
+    LinZ  : IsZero [<]
+    SnocZ : IsZero qctx -> IsZero (qctx :< Zero)
+
+  export
+  isZeroIrrel : {qctx : _} -> (0 _ : IsZero qctx) -> IsZero qctx
+  isZeroIrrel {qctx = [<]}    LinZ      = LinZ
+  isZeroIrrel {qctx = _ :< _} (SnocZ x) = SnocZ $ isZeroIrrel x
+
+  export
+  zero : Context _ n -> Subset (QOutput n) IsZero
+  zero [<]        = Element [<] LinZ
+  zero (ctx :< _) = let zeroN = zero ctx in
+                    Element (zeroN.fst :< Zero) (SnocZ zeroN.snd)
+
+
+namespace Only
+  public export
+  data IsOnly : QOutput n -> Var n -> Type where
+    Here  : IsZero qctx   -> IsOnly (qctx :< One) VZ
+    There : IsOnly qctx i -> IsOnly (qctx :< Zero) (VS i)
+
+  export
+  isOnlyIrrel : {qctx, i : _} -> (0 _ : IsOnly qctx i) -> IsOnly qctx i
+  isOnlyIrrel {i = VZ}     (Here  z) = Here  $ isZeroIrrel z
+  isOnlyIrrel {i = (VS i)} (There o) = There $ isOnlyIrrel o
+
+  export
+  only : Context _ n -> (i : Var n) ->
+         Subset (QOutput n) (\qctx => IsOnly qctx i)
+  only (ctx :< _) VZ     =
+    let zeroN = zero ctx in
+    Element (zeroN.fst :< One) (Here zeroN.snd)
+  only (ctx :< _) (VS i) =
+    let onlyN = only ctx i in
+    Element (onlyN.fst :< Zero) (There onlyN.snd)
+
+
+public export
+data LT : Universe -> Universe -> Type where
+  Fin : k `LT` l -> U k `LT` U l
+  Any : U _ `LT` UAny
+
+
+namespace Lookup
+  public export
+  data IsLookup :
+      (tctx : TContext d n) ->
+      (i    : Var n) ->
+      (ty   : Term d from) ->
+      (by   : Shift from n) -> Type
+    where
+      Here  : IsLookup {tctx=(tctx :< ty), i=VZ, ty, by=(SS SZ)}
+      There : IsLookup {tctx, i, ty, by} ->
+              IsLookup {tctx=(tctx :< ty'), i=(VS i), ty, by=(SS by)}
+
+  public export
+  record Lookup {0 d, n : Nat} (0 tctx : TContext d n) (0 i : Var n) where
+    constructor MkLookup
+    qtys : QOutput n
+    type : Term d from
+    by   : Shift from n
+    0 only : IsOnly qtys i
+    0 look : IsLookup tctx i type by
+
+export
+lookup : (ctx : TContext d n) -> (i : Var n) -> Lookup tctx i
+lookup (ctx :< x) VZ =
+  ?lookup_rhs_3
+lookup (ctx :< x) (VS i) =
+  ?lookup_rhs_4
+
+
+
+mutual
+  public export
+  data HasTypeT :
+      (dctx : DContext d) ->
+      (tctx : TContext d n) ->
+      (qctx : QContext n) ->
+      (subj : Term d n) ->
+      (ty   : Term d n) ->
+      (tmout, tyout : QOutput n) ->
+      Type
+    where
+      TYPE :
+        WfCtx {dctx, tctx, qctx} ->
+        k `LT` l ->
+        (0 _ : IsZero tmout) -> (0 _ : IsZero tyout) ->
+        HasTypeT {dctx, tctx, qctx, subj=(TYPE k), ty=(TYPE l), tmout, tyout}
+
+  public export
+  data HasTypeE :
+      (dctx : DContext d) ->
+      (tctx : TContext d n) ->
+      (qctx : QContext n) ->
+      (subj : Elim d n) ->
+      (ty   : Term d n) ->
+      (tmout, tyout : QOutput n) ->
+      Type
+    where
+
+  public export
+  data WfCtx :
+      (dctx : DContext d) ->
+      (tctx : TContext d n) ->
+      (qctx : QContext n) ->
+      Type
+    where
+      NIL  : WfCtx [<] [<] [<]
+      BIND :
+        WfCtx    {dctx, tctx, qctx} ->
+        HasTypeT {dctx, tctx, qctx, subj=a, ty=(TYPE l), tmout, tyout} ->
+        WfCtx    {dctx, tctx=(tctx :< a), qctx=(qctx :< tmout)}
diff --git a/src/Quox/Typechecker.idr b/src/Quox/Typechecker.idr
deleted file mode 100644
index ec73f8f..0000000
--- a/src/Quox/Typechecker.idr
+++ /dev/null
@@ -1,168 +0,0 @@
-module Quox.Typechecker
-
-import public Quox.Syntax
-import public Quox.Typing
-import Quox.Error
-
-import Data.Nat
-import Data.SortedMap
-import Control.Monad.Reader
-import Control.Monad.State
-import Syntax.WithProof
-
-%default total
-
-
-public export
-data Error : Type where
-  ExpectedType : (subj, ty : Term d n) -> Error
-  UniverseInconsistency : (lo, hi : Universe) -> Error
-  GlobalNotInScope : Name -> Error
-
-public export
-record CheckResult
-  {0 d, n : Nat}
-  (0 ctx : WfContext d n)
-  (0 subj, ty : Term d n)
-where
-  constructor MkCheckResult
-  tmout, tyout : QOutput n
-  hasType : HasTypeT {ctx = ctx.ctx, subj, ty, tmout, tyout}
-
-
-public export
-record InferResult
-  {0 d, n : Nat}
-  (0 ctx : WfContext d n)
-  (0 subj : Elim d n)
-where
-  constructor MkInferResult
-  tmout, tyout : QOutput n
-  ty : Term d n
-  hasType : HasTypeE {ctx = ctx.ctx, subj, ty, tmout, tyout}
-
-
-public export
-zeroCtx : Globals -> TyContext 0 0
-zeroCtx globals = MkTyContext {globals, dctx = DNil, tctx = [<], qctx = [<]}
-
-public export
-zeroWfCtx : Globals -> WfContext 0 0
-zeroWfCtx globals = MkWfContext (zeroCtx globals) NIL
-
-public export
-Check0 : (globals : Globals) -> (subj, ty : Term 0 0) -> Type
-Check0 globals subj ty =
-  HasTypeT {ctx = zeroCtx globals, subj, ty, tmout = [<], tyout = [<]}
-
-public export
-record Infer0 (globals : Globals) (subj : Elim 0 0) where
-  constructor MkInfer0
-  ty : Term 0 0
-  hasType : HasTypeE {ctx = zeroCtx globals, subj, ty, tmout = [<], tyout = [<]}
-
-
-export
-0 isTypeZeroTyout : HasTypeT {ty = TYPE _, tyout, _} -> IsZero tyout
-isTypeZeroTyout (TYPE  {zty, _}) = zty
-isTypeZeroTyout (Pi    {zty, _}) = zty
-isTypeZeroTyout (PushT {})   = ?isTypeZeroTyout_PushT
-
-
-parameters {auto _ : MonadThrow Error m} mutual
-  private
-  checkUniverse : (lo, hi : Universe) -> m (lo `LT` hi)
-  checkUniverse lo hi with (lo `isLT` hi)
-    _ | Yes lt = pure lt
-    _ | No  _  = throw $ UniverseInconsistency {lo, hi}
-
-  private
-  expectType : (subj, ty : Term d n) ->
-               m (l : Universe ** ty = TYPE l)
-  expectType _    (TYPE l) = pure (l ** Refl)
-  expectType subj ty       = throw $ ExpectedType {subj, ty}
-
-  private
-  checkType : (ctx : WfContext d n) ->
-              (l : Universe) -> (ty : Term d n) ->
-              m (CheckResult ctx (TYPE l) ty)
-  checkType (MkWfContext {ctx, wf}) l ty = do
-    (l' ** eq) <- expectType (TYPE l) ty; let Refl = eq
-    lt <- checkUniverse l l'
-    let Element _ zprf = zero ctx.qctx
-    pure $ MkCheckResult {hasType = TYPE {wf, lt, ztm = zprf, zty = zprf}, _}
-
-  private
-  checkPi : (ctx : WfContext d n) ->
-            (qtm, qty : Qty) ->
-            (x : Name) ->
-            (arg : Term d n) ->
-            (res : Term d (S n)) ->
-            (ty  : Term d n) ->
-            m (CheckResult ctx (Pi qtm qty x arg res) ty)
-  checkPi (MkWfContext {ctx, wf}) qtm qty x arg res ty = do
-    let whole = Pi qtm qty x arg res
-    (l' ** eq) <- expectType whole ty; let Refl = eq
-    ?checkPi_rhs
-
-
-  private
-  inferFree : (ctx : WfContext {}) -> (x : Name) -> m (InferResult ctx (F x))
-  inferFree (MkWfContext {ctx, wf}) x =
-    case @@ lookup x ctx.globals of
-      (Just g ** eq) =>
-        let Element _ zprf = zero ctx.tctx
-            hasType = F {wf, g, eq, ztm = zprf, zty = zprf}
-        in
-        pure $ MkInferResult {hasType, _}
-      _ => throw $ GlobalNotInScope x
-
-  private
-  inferBound : (ctx : WfContext _ n) -> (i : Var n) -> m (InferResult ctx (B i))
-  inferBound (MkWfContext {ctx, wf}) i =
-    pure $ MkInferResult {hasType = B {wf, look = lookup ctx i, eq = Refl}, _}
-
-  private
-  inferAnn : (ctx : WfContext d n) -> (tm, ty : Term d n) ->
-             m (InferResult ctx (tm :# ty))
-  inferAnn ctx tm ty = do
-    ignore $ check ctx ty (TYPE UAny)
-    MkCheckResult {hasType, _} <- check ctx tm ty
-    pure $ MkInferResult {hasType = Ann hasType, _}
-
-
-  export
-  check : (ctx : WfContext d n) -> (subj, ty : Term d n) ->
-          m (CheckResult ctx subj ty)
-  check ctx subj ty = case subj of
-    TYPE l               => checkType ctx l ty
-    Pi qtm qty x arg res => checkPi ctx qtm qty x arg res ty
-    Lam x body           => ?check_rhs_3
-    E e                  => ?check_rhs_4
-    CloT  s th           => ?check_rhs_5
-    DCloT s th           => ?check_rhs_6
-
-  export
-  infer : (ctx : WfContext d n) -> (subj : Elim d n) ->
-          m (InferResult ctx subj)
-  infer ctx subj = case subj of
-    F x        => inferFree ctx x
-    B i        => inferBound ctx i
-    fun :@ arg => ?infer_rhs_3
-    tm :# ty   => inferAnn ctx tm ty
-    CloE  e th => ?infer_rhs_5
-    DCloE e th => ?infer_rhs_6
-
-
-parameters {auto _ : MonadThrow Error m} (globals : Globals)
-  public export
-  check0 : (subj, ty : Term 0 0) -> m (Check0 globals subj ty)
-  check0 subj ty = pure $
-    case !(check (zeroWfCtx globals) subj ty) of
-      MkCheckResult [<] [<] prf => prf
-
-  public export
-  infer0 : (subj : Elim 0 0) -> (ty : Term 0 0) -> m (Infer0 globals subj)
-  infer0 subj ty = pure $
-    case !(infer (zeroWfCtx globals) subj) of
-      MkInferResult [<] [<] ty prf => MkInfer0 ty prf
diff --git a/src/Quox/Typing.idr b/src/Quox/Typing.idr
deleted file mode 100644
index 4a4ae31..0000000
--- a/src/Quox/Typing.idr
+++ /dev/null
@@ -1,280 +0,0 @@
-module Quox.Typing
-
-import public Quox.Syntax
-import public Quox.Context
-
-import Data.Nat
-import Data.SortedMap
-import Control.Monad.Reader
-import Control.Monad.State
-
-
-%default total
-
-public export
-data DContext : Nat -> Type where
-  DNil  : DContext 0
-  DBind : DContext d -> DContext (S d)
-  DEq   : Dim d -> Dim d -> DContext d -> DContext d
-
-public export
-TContext : Nat -> Nat -> Type
-TContext d = Context (Term d)
-
-public export
-QContext : Nat -> Type
-QContext = Triangle' Qty
-
-public export
-QOutput : Nat -> Type
-QOutput = Context' Qty
-
-
-public export
-record Global where
-  constructor MkGlobal
-  type, term : forall d, n. Term d n
-
-public export
-Globals : Type
-Globals = SortedMap Name Global
-
-
-public export
-record TyContext (d, n : Nat) where
-  constructor MkTyContext
-  globals : Globals
-  dctx : DContext d
-  tctx : TContext d n
-  qctx : QContext n
-
-%name TyContext ctx
-
-
-namespace TContext
-  export
-  pushD : TContext d n -> TContext (S d) n
-  pushD tel = map (/// shift 1) tel
-
-
-namespace TyContext
-  export
-  extendTy : Term d n -> QOutput n -> TyContext d n -> TyContext d (S n)
-  extendTy s rhos = {tctx $= (:< s), qctx $= (:< rhos)}
-
-  export
-  extendDim : TyContext d n -> TyContext (S d) n
-  extendDim = {dctx $= DBind, tctx $= pushD}
-
-  export
-  eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
-  eqDim p q = {dctx $= DEq p q}
-
-
-
-namespace QOutput
-  export
-  (+) : QOutput n -> QOutput n -> QOutput n
-  (+) = zipWith (+)
-
-  export
-  (*) : Qty -> QOutput n -> QOutput n
-  (*) pi = map (pi *)
-
-
-namespace Zero
-  public export
-  data IsZero : QOutput n -> Type where
-    LinZ  : IsZero [<]
-    SnocZ : IsZero qctx -> IsZero (qctx :< Zero)
-
-  export
-  isZeroIrrel : {qctx : _} -> (0 _ : IsZero qctx) -> IsZero qctx
-  isZeroIrrel {qctx = [<]}    LinZ      = LinZ
-  isZeroIrrel {qctx = _ :< _} (SnocZ x) = SnocZ $ isZeroIrrel x
-
-  export
-  zero : Context _ n -> Subset (QOutput n) IsZero
-  zero [<]        = Element [<] LinZ
-  zero (ctx :< _) = let zeroN = zero ctx in
-                    Element (zeroN.fst :< Zero) (SnocZ zeroN.snd)
-
-
-namespace Only
-  public export
-  data IsOnly : QOutput n -> Var n -> Type where
-    Here  : IsZero qctx   -> IsOnly (qctx :< One) VZ
-    There : IsOnly qctx i -> IsOnly (qctx :< Zero) (VS i)
-
-  export
-  isOnlyIrrel : {qctx, i : _} -> (0 _ : IsOnly qctx i) -> IsOnly qctx i
-  isOnlyIrrel {i = VZ}     (Here  z) = Here  $ isZeroIrrel z
-  isOnlyIrrel {i = (VS i)} (There o) = There $ isOnlyIrrel o
-
-  export
-  only : Context _ n -> (i : Var n) ->
-         Subset (QOutput n) (\qctx => IsOnly qctx i)
-  only (ctx :< _) VZ     =
-    let zeroN = zero ctx in
-    Element (zeroN.fst :< One) (Here zeroN.snd)
-  only (ctx :< _) (VS i) =
-    let onlyN = only ctx i in
-    Element (onlyN.fst :< Zero) (There onlyN.snd)
-
-
-namespace Universe
-  public export
-  data LT : Universe -> Universe -> Type where
-    Fin : k `LT` l -> U k `LT` U l
-    Any : U _ `LT` UAny
-
-  export
-  Uninhabited (UAny `LT` j) where
-    uninhabited _ impossible
-
-  export
-  isLT : (i, j : Universe) -> Dec (i `LT` j)
-  isLT (U i) (U j) with (i `isLT` j)
-    _ | Yes prf   = Yes $ Fin prf
-    _ | No contra = No  $ \(Fin prf) => contra prf
-  isLT (U _) UAny = Yes Any
-  isLT UAny  _    = No uninhabited
-
-
-namespace Lookup
-  public export
-  data IsLookup :
-      (tctx : TContext d n) ->
-      (i    : Var n) ->
-      (ty   : Term d from) ->
-      (by   : Shift from n) -> Type
-    where
-      Here  : IsLookup {tctx=(tctx :< ty), i=VZ, ty, by=(SS SZ)}
-      There : IsLookup {tctx, i, ty, by} ->
-              IsLookup {tctx=(tctx :< ty'), i=(VS i), ty, by=(SS by)}
-
-  public export
-  record Lookup'
-    {0 d, n : Nat}
-    (0 tctx : TContext d n)
-    (0 qctx : QContext n)
-    (0 i : Var n)
-  where
-    constructor MkLookup
-    tmout, tyout : QOutput n
-    type : Term d from
-    by   : Shift from n
-    0 only : IsOnly tmout i
-    0 look : IsLookup tctx i type by
-
-  public export
-  lookup' : (tctx : TContext d n) -> (qctx : QContext n) ->
-            (i : Var n) -> Lookup' tctx qctx i
-  lookup' tctx@(_ :< _) (_ :< tyout) VZ =
-    MkLookup {only = (only tctx VZ).snd, look = Here,
-              tyout = tyout :< Zero, _}
-  lookup' (tctx :< _) (qctx :< _) (VS i) =
-    let inner = lookup' tctx qctx i in
-    MkLookup {only = There inner.only, look = There inner.look,
-              tyout = inner.tyout :< Zero, _}
-
-
-  public export %inline
-  Lookup : TyContext d n -> Var n -> Type
-  Lookup ctx i = Lookup' ctx.tctx ctx.qctx i
-
-  public export %inline
-  lookup : (ctx : TyContext d n) -> (i : Var n) -> Lookup ctx i
-  lookup ctx = lookup' ctx.tctx ctx.qctx
-
-
-
-mutual
-  public export
-  data HasTypeT :
-      {0 d, n : Nat} ->
-      (ctx  : TyContext d n) ->
-      (subj : Term d n) ->
-      (ty   : Term d n) ->
-      (tmout, tyout : QOutput n) ->
-      Type
-    where
-      TYPE :
-        (0 wf : IsWf ctx) ->
-        (lt : k `LT` l) ->
-        (0 ztm : IsZero tmout) -> (0 zty : IsZero tyout) ->
-        HasTypeT {ctx, subj = TYPE k, ty = TYPE l, tmout, tyout}
-      Pi :
-        (tyA : HasTypeT {ctx, subj = a, ty = TYPE l, tmout = tmoutA, tyout}) ->
-        (tyB : HasTypeT {ctx = extendTy a tmoutA ctx, subj = b, ty = TYPE l,
-                         tmout = tmoutB :< qty, tyout = tyout :< Zero}) ->
-        (0 zty : IsZero tyout) ->
-        HasTypeT {ctx, subj = Pi qtm qty x a b, ty = TYPE l,
-                  tmout = tmoutA + tmoutB, tyout}
-      PushT :
-        (0 eq : ty' = pushSubstsT' ty) ->
-        (j : HasTypeT {ctx, subj, ty = ty', tmout, tyout}) ->
-        HasTypeT {ctx, subj, ty, tmout, tyout}
-
-  public export
-  data HasTypeE :
-      {0 d, n : Nat} ->
-      (ctx  : TyContext d n) ->
-      (subj : Elim d n) ->
-      (ty   : Term d n) ->
-      (tmout, tyout : QOutput n) ->
-      Type
-    where
-      F :
-        (0 wf : IsWf ctx) ->
-        (g : Global) ->
-        (0 eq : lookup x ctx.globals = Just g) ->
-        (0 ztm : IsZero tmout) -> (0 zty : IsZero tyout) ->
-        HasTypeE {ctx, subj = F x, ty = g.type, tmout, tyout}
-      B :
-        {0 ctx : TyContext d n} ->
-        (0 wf : IsWf ctx) ->
-        (look : Lookup ctx i) ->
-        (0 eq : ty = look.type // look.by) ->
-        HasTypeE {ctx, subj = B i, ty, tmout = look.tmout, tyout = look.tyout}
-      Ann :
-        HasTypeT {ctx, subj = tm,       ty, tmout, tyout} ->
-        HasTypeE {ctx, subj = tm :# ty, ty, tmout, tyout}
-      PushE :
-        (0 eq : ty' = pushSubstsT' ty) ->
-        HasTypeE {ctx, subj, ty = ty', tmout, tyout} ->
-        HasTypeE {ctx, subj, ty, tmout, tyout}
-
-  public export
-  data IsWf' :
-      (globals : Globals) ->
-      (dctx : DContext d) ->
-      (tctx : TContext d n) ->
-      (qctx : QContext n) -> Type
-    where
-      NIL  : IsWf' globals dctx [<] [<]
-      BIND :
-        IsWf' {globals, dctx, tctx, qctx} ->
-        HasTypeT {ctx = MkTyContext {globals, dctx, tctx, qctx},
-                  subj, ty = TYPE l, tmout, tyout} ->
-        IsWf' {globals, dctx, tctx = tctx :< subj, qctx = qctx :< tmout}
-
-  public export %inline
-  IsWf : TyContext d n -> Type
-  IsWf (MkTyContext {globals, dctx, tctx, qctx}) =
-    IsWf' {globals, dctx, tctx, qctx}
-
-public export
-record WfContext (d, n : Nat) where
-  constructor MkWfContext
-  ctx  : TyContext d n
-  0 wf : IsWf ctx
-
-
-public export
-record TypeTerm {0 d, n : Nat} (ctx : TyContext d n) where
-  constructor MkTypeTerm
-  term : Term d n
-  univ : Universe
-  tmout, tyout : QOutput n
-  isType : HasTypeT {ctx, subj = term, ty = TYPE univ, tmout, tyout}