diff --git a/exe/Main.idr b/exe/Main.idr
index 5d0bf4f..bee32d7 100644
--- a/exe/Main.idr
+++ b/exe/Main.idr
@@ -5,6 +5,7 @@ import public Quox.Syntax
 import public Quox.Equal
 import public Quox.Pretty
 import public Quox.Typechecker
+import public Quox.Syntax.Qty.Three
 
 import Data.Nat
 import Data.Vect
@@ -53,7 +54,7 @@ banner : PrettyOpts -> String
 banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
 
 export
-tm : Term 1 2
+tm : Term Three 1 2
 tm =
   (Pi One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
     `DCloT` (K One ::: id))
diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 33298e2..3e846c8 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -2,49 +2,66 @@ module Quox.Definition
 
 import public Quox.Syntax
 import public Data.SortedMap
-import public Control.Monad.State
+import public Control.Monad.Reader
+import Decidable.Decidable
 
 
 public export
-record AnyTerm where
+record AnyTerm q where
   constructor T
-  get : forall d, n. Term d n
+  get : forall d, n. Term q d n
 
 public export
-record Definition where
+record Definition' q (isGlobal : q -> Type) where
   constructor MkDef'
-  qty  : Qty
-  type : AnyTerm
-  term : Maybe AnyTerm
-  {auto 0 qtyGlobal : IsGlobal qty}
+  qty  : q
+  type : AnyTerm q
+  term : Maybe $ AnyTerm q
+  {auto 0 qtyGlobal : isGlobal qty}
+
+public export
+0 Definition : (q : Type) -> IsQty q => Type
+Definition q = Definition' q IsGlobal
 
 public export %inline
-mkDef : (qty : Qty) -> (0 _ : IsGlobal qty) =>
-        (type, term : forall d, n. Term d n) -> Definition
+mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
+        (type, term : forall d, n. Term q d n) -> Definition q
 mkDef qty type term = MkDef' {qty, type = T type, term = Just (T term)}
 
 public export %inline
-mkAbstract : (qty : Qty) -> (0 _ : IsGlobal qty) =>
-             (type : forall d, n. Term d n) -> Definition
+mkAbstract : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
+             (type : forall d, n. Term q d n) -> Definition q
 mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}
 
 
 public export %inline
-(.type0) : Definition -> Term 0 0
+(.type0) : Definition' q _ -> Term q 0 0
 g.type0 = g.type.get
 
 public export %inline
-(.term0) : Definition -> Maybe (Term 0 0)
+(.term0) : Definition' q _ -> Maybe (Term q 0 0)
 g.term0 = map (\t => t.get) g.term
 
 public export %inline
-(.qtyP) : Definition -> Subset Qty IsGlobal
+(.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
 g.qtyP = Element g.qty g.qtyGlobal
 
 public export %inline
-isZero : Definition -> Bool
-isZero g = g.qty == Zero
+isZero : IsQty q => Definition q -> Bool
+isZero g = isYes $ isZero g.qty
 
 public export
-Definitions : Type
-Definitions = SortedMap Name Definition
+0 Definitions' : (q : Type) -> (q -> Type) -> Type
+Definitions' q isGlobal = SortedMap Name $ Definition' q isGlobal
+
+public export
+0 Definitions : (q : Type) -> IsQty q => Type
+Definitions q = Definitions' q IsGlobal
+
+
+public export
+0 HasDefs' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+HasDefs' q isGlobal = MonadReader (Definitions' q isGlobal)
+
+0 HasDefs : (q : Type) -> IsQty q => (Type -> Type) -> Type
+HasDefs q = HasDefs' q IsGlobal
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index cbbf6cc..978a65f 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -9,194 +9,228 @@ import Data.Maybe
 
 
 private %inline
-ClashE : EqMode -> Elim d n -> Elim d n -> Error
+ClashE : EqMode -> Elim q d n -> Elim q d n -> Error q
 ClashE mode = ClashT mode `on` E
 
 
 public export
-record Env where
+record Env' q (isGlobal : q -> Type) where
   constructor MakeEnv
-  defs : Definitions
+  defs : Definitions' q isGlobal
   mode : EqMode
 
+public export
+0 Env : (q : Type) -> IsQty q => Type
+Env q = Env' q IsGlobal
 
-parameters {auto _ : MonadError Error m} {auto _ : MonadReader Env m}
-  private %inline
-  mode : m EqMode
-  mode = asks mode
+public export
+0 HasEnv' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+HasEnv' q isGlobal = MonadReader (Env' q isGlobal)
 
-  private %inline
-  clashT : Term d n -> Term d n -> m a
-  clashT s t = throwError $ ClashT !mode s t
-
-  private %inline
-  clashE : Elim d n -> Elim d n -> m a
-  clashE e f = throwError $ ClashE !mode e f
-
-  private %inline
-  defE : Name -> m (Maybe (Elim d n))
-  defE x = asks $ \env => do
-    g <- lookup x env.defs
-    pure $ (!g.term).get :# g.type.get
-
-  private %inline
-  defT : Name -> m (Maybe (Term d n))
-  defT x = map E <$> defE x
-
-  export %inline
-  compareU' : Universe -> Universe -> m Bool
-  compareU' i j = pure $ 
-    case !mode of Equal => i == j; Sub => i <= j
-
-  export %inline
-  compareU : Universe -> Universe -> m ()
-  compareU k l = unless !(compareU' k l) $
-    throwError $ ClashU !mode k l
-
-  mutual
-    private covering
-    compareTN' : (s, t : Term 0 n) ->
-                 (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
-
-    compareTN' (E e) (E f) ps pt = compareE0 e f
-    -- if either term is a def, try to unfold it
-    compareTN' s@(E (F x)) t ps pt = do
-      Just s' <- defT x  | Nothing => clashT s t
-      compareT0 s' t
-    compareTN' s t@(E (F y)) ps pt = do
-      Just t' <- defT y  | Nothing => clashT s t
-      compareT0 s t'
-    compareTN' s@(E _) t _ _ = clashT s t
-
-    compareTN' (TYPE k) (TYPE l) _ _ = compareU k l
-    compareTN' s@(TYPE _) t _ _ = clashT s t
-
-    compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
-      unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
-      compareT0  arg2 arg1 -- reversed for contravariant domain
-      compareTS0 res1 res2
-    compareTN' s@(Pi {}) t _ _ = clashT s t
-
-    -- [todo] eta
-    compareTN' (Lam _ body1) (Lam _ body2) _ _ =
-      local {mode := Equal} $ compareTS0 body1 body2
-    compareTN' s@(Lam {}) t _ _ = clashT s t
-
-    compareTN' (CloT  {}) _ ps _ = void $ ps IsCloT
-    compareTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
-
-    private covering
-    compareEN' : (e, f : Elim 0 n) ->
-                 (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
-
-    compareEN' e@(F x) f@(F y) _ _ =
-      if x == y then pure () else
-      case (!(defE x), !(defE y)) of
-           (Nothing, Nothing) => clashE e f
-           (s', t') => compareE0 (fromMaybe e s') (fromMaybe f t')
-    compareEN' e@(F x) f _ _ = do
-      Just e' <- defE x  | Nothing => clashE e f
-      compareE0 e' f
-    compareEN' e f@(F y) _ _ = do
-      Just f' <- defE y  | Nothing => clashE e f
-      compareE0 e f'
-
-    compareEN' e@(B i) f@(B j) _ _ =
-      unless (i == j) $ clashE e f
-    compareEN' e@(B _) f _ _ = clashE e f
-
-    -- [todo] tracking variance of functions? maybe???
-    -- probably not
-    compareEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
-      local {mode := Equal} $ do
-        compareE0 fun1 fun2
-        compareT0 arg1 arg2
-    compareEN' e@(_ :@ _) f _ _ = clashE e f
-
-    -- [todo] is always checking the types are equal correct?
-    compareEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
-      compareT0 tm1 tm2
-      local {mode := Equal} $ compareT0 ty1 ty2
-    compareEN' e@(_ :# _) f _ _ = clashE e f
-
-    compareEN' (CloE  {}) _ pe _ = void $ pe IsCloE
-    compareEN' (DCloE {}) _ pe _ = void $ pe IsDCloE
+public export
+0 HasEnv : (q : Type) -> IsQty q => (Type -> Type) -> Type
+HasEnv q = HasEnv' q IsGlobal
 
 
-    private covering %inline
-    compareTN : NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
-    compareTN s t = compareTN' s.fst t.fst s.snd t.snd
+public export
+0 CanEqual' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+CanEqual' q isGlobal m = (HasErr q m, HasEnv' q isGlobal m)
 
-    private covering %inline
-    compareEN : NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
-    compareEN e f = compareEN' e.fst f.fst e.snd f.snd
+public export
+0 CanEqual : (q : Type) -> IsQty q => (Type -> Type) -> Type
+CanEqual q = CanEqual' q IsGlobal
 
 
-    export covering %inline
-    compareT : DimEq d -> Term d n -> Term d n -> m ()
-    compareT eqs s t =
-      for_ (splits eqs) $ \th => compareT0 (s /// th) (t /// th)
 
-    export covering %inline
-    compareE : DimEq d -> Elim d n -> Elim d n -> m ()
-    compareE eqs e f =
-      for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th)
+private %inline
+mode : HasEnv' _ _ m => m EqMode
+mode = asks mode
+
+private %inline
+clashT : CanEqual' q _ m => Term q d n -> Term q d n -> m a
+clashT s t = throwError $ ClashT !mode s t
+
+private %inline
+clashE : CanEqual' q _ m => Elim q d n -> Elim q d n -> m a
+clashE e f = throwError $ ClashE !mode e f
+
+private %inline
+defE : HasEnv' q _ m => Name -> m (Maybe (Elim q d n))
+defE x = asks $ \env => do
+  g <- lookup x env.defs
+  pure $ (!g.term).get :# g.type.get
+
+private %inline
+defT : HasEnv' q _ m => Name -> m (Maybe (Term q d n))
+defT x = map E <$> defE x
+
+export %inline
+compareU' : HasEnv' q _ m => Universe -> Universe -> m Bool
+compareU' i j = pure $
+  case !mode of Equal => i == j; Sub => i <= j
+
+export %inline
+compareU : CanEqual' q _ m => Universe -> Universe -> m ()
+compareU k l = unless !(compareU' k l) $
+  throwError $ ClashU !mode k l
+
+mutual
+  private covering
+  compareTN' : CanEqual' q _ m => Eq q =>
+               (s, t : Term q 0 n) ->
+               (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
+
+  compareTN' (E e) (E f) ps pt = compareE0 e f
+  -- if either term is a def, try to unfold it
+  compareTN' s@(E (F x)) t ps pt = do
+    Just s' <- defT x  | Nothing => clashT s t
+    compareT0 s' t
+  compareTN' s t@(E (F y)) ps pt = do
+    Just t' <- defT y  | Nothing => clashT s t
+    compareT0 s t'
+  compareTN' s@(E _) t _ _ = clashT s t
+
+  compareTN' (TYPE k) (TYPE l) _ _ = compareU k l
+  compareTN' s@(TYPE _) t _ _ = clashT s t
+
+  compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
+    unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
+    compareT0  arg2 arg1 -- reversed for contravariant domain
+    compareTS0 res1 res2
+  compareTN' s@(Pi {}) t _ _ = clashT s t
+
+  -- [todo] eta
+  compareTN' (Lam _ body1) (Lam _ body2) _ _ =
+    local {mode := Equal} $ compareTS0 body1 body2
+  compareTN' s@(Lam {}) t _ _ = clashT s t
+
+  compareTN' (CloT  {}) _ ps _ = void $ ps IsCloT
+  compareTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
+
+  private covering
+  compareEN' : CanEqual' q _ m => Eq q =>
+               (e, f : Elim q 0 n) ->
+               (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
+
+  compareEN' e@(F x) f@(F y) _ _ =
+    if x == y then pure () else
+    case (!(defE x), !(defE y)) of
+         (Nothing, Nothing) => clashE e f
+         (s', t') => compareE0 (fromMaybe e s') (fromMaybe f t')
+  compareEN' e@(F x) f _ _ = do
+    Just e' <- defE x  | Nothing => clashE e f
+    compareE0 e' f
+  compareEN' e f@(F y) _ _ = do
+    Just f' <- defE y  | Nothing => clashE e f
+    compareE0 e f'
+
+  compareEN' e@(B i) f@(B j) _ _ =
+    unless (i == j) $ clashE e f
+  compareEN' e@(B _) f _ _ = clashE e f
+
+  -- [todo] tracking variance of functions? maybe???
+  -- probably not
+  compareEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
+    local {mode := Equal} $ do
+      compareE0 fun1 fun2
+      compareT0 arg1 arg2
+  compareEN' e@(_ :@ _) f _ _ = clashE e f
+
+  -- [todo] is always checking the types are equal correct?
+  compareEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
+    compareT0 tm1 tm2
+    local {mode := Equal} $ compareT0 ty1 ty2
+  compareEN' e@(_ :# _) f _ _ = clashE e f
+
+  compareEN' (CloE  {}) _ pe _ = void $ pe IsCloE
+  compareEN' (DCloE {}) _ pe _ = void $ pe IsDCloE
 
 
-    export covering %inline
-    compareT0 : Term 0 n -> Term 0 n -> m ()
-    compareT0 s t = compareTN (whnfT s) (whnfT t)
+  private covering %inline
+  compareTN : CanEqual' q _ m => Eq q =>
+              NonRedexTerm q 0 n -> NonRedexTerm q 0 n -> m ()
+  compareTN s t = compareTN' s.fst t.fst s.snd t.snd
 
-    export covering %inline
-    compareE0 : Elim 0 n -> Elim 0 n -> m ()
-    compareE0 e f = compareEN (whnfE e) (whnfE f)
-
-    export covering %inline
-    compareTS0 : ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
-    compareTS0 (TUnused body1) (TUnused body2) =
-      compareT0 body1 body2
-    compareTS0 body1 body2 =
-      compareT0 (fromScopeTerm body1) (fromScopeTerm body2)
-
-
-parameters {auto _ : MonadError Error m} {auto _ : MonadReader Definitions m}
-  private %inline
-  into : EqMode ->
-         (forall n. MonadError Error n => MonadReader Env n =>
-            DimEq d -> a -> a -> n ()) ->
-         DimEq d -> a -> a -> m ()
-  into mode f eqs a b =
-    runReaderT {m} (MakeEnv {mode, defs = !ask}) $ f eqs a b
-
-  export covering %inline
-  equalTWith : DimEq d -> Term d n -> Term d n -> m ()
-  equalTWith = into Equal compareT
-
-  export covering %inline
-  equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
-  equalEWith = into Equal compareE
-
-  export covering %inline
-  subTWith : DimEq d -> Term d n -> Term d n -> m ()
-  subTWith = into Sub compareT
-
-  export covering %inline
-  subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
-  subEWith = into Sub compareE
+  private covering %inline
+  compareEN : CanEqual' q _ m => Eq q =>
+              NonRedexElim q 0 n -> NonRedexElim q 0 n -> m ()
+  compareEN e f = compareEN' e.fst f.fst e.snd f.snd
 
 
   export covering %inline
-  equalT : {d : Nat} -> Term d n -> Term d n -> m ()
-  equalT = equalTWith DimEq.new
+  compareT : CanEqual' q _ m => Eq q =>
+             DimEq d -> Term q d n -> Term q d n -> m ()
+  compareT eqs s t =
+    for_ (splits eqs) $ \th => compareT0 (s /// th) (t /// th)
 
   export covering %inline
-  equalE : {d : Nat} -> Elim d n -> Elim d n -> m ()
-  equalE = equalEWith DimEq.new
+  compareE : CanEqual' q _ m => Eq q =>
+             DimEq d -> Elim q d n -> Elim q d n -> m ()
+  compareE eqs e f =
+    for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th)
+
 
   export covering %inline
-  subT : {d : Nat} -> Term d n -> Term d n -> m ()
-  subT = subTWith DimEq.new
+  compareT0 : CanEqual' q _ m => Eq q => Term q 0 n -> Term q 0 n -> m ()
+  compareT0 s t = compareTN (whnfT s) (whnfT t)
 
   export covering %inline
-  subE : {d : Nat} -> Elim d n -> Elim d n -> m ()
-  subE = subEWith DimEq.new
+  compareE0 : CanEqual' q _ m => Eq q => Elim q 0 n -> Elim q 0 n -> m ()
+  compareE0 e f = compareEN (whnfE e) (whnfE f)
+
+  export covering %inline
+  compareTS0 : CanEqual' q _ m => Eq q =>
+               ScopeTerm q 0 n -> ScopeTerm q 0 n -> m ()
+  compareTS0 (TUnused body1) (TUnused body2) =
+    compareT0 body1 body2
+  compareTS0 body1 body2 =
+    compareT0 (fromScopeTerm body1) (fromScopeTerm body2)
+
+
+private %inline
+into : HasErr q m => HasDefs' q isg m => Eq q =>
+       (forall n. HasErr q n => HasEnv' q isg n => d -> a -> a -> n ()) ->
+       EqMode -> d -> a -> a -> m ()
+into f mode eqs a b =
+  runReaderT {m} (MakeEnv {mode, defs = !ask}) $ f eqs a b
+
+export covering %inline
+equalTWith : HasErr q m => HasDefs' q _ m => Eq q =>
+             DimEq d -> Term q d n -> Term q d n -> m ()
+equalTWith = into compareT Equal
+
+export covering %inline
+equalEWith : HasErr q m => HasDefs' q _ m => Eq q =>
+             DimEq d -> Elim q d n -> Elim q d n -> m ()
+equalEWith = into compareE Equal
+
+export covering %inline
+subTWith : HasErr q m => HasDefs' q _ m => Eq q =>
+           DimEq d -> Term q d n -> Term q d n -> m ()
+subTWith = into compareT Sub
+
+export covering %inline
+subEWith : HasErr q m => HasDefs' q _ m => Eq q =>
+           DimEq d -> Elim q d n -> Elim q d n -> m ()
+subEWith = into compareE Sub
+
+
+export covering %inline
+equalT : HasErr q m => HasDefs' q _ m => Eq q =>
+         {d : Nat} -> Term q d n -> Term q d n -> m ()
+equalT = equalTWith DimEq.new
+
+export covering %inline
+equalE : HasErr q m => HasDefs' q _ m => Eq q =>
+         {d : Nat} -> Elim q d n -> Elim q d n -> m ()
+equalE = equalEWith DimEq.new
+
+export covering %inline
+subT : HasErr q m => HasDefs' q _ m => Eq q =>
+       {d : Nat} -> Term q d n -> Term q d n -> m ()
+subT = subTWith DimEq.new
+
+export covering %inline
+subE : HasErr q m => HasDefs' q _ m => Eq q =>
+       {d : Nat} -> Elim q d n -> Elim q d n -> m ()
+subE = subEWith DimEq.new
diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index 4ec000a..9063dd7 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -1,84 +1,78 @@
 module Quox.Syntax.Qty
 
 import Quox.Pretty
-
-import Data.Fin
-import Generics.Derive
+import Data.DPair
 
 %default total
-%language ElabReflection
 
 
-public export
-data Qty = Zero | One | Any
-%name Qty.Qty pi, rh
-
-%runElab derive "Qty" [Generic, Meta, Eq, Ord, DecEq, Show]
-
-
-export
-PrettyHL Qty where
-  prettyM pi = hl Qty <$>
-    case pi of
-      Zero => ifUnicode "𝟬" "0"
-      One  => ifUnicode "𝟭" "1"
-      Any  => ifUnicode "𝛚" "*"
-
 private
 commas : List (Doc HL) -> List (Doc HL)
-commas [] = []
-commas [x] = [x]
+commas []      = []
+commas [x]     = [x]
 commas (x::xs) = (x <+> hl Delim ",") :: commas xs
 
 export %inline
-prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
+prettyQtyBinds : Pretty.HasEnv m => PrettyHL q =>
+                 List q -> m (Doc HL)
 prettyQtyBinds =
   map ((hl Delim "@" <++>) . align . sep . commas) . traverse pretty0M
 
 
 public export
-plus : Qty -> Qty -> Qty
-plus Zero rh   = rh
-plus pi   Zero = pi
-plus _    _    = Any
-
-public export
-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
-compat : Qty -> Qty -> Bool
-compat pi rh = rh == Any || pi == rh
-
-
-public export
-interface IsQty q where
+interface Eq q => IsQty q where
   zero, one : q
   (+),  (*) : q -> q -> q
-  (<=.)     : q -> q -> Bool
+
+  ||| true if bindings of this quantity will be erased
+  ||| and must not be runtime relevant
+  IsZero : q -> Type
+  isZero : (pi : q) -> Dec (IsZero pi)
+  zeroIsZero : IsZero zero
+
+  ||| true if bindings of this quantity must be linear
+  -- [fixme] is this needed for anything?
+  IsOne : q -> Type
+  isOne : (pi : q) -> Dec (IsOne pi)
+  oneIsOne : IsOne one
+
+  ||| ``p `Compat` q`` if it is ok for a binding of
+  ||| quantity `q` to be used exactly `p` times.
+  ||| e.g. ``1 `Compat` 1``, ``1 `Compat` ω``
+  Compat : q -> q -> Type
+  compat : (pi, rh : q) -> Dec (pi `Compat` rh)
+
+  ||| true if it is ok for this quantity to appear for the
+  ||| subject of a typing judgement. this is about the
+  ||| subject reduction stuff in atkey
+  IsSubj : q -> Type
+  isSubj : (pi : q) -> Dec (IsSubj pi)
+  zeroIsSubj : IsSubj zero
+  oneIsSubj  : IsSubj one
+
+  ||| true if it is ok for a global definition to have this
+  ||| quantity. so not exact usage counts, maybe.
+  IsGlobal : q -> Type
+  isGlobal : (pi : q) -> Dec (IsGlobal pi)
+  zeroIsGlobal : IsGlobal zero
 
 public export
-IsQty Qty where
-  zero  = Zero; one = One
-  (+)   = plus; (*) = times
-  (<=.) = compat
+0 SQty : (q : Type) -> IsQty q => Type
+SQty q = Subset q IsSubj
 
+public export %inline
+szero : IsQty q => SQty q
+szero = Element zero zeroIsSubj
+
+public export %inline
+sone : IsQty q => SQty q
+sone = Element one oneIsSubj
 
 public export
-data IsSubj : Qty -> Type where
-  SZero : IsSubj Zero
-  SOne  : IsSubj One
+0 GQty : (q : Type) -> IsQty q => Type
+GQty q = Subset q IsGlobal
 
-export Uninhabited (IsSubj Any) where uninhabited _ impossible
+public export %inline
+gzero : IsQty q => GQty q
+gzero = Element zero zeroIsGlobal
 
-public export
-data IsGlobal : Qty -> Type where
-  GZero : IsGlobal Zero
-  GAny  : IsGlobal Any
-
-export Uninhabited (IsGlobal One) where uninhabited _ impossible
diff --git a/lib/Quox/Syntax/Qty/Three.idr b/lib/Quox/Syntax/Qty/Three.idr
new file mode 100644
index 0000000..13df037
--- /dev/null
+++ b/lib/Quox/Syntax/Qty/Three.idr
@@ -0,0 +1,111 @@
+module Quox.Syntax.Qty.Three
+
+import Quox.Pretty
+import public Quox.Syntax.Qty
+import Generics.Derive
+
+%default total
+%language ElabReflection
+
+
+public export
+data Three = Zero | One | Any
+%name Three pi, rh
+
+%runElab derive "Three" [Generic, Meta, Eq, Ord, DecEq, Show]
+
+
+export
+PrettyHL Three where
+  prettyM pi = hl Qty <$>
+    case pi of
+      Zero => ifUnicode "𝟬" "0"
+      One  => ifUnicode "𝟭" "1"
+      Any  => ifUnicode "𝛚" "*"
+
+
+public export
+plus : Three -> Three -> Three
+plus Zero rh   = rh
+plus pi   Zero = pi
+plus _    _    = Any
+
+public export
+times : Three -> Three -> Three
+times Zero _    = Zero
+times _    Zero = Zero
+times One  rh   = rh
+times pi   One  = pi
+times Any  Any  = Any
+
+public export
+data Compat3 : Three -> Three -> Type where
+  CmpRefl : Compat3 pi pi
+  CmpAny  : Compat3 pi Any
+
+public export
+compat3 : (pi, rh : Three) -> Dec (pi `Compat3` rh)
+compat3 pi rh with (decEq pi rh)
+  compat3 pi pi | Yes Refl = Yes CmpRefl
+  compat3 pi rh | No ne with (decEq rh Any)
+    compat3 pi Any | No ne | Yes Refl = Yes CmpAny
+    compat3 pi rh  | No ne | No  na   = No $ \case
+      CmpRefl => ne Refl
+      CmpAny  => na Refl
+
+
+public export
+data IsSubj3 : Three -> Type where
+  SZero : IsSubj3 Zero
+  SOne  : IsSubj3 One
+
+public export
+isSubj3 : (pi : Three) -> Dec (IsSubj3 pi)
+isSubj3 Zero = Yes SZero
+isSubj3 One  = Yes SOne
+isSubj3 Any  = No $ \case _ impossible
+
+
+public export
+data IsGlobal3 : Three -> Type where
+  GZero : IsGlobal3 Zero
+  GAny  : IsGlobal3 Any
+
+isGlobal3 : (pi : Three) -> Dec (IsGlobal3 pi)
+isGlobal3 Zero = Yes GZero
+isGlobal3 One  = No $ \case _ impossible
+isGlobal3 Any  = Yes GAny
+
+
+public export
+IsQty Three where
+  zero = Zero
+  one  = One
+
+  (+) = plus
+  (*) = times
+
+  IsZero     = Equal Zero
+  isZero     = decEq Zero
+  zeroIsZero = Refl
+
+  IsOne    = Equal One
+  isOne    = decEq One
+  oneIsOne = Refl
+
+  Compat = Compat3
+  compat = compat3
+
+  IsSubj     = IsSubj3
+  isSubj     = isSubj3
+  zeroIsSubj = SZero
+  oneIsSubj  = SOne
+
+  IsGlobal     = IsGlobal3
+  isGlobal     = isGlobal3
+  zeroIsGlobal = GZero
+
+
+export Uninhabited (IsGlobal3 One) where uninhabited _ impossible
+
+export Uninhabited (IsSubj3 Any) where uninhabited _ impossible
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index f891a30..a9aa9ac 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -26,63 +26,67 @@ infixl 8 :#
 infixl 9 :@
 mutual
   public export
-  TSubst : Nat -> Nat -> Nat -> Type
-  TSubst d = Subst (\n => Elim d n)
+  TSubst : Type -> Nat -> Nat -> Nat -> Type
+  TSubst q d = Subst (\n => Elim q d n)
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
-  data Term : (d, n : Nat) -> Type where
+  data Term : (q : Type) -> (d, n : Nat) -> Type where
     ||| type of types
-    TYPE : (l : Universe) -> Term d n
+    TYPE : (l : Universe) -> Term q d n
 
     ||| function type
-    Pi  : (qty : Qty) -> (x : Name) ->
-          (arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
+    Pi  : (qty : q) -> (x : Name) ->
+          (arg : Term q d n) -> (res : ScopeTerm q d n) -> Term q d n
     ||| function term
-    Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
+    Lam : (x : Name) -> (body : ScopeTerm q d n) -> Term q d n
 
     ||| elimination
-    E : (e : Elim d n) -> Term d n
+    E : (e : Elim q d n) -> Term q d n
 
     ||| term closure/suspended substitution
-    CloT  : (tm : Term d from)  -> (th : Lazy (TSubst d from to)) -> Term d to
+    CloT  : (tm : Term q d from) -> (th : Lazy (TSubst q d from to)) ->
+            Term q d to
     ||| dimension closure/suspended substitution
-    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
+    DCloT : (tm : Term q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
+            Term q dto n
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
-  data Elim : (d, n : Nat) -> Type where
+  data Elim : (q : Type) -> (d, n : Nat) -> Type where
     ||| free variable
-    F : (x : Name) -> Elim d n
+    F : (x : Name) -> Elim q d n
     ||| bound variable
-    B : (i : Var n) -> Elim d n
+    B : (i : Var n) -> Elim q d n
 
     ||| term application
-    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
+    (:@) : (fun : Elim q d n) -> (arg : Term q d n) -> Elim q d n
 
     ||| type-annotated term
-    (:#) : (tm, ty : Term d n) -> Elim d n
+    (:#) : (tm, ty : Term q d n) -> Elim q d n
 
     ||| term closure/suspended substitution
-    CloE  : (el : Elim d from)  -> (th : Lazy (TSubst d from to)) -> Elim d to
+    CloE  : (el : Elim q d from) -> (th : Lazy (TSubst q d from to)) ->
+            Elim q d to
     ||| dimension closure/suspended substitution
-    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
+    DCloE : (el : Elim q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
+            Elim q dto n
 
   ||| a scope with one more bound variable
   public export
-  data ScopeTerm : (d, n : Nat) -> Type where
+  data ScopeTerm : (q : Type) -> (d, n : Nat) -> Type where
     ||| variable is used
-    TUsed : (body : Term d (S n)) -> ScopeTerm d n
+    TUsed : (body : Term q d (S n)) -> ScopeTerm q d n
     ||| variable is unused
-    TUnused : (body : Term d n) -> ScopeTerm d n
+    TUnused : (body : Term q d n) -> ScopeTerm q d n
 
   ||| a scope with one more bound dimension variable
   public export
-  data DScopeTerm : (d, n : Nat) -> Type where
+  data DScopeTerm : (q : Type) -> (d, n : Nat) -> Type where
     ||| variable is used
-    DUsed : (body : Term (S d) n) -> DScopeTerm d n
+    DUsed : (body : Term q (S d) n) -> DScopeTerm q d n
     ||| variable is unused
-    DUnused : (body : Term d n) -> DScopeTerm d n
+    DUnused : (body : Term q d n) -> DScopeTerm q d n
 
 %name Term s, t, r
 %name Elim e, f
@@ -90,21 +94,21 @@ mutual
 %name DScopeTerm body
 
 public export %inline
-Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
+Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n
 Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
 
 ||| same as `F` but as a term
 public export %inline
-FT : Name -> Term d n
+FT : Name -> Term q d n
 FT = E . F
 
 ||| abbreviation for a bound variable like `BV 4` instead of
 ||| `B (VS (VS (VS (VS VZ))))`
 public export %inline
-BV : (i : Nat) -> (0 _ : LT i n) => Elim d n
+BV : (i : Nat) -> (0 _ : LT i n) => Elim q d n
 BV i = B $ V i
 
 ||| same as `BV` but as a term
 public export %inline
-BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
+BVT : (i : Nat) -> (0 _ : LT i n) => Term q d n
 BVT i = E $ BV i
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index ea5457e..27a0b00 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -28,7 +28,7 @@ colonD = hl Syntax ":"
 
 mutual
   export covering
-  PrettyHL (Term d n) where
+  PrettyHL q => PrettyHL (Term q d n) where
     prettyM (TYPE l) =
       parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
     prettyM (Pi qty x s t) =
@@ -49,7 +49,7 @@ mutual
         [|withPrec SApp (prettyM s) </> prettyDSubst th|]
 
   export covering
-  PrettyHL (Elim d n) where
+  PrettyHL q => PrettyHL (Elim q d n) where
     prettyM (F x) =
       hl' Free <$> prettyM x
     prettyM (B i) =
@@ -70,15 +70,17 @@ mutual
         [|withPrec SApp (prettyM e) </> prettyDSubst th|]
 
   export covering
-  PrettyHL (ScopeTerm d n) where
+  PrettyHL q => PrettyHL (ScopeTerm q d n) where
     prettyM body = prettyM $ fromScopeTerm body
 
   export covering
-  prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
+  prettyTSubst : Pretty.HasEnv m => PrettyHL q =>
+                 TSubst q d from to -> m (Doc HL)
   prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
 
   export covering
-  prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
+  prettyBinder : Pretty.HasEnv m => PrettyHL q =>
+                 List q -> Name -> Term q d n -> m (Doc HL)
   prettyBinder pis x a =
     pure $ parens $ hang 2 $
       hsep [hl TVar !(prettyM x),
diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Syntax/Term/Reduce.idr
index 8be3336..5bce4dd 100644
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@@ -7,43 +7,57 @@ import Quox.Syntax.Term.Subst
 
 
 mutual
-  ||| 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
-  topCloT : Term d n -> Bool
-  topCloT (CloT  _ _) = True
-  topCloT (DCloT _ _) = True
-  topCloT (E e)       = topCloE e
-  topCloT _           = False
+  public export
+  data NotCloT : Term {} -> Type where
+    NCTYPE : NotCloT $ TYPE _
+    NCPi   : NotCloT $ Pi {}
+    NCLam  : NotCloT $ Lam {}
+    NCE    : NotCloE e -> NotCloT $ E e
 
-  ||| true if an elimination has a closure or dimension closure at the top level
-  public export %inline
-  topCloE : Elim d n -> Bool
-  topCloE (CloE  _ _) = True
-  topCloE (DCloE _ _) = True
-  topCloE _           = False
+  public export
+  data NotCloE : Elim {} -> Type where
+    NCF   : NotCloE $ F _
+    NCB   : NotCloE $ B _
+    NCApp : NotCloE $ _ :@ _
+    NCAnn : NotCloE $ _ :# _
 
+mutual
+  export
+  notCloT : (t : Term {}) -> Dec (NotCloT t)
+  notCloT (TYPE _) = Yes NCTYPE
+  notCloT (Pi {})  = Yes NCPi
+  notCloT (Lam {}) = Yes NCLam
+  notCloT (E e) with (notCloE e)
+    notCloT (E e) | Yes nc = Yes $ NCE nc
+    notCloT (E e) | No  c  = No  $ \case NCE nc => c nc
+  notCloT (CloT {})  = No $ \case _ impossible
+  notCloT (DCloT {}) = No $ \case _ impossible
 
-public export IsNotCloT : Term d n -> Type
-IsNotCloT = So . not . topCloT
+  export
+  notCloE : (e : Elim {}) -> Dec (NotCloE e)
+  notCloE (F _)      = Yes NCF
+  notCloE (B _)      = Yes NCB
+  notCloE (_ :@ _)   = Yes NCApp
+  notCloE (_ :# _)   = Yes NCAnn
+  notCloE (CloE  {}) = No $ \case _ impossible
+  notCloE (DCloE {}) = No $ \case _ impossible
 
 ||| a term which is not a top level closure
-public export NotCloTerm : Nat -> Nat -> Type
-NotCloTerm d n = Subset (Term d n) IsNotCloT
-
-public export IsNotCloE : Elim d n -> Type
-IsNotCloE = So . not . topCloE
+public export
+NotCloTerm : Type -> Nat -> Nat -> Type
+NotCloTerm q d n = Subset (Term q d n) NotCloT
 
 ||| an elimination which is not a top level closure
-public export NotCloElim : Nat -> Nat -> Type
-NotCloElim d n = Subset (Elim d n) IsNotCloE
+public export
+NotCloElim : Type -> Nat -> Nat -> Type
+NotCloElim q d n = Subset (Elim q d n) NotCloE
 
 public export %inline
-ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
+ncloT : (t : Term q d n) -> (0 _ : NotCloT t) => NotCloTerm q d n
 ncloT t @{p} = Element t p
 
 public export %inline
-ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
+ncloE : (e : Elim q d n) -> (0 _ : NotCloE e) => NotCloElim q d n
 ncloE e @{p} = Element e p
 
 
@@ -52,18 +66,18 @@ mutual
   ||| if the input term has any top-level closures, push them under one layer of
   ||| syntax
   export %inline
-  pushSubstsT : Term d n -> NotCloTerm d n
+  pushSubstsT : Term q d n -> NotCloTerm q d n
   pushSubstsT s = pushSubstsTWith id id s
 
   ||| if the input elimination has any top-level closures, push them under one
   ||| layer of syntax
   export %inline
-  pushSubstsE : Elim d n -> NotCloElim d n
+  pushSubstsE : Elim q d n -> NotCloElim q d n
   pushSubstsE e = pushSubstsEWith id id e
 
   export
-  pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
-                    Term dfrom from -> NotCloTerm dto to
+  pushSubstsTWith : DSubst dfrom dto -> TSubst q dto from to ->
+                    Term q dfrom from -> NotCloTerm q dto to
   pushSubstsTWith th ph (TYPE l) =
     ncloT $ TYPE l
   pushSubstsTWith th ph (Pi qty x a body) =
@@ -78,15 +92,15 @@ mutual
     pushSubstsTWith (ps . th) ph s
 
   export
-  pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
-                    Elim dfrom from -> NotCloElim dto to
+  pushSubstsEWith : DSubst dfrom dto -> TSubst q dto from to ->
+                    Elim q dfrom from -> NotCloElim q dto to
   pushSubstsEWith th ph (F x) =
     ncloE $ F x
   pushSubstsEWith th ph (B i) =
     let res = ph !! i in
-    case choose $ topCloE res of
-         Left  _ => assert_total pushSubstsE res
-         Right _ => ncloE res
+    case notCloE res of
+         Yes _ => ncloE res
+         No  _ => assert_total pushSubstsE res
   pushSubstsEWith th ph (f :@ s) =
     ncloE $ subs f th ph :@ subs s th ph
   pushSubstsEWith th ph (s :# a) =
@@ -97,22 +111,22 @@ mutual
     pushSubstsEWith (ps . th) ph e
 
 
-parameters (th : DSubst dfrom dto) (ph : TSubst dto from to)
+parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to)
   public export %inline
-  pushSubstsTWith' : Term dfrom from -> Term dto to
+  pushSubstsTWith' : Term q dfrom from -> Term q dto to
   pushSubstsTWith' s = (pushSubstsTWith th ph s).fst
 
   public export %inline
-  pushSubstsEWith' : Elim dfrom from -> Elim dto to
+  pushSubstsEWith' : Elim q dfrom from -> Elim q dto to
   pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
 
 
 public export %inline
-pushSubstsT' : Term d n -> Term d n
+pushSubstsT' : Term q d n -> Term q d n
 pushSubstsT' s = (pushSubstsT s).fst
 
 public export %inline
-pushSubstsE' : Elim d n -> Elim d n
+pushSubstsE' : Elim q d n -> Elim q d n
 pushSubstsE' e = (pushSubstsE e).fst
 
 
@@ -159,41 +173,41 @@ pushSubstsE' e = (pushSubstsE e).fst
 
 
 public export %inline
-weakT : Term d n -> Term d (S n)
+weakT : Term q d n -> Term q d (S n)
 weakT t = t //. shift 1
 
 public export %inline
-weakE : Elim d n -> Elim d (S n)
+weakE : Elim q d n -> Elim q d (S n)
 weakE t = t //. shift 1
 
 
 mutual
   public export
-  data IsRedexT : Term d n -> Type where
+  data IsRedexT : Term q d n -> Type where
     IsUpsilonT : IsRedexT $ E (_ :# _)
     IsCloT     : IsRedexT $ CloT {}
     IsDCloT    : IsRedexT $ DCloT {}
     IsERedex   : IsRedexE e -> IsRedexT $ E e
 
   public export %inline
-  NotRedexT : Term d n -> Type
+  NotRedexT : Term q d n -> Type
   NotRedexT = Not . IsRedexT
 
   public export
-  data IsRedexE : Elim d n -> Type where
+  data IsRedexE : Elim q d n -> Type where
     IsUpsilonE : IsRedexE $ E _ :# _
     IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
     IsCloE     : IsRedexE $ CloE {}
     IsDCloE    : IsRedexE $ DCloE {}
 
   public export %inline
-  NotRedexE : Elim d n -> Type
+  NotRedexE : Elim q d n -> Type
   NotRedexE = Not . IsRedexE
 
 
 mutual
   export %inline
-  isRedexT : (t : Term d n) -> Dec (IsRedexT t)
+  isRedexT : (t : Term {}) -> Dec (IsRedexT t)
   isRedexT (E (tm :# ty)) = Yes IsUpsilonT
   isRedexT (CloT {})      = Yes IsCloT
   isRedexT (DCloT {})     = Yes IsDCloT
@@ -201,7 +215,7 @@ mutual
   isRedexT (E (DCloE {})) = Yes $ IsERedex IsDCloE
   isRedexT (E e@(_ :@ _)) with (isRedexE e)
     _ | Yes yes = Yes $ IsERedex yes
-    _ | No  no  = No \case IsERedex p => no p
+    _ | No  no  = No  $ \case IsERedex p => no p
   isRedexT (TYPE {}) = No $ \case _ impossible
   isRedexT (Pi   {}) = No $ \case _ impossible
   isRedexT (Lam  {}) = No $ \case _ impossible
@@ -209,7 +223,7 @@ mutual
   isRedexT (E (B _)) = No $ \case IsERedex _ impossible
 
   export %inline
-  isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
+  isRedexE : (e : Elim {}) -> Dec (IsRedexE e)
   isRedexE (E _ :# _)                    = Yes IsUpsilonE
   isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
   isRedexE (CloE {})                     = Yes IsCloE
@@ -239,39 +253,38 @@ mutual
 
 
 public export %inline
-RedexTerm : Nat -> Nat -> Type
-RedexTerm d n = Subset (Term d n) IsRedexT
+RedexTerm : Type -> Nat -> Nat -> Type
+RedexTerm q d n = Subset (Term q d n) IsRedexT
 
 public export %inline
-NonRedexTerm : Nat -> Nat -> Type
-NonRedexTerm d n = Subset (Term d n) NotRedexT
-
+NonRedexTerm : Type -> Nat -> Nat -> Type
+NonRedexTerm q d n = Subset (Term q d n) NotRedexT
 
 public export %inline
-RedexElim : Nat -> Nat -> Type
-RedexElim d n = Subset (Elim d n) IsRedexE
+RedexElim : Type -> Nat -> Nat -> Type
+RedexElim q d n = Subset (Elim q d n) IsRedexE
 
 public export %inline
-NonRedexElim : Nat -> Nat -> Type
-NonRedexElim d n = Subset (Elim d n) NotRedexE
+NonRedexElim : Type -> Nat -> Nat -> Type
+NonRedexElim q d n = Subset (Elim q d n) NotRedexE
 
 
 ||| substitute a term with annotation for the bound variable of a `ScopeTerm`
 export %inline
-substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
+substScope : (arg, argTy : Term q d n) -> (body : ScopeTerm q d n) -> Term q d n
 substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
 substScope arg argTy (TUnused body) = body
 
 mutual
   export %inline
-  stepT' : (s : Term d n) -> IsRedexT s -> Term d n
+  stepT' : (s : Term q d n) -> IsRedexT s -> Term q d n
   stepT' (E (s :# _)) IsUpsilonT   = s
   stepT' (CloT  s th) IsCloT       = pushSubstsTWith' id th s
   stepT' (DCloT s th) IsDCloT      = pushSubstsTWith' th id s
   stepT' (E e)        (IsERedex p) = E $ stepE' e p
 
   export %inline
-  stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
+  stepE' : (e : Elim q d n) -> IsRedexE e -> Elim q d n
   stepE' (E e :# _) IsUpsilonE = e
   stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
     substScope s arg body :# substScope s arg res
@@ -279,21 +292,21 @@ mutual
   stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
 
 export %inline
-stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
+stepT : (s : Term q d n) -> Either (NotRedexT s) (Term q d n)
 stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
 
 export %inline
-stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
+stepE : (e : Elim q d n) -> Either (NotRedexE e) (Elim q d n)
 stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
 
 export covering
-whnfT : Term d n -> NonRedexTerm d n
+whnfT : Term q d n -> NonRedexTerm q d n
 whnfT s = case stepT s of
                Right s'   => whnfT s'
                Left  done => Element s done
 
 export covering
-whnfE : Elim d n -> NonRedexElim d n
+whnfE : Elim q d n -> NonRedexElim q d n
 whnfE e = case stepE e of
                Right e'   => whnfE e'
                Left  done => Element e done
diff --git a/lib/Quox/Syntax/Term/Split.idr b/lib/Quox/Syntax/Term/Split.idr
index 2977ed1..297b893 100644
--- a/lib/Quox/Syntax/Term/Split.idr
+++ b/lib/Quox/Syntax/Term/Split.idr
@@ -9,74 +9,100 @@ import Data.Vect
 %default total
 
 
-public export %inline
-isLam : Term d n -> Bool
-isLam (Lam {}) = True
-isLam _        = False
-
 public export
-NotLam : Term d n -> Type
-NotLam = So . not . isLam
-
+data IsLam : Term {} -> Type where
+  ItIsLam : IsLam $ Lam x body
 
 public export %inline
-isApp : Elim d n -> Bool
-isApp ((:@) {}) = True
-isApp _         = False
+isLam : (s : Term {}) -> Dec (IsLam s)
+isLam (TYPE _)   = No $ \case _ impossible
+isLam (Pi {})    = No $ \case _ impossible
+isLam (Lam {})   = Yes ItIsLam
+isLam (E _)      = No $ \case _ impossible
+isLam (CloT {})  = No $ \case _ impossible
+isLam (DCloT {}) = No $ \case _ impossible
+
+public export %inline
+NotLam : Term {} -> Type
+NotLam = Not . IsLam
+
 
 public export
-NotApp : Elim d n -> Type
-NotApp = So . not . isApp
+data IsApp : Elim {} -> Type where
+  ItIsApp : IsApp $ f :@ s
+
+public export %inline
+isApp : (e : Elim {}) -> Dec (IsApp e)
+isApp (F _)      = No $ \case _ impossible
+isApp (B _)      = No $ \case _ impossible
+isApp (_ :@ _)   = Yes ItIsApp
+isApp (_ :# _)   = No $ \case _ impossible
+isApp (CloE {})  = No $ \case _ impossible
+isApp (DCloE {}) = No $ \case _ impossible
+
+public export
+NotApp : Elim {} -> Type
+NotApp = Not . IsApp
 
 
 infixl 9 :@@
 ||| apply multiple arguments at once
 public export %inline
-(:@@) : Elim d n -> List (Term d n) -> Elim d n
+(:@@) : Elim q d n -> List (Term q d n) -> Elim q d n
 f :@@ ss = foldl (:@) f ss
 
 public export
-record GetArgs (d, n : Nat) where
+record GetArgs q d n where
   constructor GotArgs
-  fun      : Elim d n
-  args     : List (Term d n)
+  fun      : Elim q d n
+  args     : List (Term q d n)
   0 notApp : NotApp fun
 
 export
-getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
-getArgs' fun args with (choose $ isApp fun)
-  getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
-  _ | Right no = GotArgs {fun, args, notApp = no}
+getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
+getArgs' fun args with (isApp fun)
+  getArgs' (f :@ a) args | Yes yes = getArgs' f (a :: args)
+  getArgs' fun args      | No  no  = GotArgs {fun, args, notApp = no}
 
 ||| splits an application into its head and arguments. if it's not an
 ||| application then the list is just empty
 export %inline
-getArgs : Elim d n -> GetArgs d n
+getArgs : Elim q d n -> GetArgs q d n
 getArgs e = getArgs' e []
 
 
 infixr 1 :\\
 public export
-(:\\) : Vect m Name -> Term d (m + n) -> Term d n
-[]      :\\ t = t
-x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
-                Lam x $ TUsed $ xs :\\ t'
+absN : Vect m Name -> Term q d (m + n) -> Term q d n
+absN {m = 0}   []        s = s
+absN {m = S m} (x :: xs) s = Lam x $ TUsed $ absN xs $
+                             rewrite sym $ plusSuccRightSucc m n in s
+
+public export %inline
+(:\\) : Vect m Name -> Term q d (m + n) -> Term q d n
+(:\\) = absN
+
 
 public export
-record GetLams (d, n : Nat) where
+record GetLams q d n where
   constructor GotLams
   names    : Vect lams Name
-  body     : Term d rest
+  body     : Term q d rest
   0 eq     : lams + n = rest
   0 notLam : NotLam body
 
-public export
-getLams : Term d n -> GetLams d n
-getLams s with (choose $ isLam s)
-  getLams s@(Lam x body) | Left yes =
-    let inner = getLams $ assert_smaller s $ fromScopeTerm body in
-    GotLams {names  = x :: inner.names,
-             body   = inner.body,
-             eq     = plusSuccRightSucc {} `trans` inner.eq,
-             notLam = inner.notLam}
-  _ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}
+export
+getLams' : forall lams, rest.
+           Vect lams Name -> Term q d rest -> lams + n = rest -> GetLams q d n
+getLams' xs s eq with (isLam s)
+  getLams' xs (Lam x sbody) Refl | Yes ItIsLam =
+    let 0 s  = Lam x sbody
+        body = assert_smaller s $ fromScopeTerm sbody
+    in
+    getLams' (x :: xs) body Refl
+  getLams' xs s eq | No no =
+    GotLams xs s eq no
+
+export
+getLams : Term q d n -> GetLams q d n
+getLams s = getLams' [] s Refl
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 8e48065..8165edd 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -5,8 +5,8 @@ import Quox.Syntax.Term.Base
 %default total
 
 
-export FromVar (Elim d) where fromVar = B
-export FromVar (Term d) where fromVar = E . fromVar
+export FromVar (Elim q d) where fromVar = B
+export FromVar (Term q d) where fromVar = E . fromVar
 
 ||| does the minimal reasonable work:
 ||| - deletes the closure around a free name since it doesn't do anything
@@ -15,7 +15,7 @@ export FromVar (Term d) where fromVar = E . fromVar
 ||| - immediately looks up a bound variable
 ||| - otherwise, wraps in a new closure
 export
-CanSubst (Elim d) (Elim d) where
+CanSubst (Elim q d) (Elim q d) where
   F x       // _  = F x
   B i       // th = th !! i
   CloE e ph // th = assert_total CloE e $ ph . th
@@ -30,7 +30,7 @@ CanSubst (Elim d) (Elim d) where
 ||| - goes inside `E` in case it is a simple variable or something
 ||| - otherwise, wraps in a new closure
 export
-CanSubst (Elim d) (Term d) where
+CanSubst (Elim q d) (Term q d) where
   TYPE l    // _  = TYPE l
   E e       // th = E $ e // th
   CloT s ph // th = CloT s $ ph . th
@@ -39,13 +39,13 @@ CanSubst (Elim d) (Term d) where
                          th       => CloT s th
 
 export
-CanSubst (Elim d) (ScopeTerm d) where
+CanSubst (Elim q d) (ScopeTerm q d) where
   TUsed   body // th = TUsed   $ body // push th
   TUnused body // th = TUnused $ body // 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 CanSubst Var (ScopeTerm d) where s // th = s // map (B {d}) th
+export CanSubst Var (Term      q d) where s // th = s // map (B {q, d}) th
+export CanSubst Var (Elim      q d) where e // th = e // map (B {q, d}) th
+export CanSubst Var (ScopeTerm q d) where s // th = s // map (B {q, d}) th
 
 
 infixl 8 //., ///
@@ -53,13 +53,13 @@ mutual
   namespace Term
     ||| applies a term substitution with a less ambiguous type
     export
-    (//.) : Term d from -> TSubst d from to -> Term d to
+    (//.) : Term q d from -> TSubst q d from to -> Term q d to
     t //. th = t // th
 
     ||| applies a dimension substitution with the same behaviour as `(//)`
     ||| above
     export
-    (///) : Term dfrom n -> DSubst dfrom dto -> Term dto n
+    (///) : Term q dfrom n -> DSubst dfrom dto -> Term q dto n
     TYPE l     /// _        = TYPE l
     E e        /// th       = E $ e /// th
     DCloT s ph /// th       = DCloT s $ ph . th
@@ -68,20 +68,20 @@ mutual
 
     ||| applies a term and dimension substitution
     public export %inline
-    subs : Term dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           Term dto to
+    subs : Term q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
+           Term q dto to
     subs s th ph = s /// th // ph
 
   namespace Elim
     ||| applies a term substitution with a less ambiguous type
     export
-    (//.) : Elim d from -> TSubst d from to -> Elim d to
+    (//.) : Elim q d from -> TSubst q d from to -> Elim q d to
     e //. th = e // th
 
     ||| applies a dimension substitution with the same behaviour as `(//)`
     ||| above
     export
-    (///) : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
+    (///) : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
     F x        /// _        = F x
     B i        /// _        = B i
     DCloE e ph /// th       = DCloE e $ ph . th
@@ -90,46 +90,46 @@ mutual
 
     ||| applies a term and dimension substitution
     public export %inline
-    subs : Elim dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           Elim dto to
+    subs : Elim q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
+           Elim q dto to
     subs e th ph = e /// th // ph
 
   namespace ScopeTerm
     ||| applies a term substitution with a less ambiguous type
     export
-    (//.) : ScopeTerm d from -> TSubst d from to -> ScopeTerm d to
+    (//.) : ScopeTerm q d from -> TSubst q d from to -> ScopeTerm q d to
     body //. th = body // th
 
     ||| applies a dimension substitution with the same behaviour as `(//)`
     ||| above
     export
-    (///) : ScopeTerm dfrom n -> DSubst dfrom dto -> ScopeTerm dto n
+    (///) : ScopeTerm q dfrom n -> DSubst dfrom dto -> ScopeTerm q dto n
     TUsed   body /// th = TUsed   $ body /// th
     TUnused body /// th = TUnused $ body /// th
 
     ||| applies a term and dimension substitution
     public export %inline
-    subs : ScopeTerm dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
-           ScopeTerm dto to
+    subs : ScopeTerm q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
+           ScopeTerm q dto to
     subs body th ph = body /// th // ph
 
-export CanShift (Term      d) where s // by = s //. Shift by
-export CanShift (Elim      d) where e // by = e //. Shift by
-export CanShift (ScopeTerm d) where s // by = s //. Shift by
+export CanShift (Term      q d) where s // by = s //. Shift by
+export CanShift (Elim      q d) where e // by = e //. Shift by
+export CanShift (ScopeTerm q d) where s // by = s //. Shift by
 
 
 export %inline
-comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
-        TSubst dto from to
+comp' : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
+        TSubst q dto from to
 comp' th ps ph = map (/// th) ps . ph
 
 
 export
-fromDScopeTerm : DScopeTerm d n -> Term (S d) n
+fromDScopeTerm : DScopeTerm q d n -> Term q (S d) n
 fromDScopeTerm (DUsed   body) = body
 fromDScopeTerm (DUnused body) = body /// shift 1
 
 export
-fromScopeTerm : ScopeTerm d n -> Term d (S n)
+fromScopeTerm : ScopeTerm q d n -> Term q d (S n)
 fromScopeTerm (TUsed   body) = body
 fromScopeTerm (TUnused body) = body //. shift 1
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 5156040..cd57c76 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -4,48 +4,50 @@ import public Quox.Syntax
 import public Quox.Typing
 import public Quox.Equal
 import public Control.Monad.Either
+import Decidable.Decidable
 
 %default total
 
 
 private covering %inline
-expectTYPE : MonadError Error m => Term d n -> m Universe
+expectTYPE : HasErr q m => Term q d n -> m Universe
 expectTYPE s =
   case (whnfT s).fst of
        TYPE l => pure l
        _      => throwError $ ExpectedTYPE s
 
 private covering %inline
-expectPi : MonadError Error m => Term d n ->
-           m (Qty, Term d n, ScopeTerm d n)
+expectPi : HasErr q m => Term q d n ->
+           m (q, Term q d n, ScopeTerm q d n)
 expectPi ty =
   case (whnfT ty).fst of
        Pi qty _ arg res => pure (qty, arg, res)
        _                => throwError $ ExpectedPi ty
 
 private %inline
-expectEqualQ : MonadError Error m =>
-               (expect, actual : Qty) -> m ()
+expectEqualQ : HasErr q m => Eq q =>
+               (expect, actual : q) -> m ()
 expectEqualQ pi rh =
   unless (pi == rh) $ throwError $ ClashQ pi rh
 
 
 private %inline
-popQ : MonadError Error m => Qty -> QOutput (S n) -> m (QOutput n)
+popQ : HasErr q m => Eq q => q -> QOutput q (S n) -> m (QOutput q n)
 popQ pi (qctx :< rh) = expectEqualQ pi rh $> qctx
 
 
 private %inline
-tail : TyContext d (S n) -> TyContext d n
+tail : TyContext q d (S n) -> TyContext q d n
 tail = {tctx $= tail, qctx $= tail}
 
 
 private %inline
-weakI : InferResult d n -> InferResult d (S n)
+weakI : IsQty q => InferResult q d n -> InferResult q d (S n)
 weakI = {type $= weakT, qout $= (:< zero)}
 
 private
-lookupBound : {n : Nat} -> Qty -> Var n -> TyContext d n -> InferResult d n
+lookupBound : IsQty q =>
+              {n : Nat} -> q -> Var n -> TyContext q d n -> InferResult q d n
 lookupBound pi VZ (MkTyContext {tctx = _ :< ty, _}) =
   InfRes {type = weakT ty, qout = zero :< pi}
 lookupBound pi (VS i) ctx =
@@ -53,18 +55,22 @@ lookupBound pi (VS i) ctx =
 
 
 private %inline
-subjMult : Qty -> Qty -> Subset Qty IsSubj
-subjMult sg qty =
-  if sg == Zero || qty == Zero
-     then Element Zero %search
-     else Element One  %search
+subjMult : IsQty q => (sg : SQty q) -> q -> SQty q
+subjMult (Element sg subj) qty =
+  if isYes (isZero sg) || isYes (isZero qty)
+     then Element zero zeroIsSubj
+     else Element sg   subj
 
 
 public export
-CanTC : (Type -> Type) -> Type
-CanTC m = (MonadError Error m, MonadReader Definitions m)
+0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m)
 
-parameters {auto _ : CanTC m}
+public export
+0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type
+CanTC q = CanTC' q IsGlobal
+
+parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  mutual
   -- [todo] it seems like the options here for dealing with substitutions are
   -- to either push them or parametrise the whole typechecker over ambient
@@ -73,76 +79,78 @@ parameters {auto _ : CanTC m}
 
   export covering %inline
   check : {d, n : Nat} ->
-          (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
-          (subj : Term d n) -> (ty : Term d n) ->
-          m (CheckResult n)
+          (ctx : TyContext q d n) -> (sg : SQty q) ->
+          (subj : Term q d n) -> (ty : Term q d n) ->
+          m (CheckResult q n)
   check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
 
   export covering %inline
   infer : {d, n : Nat} ->
-          (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
-          (subj : Elim d n) ->
-          m (InferResult d n)
+          (ctx : TyContext q d n) -> (sg : SQty q) ->
+          (subj : Elim q d n) ->
+          m (InferResult q d n)
   infer ctx sg subj = infer' ctx sg (pushSubstsE subj)
 
 
   export covering
   check' : {d, n : Nat} ->
-           (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
-           (subj : NotCloTerm d n) -> (ty : Term d n) ->
-           m (CheckResult n)
+           (ctx : TyContext q d n) -> (sg : SQty q) ->
+           (subj : NotCloTerm q d n) -> (ty : Term q d n) ->
+           m (CheckResult q n)
 
   check' ctx sg (Element (TYPE l) _) ty = do
     l' <- expectTYPE ty
-    expectEqualQ zero sg
+    expectEqualQ zero sg.fst
     unless (l < l') $ throwError $ BadUniverse l l'
     pure zero
 
   check' ctx sg (Element (Pi qty x arg res) _) ty = do
     l <- expectTYPE ty
-    expectEqualQ zero sg
-    ignore $ check ctx zero arg (TYPE l)
+    expectEqualQ zero sg.fst
+    ignore $ check ctx szero arg (TYPE l)
     case res of
-         TUsed   res => ignore $ check (extendTy arg zero ctx) zero res (TYPE l)
-         TUnused res => ignore $ check ctx                     zero res (TYPE l)
+         TUsed   res =>
+           ignore $ check (extendTy arg zero ctx) szero res (TYPE l)
+         TUnused res =>
+           ignore $ check ctx szero res (TYPE l)
     pure zero
 
   check' ctx sg (Element (Lam x body) _) ty = do
     (qty, arg, res) <- expectPi ty
     -- [todo] do this properly?
     let body = fromScopeTerm body; res = fromScopeTerm res
-    qout <- check (extendTy arg (sg * qty) ctx) sg body res
+    qout <- check (extendTy arg (sg.fst * qty) ctx) sg body res
     popQ qty qout
 
   check' ctx sg (Element (E e) _) ty = do
     infres <- infer ctx sg e
-    ignore $ check ctx zero ty (TYPE UAny)
+    ignore $ check ctx szero ty (TYPE UAny)
     subT infres.type ty
     pure infres.qout
 
   export covering
   infer' : {d, n : Nat} ->
-           (ctx : TyContext d n) -> (sg : Qty) -> (0 _ : IsSubj sg) =>
-           (subj : NotCloElim d n) ->
-           m (InferResult d n)
+           (ctx : TyContext q d n) -> (sg : SQty q) ->
+           (subj : NotCloElim q d n) ->
+           m (InferResult q d n)
 
   infer' ctx sg (Element (F x) _) = do
     Just g <- asks $ lookup x  | Nothing => throwError $ NotInScope x
-    when (isZero g) $ expectEqualQ sg Zero
+    when (isZero g) $ expectEqualQ sg.fst zero
     pure $ InfRes {type = g.type.get, qout = zero}
 
   infer' ctx sg (Element (B i) _) =
-    pure $ lookupBound sg i ctx
+    pure $ lookupBound sg.fst i ctx
 
   infer' ctx sg (Element (fun :@ arg) _) = do
     funres <- infer ctx sg fun
     (qty, argty, res) <- expectPi funres.type
-    let Element sg' _ = subjMult sg qty
+    let sg' = subjMult sg qty
     argout <- check ctx sg' arg argty
     pure $ InfRes {type = fromScopeTerm res //. ((arg :# argty) ::: id),
                    qout = funres.qout + argout}
 
   infer' ctx sg (Element (tm :# ty) _) = do
-    ignore $ check ctx zero ty (TYPE UAny)
+    ignore $ check ctx szero ty (TYPE UAny)
     qout <- check ctx sg tm ty
     pure $ InfRes {type = ty, qout}
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 6847325..899d815 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -6,6 +6,7 @@ import public Quox.Definition
 
 import Data.Nat
 import public Data.SortedMap
+import Control.Monad.Either
 import Control.Monad.Reader
 import Control.Monad.State
 import Generics.Derive
@@ -24,71 +25,72 @@ data DContext : Nat -> Type where
   DEq   : Dim d -> Dim d -> DContext d -> DContext d
 
 public export
-TContext : Nat -> Nat -> Type
-TContext d = Context (Term d)
+TContext : Type -> Nat -> Nat -> Type
+TContext q d = Context (Term q d)
 
 public export
-QContext : Nat -> Type
-QContext = Context' Qty
+QContext : Type -> Nat -> Type
+QContext = Context'
 
 public export
-QOutput : Nat -> Type
+QOutput : Type -> Nat -> Type
 QOutput = QContext
 
 
 public export
-record TyContext (d, n : Nat) where
+record TyContext q d n where
   constructor MkTyContext
   dctx : DContext d
-  tctx : TContext d n
-  qctx : QContext n
+  tctx : TContext q d n
+  qctx : QContext q n
 
 %name TyContext ctx
 
 
 namespace TContext
   export
-  pushD : TContext d n -> TContext (S d) n
+  pushD : TContext q d n -> TContext q (S d) n
   pushD tel = map (/// shift 1) tel
 
 
 namespace TyContext
   export
-  extendTy : Term d n -> Qty -> TyContext d n -> TyContext d (S n)
+  extendTy : Term q d n -> q -> TyContext q d n -> TyContext q d (S n)
   extendTy s rho = {tctx $= (:< s), qctx $= (:< rho)}
 
   export
-  extendDim : TyContext d n -> TyContext (S d) n
+  extendDim : TyContext q d n -> TyContext q (S d) n
   extendDim = {dctx $= DBind, tctx $= pushD}
 
   export
-  eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
+  eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
   eqDim p q = {dctx $= DEq p q}
 
 
 namespace QOutput
-  export
-  (+) : QOutput n -> QOutput n -> QOutput n
-  (+) = zipWith (+)
+  parameters {auto _ : IsQty q}
+    export
+    (+) : QOutput q n -> QOutput q n -> QOutput q n
+    (+) = zipWith (+)
 
-  export
-  (*) : Qty -> QOutput n -> QOutput n
-  (*) pi = map (pi *)
+    export
+    (*) : q -> QOutput q n -> QOutput q n
+    (*) pi = map (pi *)
 
-  export
-  zero : {n : Nat} -> QOutput n
-  zero = pure Zero
+    export
+    zero : {n : Nat} -> QOutput q n
+    zero = pure zero
 
 
 public export
-CheckResult : Nat -> Type
+CheckResult : Type -> Nat -> Type
 CheckResult = QOutput
 
 public export
-record InferResult d n where
+record InferResult q d n where
   constructor InfRes
-  type : Term d n
-  qout : QOutput n
+  type : Term q d n
+  qout : QOutput q n
 
 
 public export
@@ -97,12 +99,16 @@ data EqMode = Equal | Sub
 
 
 public export
-data Error
-= ExpectedTYPE (Term d n)
-| ExpectedPi   (Term d n)
+data Error q
+= ExpectedTYPE (Term q d n)
+| ExpectedPi   (Term q d n)
 | BadUniverse  Universe Universe
 
-| ClashT EqMode (Term d n) (Term d n)
-| ClashU EqMode Universe Universe
-| ClashQ        Qty      Qty
+| ClashT EqMode (Term q d n) (Term q d n)
+| ClashU EqMode Universe     Universe
+| ClashQ        q            q
 | NotInScope    Name
+
+public export
+0 HasErr : Type -> (Type -> Type) -> Type
+HasErr q = MonadError (Error q)
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index eda73bb..ddf4d06 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -16,6 +16,7 @@ modules =
   Quox.Syntax.Dim,
   Quox.Syntax.DimEq,
   Quox.Syntax.Qty,
+  Quox.Syntax.Qty.Three,
   Quox.Syntax.Shift,
   Quox.Syntax.Subst,
   Quox.Syntax.Term,
diff --git a/tests/TermImpls.idr b/tests/TermImpls.idr
index b14aaac..ca3caf6 100644
--- a/tests/TermImpls.idr
+++ b/tests/TermImpls.idr
@@ -1,7 +1,7 @@
 module TermImpls
 
 import Quox.Syntax
-import Quox.Pretty
+import public Quox.Pretty
 
 
 private
@@ -22,7 +22,7 @@ eqSubst (_ ::: _)  (Shift _)  = Nothing
 
 mutual
   export covering
-  Eq (Term d n) where
+  Eq q => Eq (Term q d n) where
     TYPE k == TYPE l = k == l
     TYPE _ == _ = False
 
@@ -49,7 +49,7 @@ mutual
     DCloT {} == _ = False
 
   export covering
-  Eq (Elim d n) where
+  Eq q => Eq (Elim q d n) where
     F x == F y = x == y
     F _ == _ = False
 
@@ -75,16 +75,16 @@ mutual
     DCloE {} == _ = False
 
   export covering
-  Eq (ScopeTerm d n) where
+  Eq q => Eq (ScopeTerm q d n) where
     TUsed   s == TUsed   t = s == t
     TUnused s == TUnused t = s == t
     TUsed   _ == TUnused _ = False
     TUnused _ == TUsed   _ = False
 
 export covering
-Show (Term d n) where
+PrettyHL q => Show (Term q d n) where
   showPrec d t = showParens (d /= Open) $ prettyStr True t
 
 export covering
-Show (Elim d n) where
+PrettyHL q => Show (Elim q d n) where
   showPrec d e = showParens (d /= Open) $ prettyStr True e
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 91dcde5..2f89322 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -2,10 +2,11 @@ module Tests.Equal
 
 import Quox.Equal as Lib
 import Quox.Pretty
+import Quox.Syntax.Qty.Three
 import TAP
 
 export
-ToInfo Error where
+ToInfo (Error Three) where
   toInfo (NotInScope x) =
     [("type", "NotInScope"),
      ("name", show x)]
@@ -35,10 +36,11 @@ ToInfo Error where
      ("right", prettyStr True rh)]
 
 
-M = ReaderT Definitions (Either Error)
+0 M : Type -> Type
+M = ReaderT (Definitions Three) (Either (Error Three))
 
 parameters (label : String) (act : Lazy (M ()))
-           {default empty globals : Definitions}
+           {default empty globals : Definitions Three}
   testEq : Test
   testEq = test label $ runReaderT globals act
 
@@ -46,19 +48,19 @@ parameters (label : String) (act : Lazy (M ()))
   testNeq = testThrows label (const True) $ runReaderT globals act
 
 
-subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+subT : {default 0 d, n : Nat} -> Term Three d n -> Term Three d n -> M ()
 subT = Lib.subT
 %hide Lib.subT
 
-equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+equalT : {default 0 d, n : Nat} -> Term Three d n -> Term Three d n -> M ()
 equalT = Lib.equalT
 %hide Lib.equalT
 
-subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+subE : {default 0 d, n : Nat} -> Elim Three d n -> Elim Three d n -> M ()
 subE = Lib.subE
 %hide Lib.subE
 
-equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+equalE : {default 0 d, n : Nat} -> Elim Three d n -> Elim Three d n -> M ()
 equalE = Lib.equalE
 %hide Lib.equalE
 
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index 9b4a2be..b1671c3 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -1,6 +1,7 @@
 module Tests.Reduce
 
 import Quox.Syntax as Lib
+import Quox.Syntax.Qty.Three
 import TermImpls
 import TAP
 
@@ -22,17 +23,18 @@ testNoStep step label e = test "\{label}  (no step)" $
        Right e' => with Prelude.(::) Left [("reduced", e')]
 
 
+
 parameters {default 0 d, n : Nat}
-  testWhnfT : String -> Term d n -> Term d n -> Test
+  testWhnfT : String -> Term Three d n -> Term Three d n -> Test
   testWhnfT = testWhnf whnfT
 
-  testWhnfE : String -> Elim d n -> Elim d n -> Test
+  testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test
   testWhnfE = testWhnf whnfE
 
-  testNoStepE : String -> Elim d n -> Test
+  testNoStepE : String -> Elim Three d n -> Test
   testNoStepE = testNoStep stepE
 
-  testNoStepT : String -> Term d n -> Test
+  testNoStepT : String -> Term Three d n -> Test
   testNoStepT = testNoStep stepT