From ba2818a8659d125a0a3f430f17a7758e55754d11 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 1 Apr 2023 19:16:43 +0200
Subject: [PATCH] remove IsQty interface

---
 lib/Quox/Definition.idr              |  73 ++++-------
 lib/Quox/Equal.idr                   | 102 ++++++++-------
 lib/Quox/Parser/FromParser.idr       |  63 +++++-----
 lib/Quox/Parser/FromParser/Error.idr |   4 +-
 lib/Quox/Parser/Parser.idr           |  14 +--
 lib/Quox/Parser/Syntax.idr           |  27 ++--
 lib/Quox/Reduce.idr                  |  17 ++-
 lib/Quox/Syntax/Qty.idr              | 179 +++++++++++++++++----------
 lib/Quox/Syntax/Qty/Three.idr        | 143 ---------------------
 lib/Quox/Syntax/Term/Base.idr        | 138 ++++++++++-----------
 lib/Quox/Syntax/Term/Pretty.idr      |  37 +++---
 lib/Quox/Syntax/Term/Split.idr       |  82 ++++++------
 lib/Quox/Syntax/Term/Subst.idr       |  88 ++++++-------
 lib/Quox/Typechecker.idr             |  99 +++++++--------
 lib/Quox/Typing.idr                  |  77 ++++++------
 lib/Quox/Typing/Context.idr          | 103 ++++++++-------
 lib/Quox/Typing/Error.idr            | 106 ++++++++--------
 lib/quox-lib.ipkg                    |   1 -
 tests/TermImpls.idr                  |   8 +-
 tests/Tests/Equal.idr                |  90 +++++++-------
 tests/Tests/PrettyTerm.idr           |   9 +-
 tests/Tests/Reduce.idr               |  13 +-
 tests/Tests/Typechecker.idr          | 127 ++++++++++---------
 tests/TypingImpls.idr                |  18 +--
 24 files changed, 729 insertions(+), 889 deletions(-)
 delete mode 100644 lib/Quox/Syntax/Qty/Three.idr

diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index c410fa2..6d65ad0 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -8,85 +8,60 @@ import Decidable.Decidable
 
 
 public export
-data DefBody q =
-    Concrete (Term q 0 0)
+data DefBody =
+    Concrete (Term 0 0)
   | Postulate
 
 namespace DefBody
   public export
-  (.term0) : DefBody q -> Maybe (Term q 0 0)
+  (.term0) : DefBody -> Maybe (Term 0 0)
   (Concrete t).term0 = Just t
   (Postulate).term0  = Nothing
 
 
 public export
-record Definition' q (isGlobal : Pred q) where
+record Definition where
   constructor MkDef
-  qty   : q
-  type0 : Term q 0 0
-  body0 : DefBody q
-  {auto 0 qtyGlobal : isGlobal qty}
-
-public export
-0 Definition : (q : Type) -> IsQty q => Type
-Definition q = Definition' q IsGlobal
+  qty   : GQty
+  type0 : Term 0 0
+  body0 : DefBody
 
 public export %inline
-mkPostulate : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
-             (type0 : Term q 0 0) -> Definition q
+mkPostulate : GQty -> (type0 : Term 0 0) -> Definition
 mkPostulate qty type0 = MkDef {qty, type0, body0 = Postulate}
 
 public export %inline
-mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
-        (type0, term0 : Term q 0 0) -> Definition q
+mkDef : GQty -> (type0, term0 : Term 0 0) -> Definition
 mkDef qty type0 term0 = MkDef {qty, type0, body0 = Concrete term0}
 
 
-public export %inline
-(.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
-g.qtyP = Element g.qty g.qtyGlobal
-
 parameters {d, n : Nat}
   public export %inline
-  (.type) : Definition' q _ -> Term q d n
+  (.type) : Definition -> Term d n
   g.type = g.type0 // shift0 d // shift0 n
 
   public export %inline
-  (.term) : Definition' q _ -> Maybe (Term q d n)
+  (.term) : Definition -> Maybe (Term d n)
   g.term = g.body0.term0 <&> \t => t // shift0 d // shift0 n
 
   public export %inline
-  toElim : Definition' q _ -> Maybe $ Elim q d n
+  toElim : Definition -> Maybe $ Elim d n
   toElim def = pure $ !def.term :# def.type
 
 
+public export %inline
+isZero : Definition -> Bool
+isZero g = g.qty.fst == Zero
+
+
 public export
-0 IsZero : IsQty q => Pred $ Definition q
-IsZero g = IsZero g.qty
+Definitions : Type
+Definitions = SortedMap Name Definition
+
+public export
+0 DefsReader : Type -> Type
+DefsReader = Reader Definitions
 
 public export %inline
-isZero : (p : IsQty q) => Dec1 $ Definition.IsZero @{p}
-isZero g = isZero g.qty
-
-
-public export
-0 Definitions' : (q : Type) -> Pred q -> 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 DefsReader' : (q : Type) -> (q -> Type) -> Type -> Type
-DefsReader' q isGlobal = Reader (Definitions' q isGlobal)
-
-public export
-0 DefsReader : (q : Type) -> IsQty q => Type -> Type
-DefsReader q = DefsReader' q IsGlobal
-
-public export %inline
-lookupElim : forall isGlobal. {d, n : Nat} ->
-             Name -> Definitions' q isGlobal -> Maybe (Elim q d n)
+lookupElim : {d, n : Nat} -> Name -> Definitions -> Maybe (Elim d n)
 lookupElim x defs = toElim !(lookup x defs)
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index b2b3daf..a422cbf 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -13,12 +13,12 @@ public export
 EqModeState = State EqMode
 
 public export
-0 EqualEff : Type -> List (Type -> Type)
-EqualEff q = [ErrorEff q, EqModeState]
+0 EqualEff : List (Type -> Type)
+EqualEff = [ErrorEff, EqModeState]
 
 public export
-0 EqualE : Type -> Type -> Type
-EqualE q = Eff $ EqualEff q
+0 EqualE : Type -> Type
+EqualE = Eff $ EqualEff
 
 
 export %inline
@@ -26,21 +26,21 @@ mode : Has EqModeState fs => Eff fs EqMode
 mode = get
 
 
-parameters (ctx : EqContext q n)
+parameters (ctx : EqContext n)
   private %inline
-  clashT : Term q 0 n -> Term q 0 n -> Term q 0 n -> EqualE q a
+  clashT : Term 0 n -> Term 0 n -> Term 0 n -> EqualE a
   clashT ty s t = throw $ ClashT ctx !mode ty s t
 
   private %inline
-  clashTy : Term q 0 n -> Term q 0 n -> EqualE q a
+  clashTy : Term 0 n -> Term 0 n -> EqualE a
   clashTy s t = throw $ ClashTy ctx !mode s t
 
   private %inline
-  clashE : Elim q 0 n -> Elim q 0 n -> EqualE q a
+  clashE : Elim 0 n -> Elim 0 n -> EqualE a
   clashE e f = throw $ ClashE ctx !mode e f
 
   private %inline
-  wrongType : Term q 0 n -> Term q 0 n -> EqualE q a
+  wrongType : Term 0 n -> Term 0 n -> EqualE a
   wrongType ty s = throw $ WrongType ctx ty s
 
 
@@ -70,7 +70,7 @@ isTyCon (CloT  {}) = False
 isTyCon (DCloT {}) = False
 
 public export %inline
-sameTyCon : (s, t : Term q d n) ->
+sameTyCon : (s, t : Term d n) ->
             (0 ts : So (isTyCon s)) => (0 tt : So (isTyCon t)) =>
             Bool
 sameTyCon (TYPE {}) (TYPE {}) = True
@@ -91,7 +91,7 @@ sameTyCon (E    {}) (E    {}) = True
 sameTyCon (E    {}) _         = False
 
 
-parameters (defs : Definitions' q g)
+parameters (defs : Definitions)
   ||| true if a type is known to be a subsingleton purely by its form.
   ||| a subsingleton is a type with only zero or one possible values.
   ||| equality/subtyping accepts immediately on values of subsingleton types.
@@ -102,8 +102,8 @@ parameters (defs : Definitions' q g)
   |||   boundary separation.
   ||| * an enum type is a subsingleton if it has zero or one tags.
   public export covering
-  isSubSing : Has (ErrorEff q) fs =>
-              {n : Nat} -> Term q 0 n -> Eff fs Bool
+  isSubSing : Has ErrorEff fs =>
+              {n : Nat} -> Term 0 n -> Eff fs Bool
   isSubSing ty0 = do
     Element ty0 nc <- whnfT defs ty0
     case ty0 of
@@ -126,14 +126,14 @@ parameters (defs : Definitions' q g)
 
 
 export
-ensureTyCon : Has (ErrorEff q) fs =>
-              (ctx : EqContext q n) -> (t : Term q 0 n) ->
+ensureTyCon : Has ErrorEff fs =>
+              (ctx : EqContext n) -> (t : Term 0 n) ->
               Eff fs (So (isTyCon t))
 ensureTyCon ctx t = case nchoose $ isTyCon t of
   Left  y => pure y
   Right n => throw $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
 
-parameters (defs : Definitions' q _) {auto _ : IsQty q}
+parameters (defs : Definitions)
   mutual
     namespace Term
       ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
@@ -141,7 +141,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
       |||
       ||| ⚠ **assumes that `s`, `t` have already been checked against `ty`**. ⚠
       export covering %inline
-      compare0 : EqContext q n -> (ty, s, t : Term q 0 n) -> EqualE q ()
+      compare0 : EqContext n -> (ty, s, t : Term 0 n) -> EqualE ()
       compare0 ctx ty s t =
         wrapErr (WhileComparingT ctx !mode ty s t) $ do
           let Val n = ctx.termLen
@@ -154,15 +154,15 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
       ||| converts an elim "Γ ⊢ e" to "Γ, x ⊢ e x", for comparing with
       ||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
       private %inline
-      toLamBody : Elim q d n -> Term q d (S n)
+      toLamBody : Elim d n -> Term d (S n)
       toLamBody e = E $ weakE e :@ BVT 0
 
       private covering
-      compare0' : EqContext q n ->
-                  (ty, s, t : Term q 0 n) ->
+      compare0' : EqContext n ->
+                  (ty, s, t : Term 0 n) ->
                   (0 nty : NotRedex defs ty) => (0 tty : So (isTyCon ty)) =>
                   (0 ns  : NotRedex defs s)  => (0 nt  : NotRedex defs t) =>
-                  EqualE q ()
+                  EqualE ()
       compare0' ctx (TYPE _) s t = compareType ctx s t
 
       compare0' ctx ty@(Pi {qty, arg, res}) s t {n} = local_ Equal $
@@ -184,10 +184,10 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
           (E _,   t) => wrongType ctx ty t
           (s,     _) => wrongType ctx ty s
         where
-          ctx' : EqContext q (S n)
+          ctx' : EqContext (S n)
           ctx' = extendTy qty res.name arg ctx
 
-          eta : Elim q 0 n -> ScopeTerm q 0 n -> EqualE q ()
+          eta : Elim 0 n -> ScopeTerm 0 n -> EqualE ()
           eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
           eta e (S _ (N _)) = clashT ctx ty s t
 
@@ -281,7 +281,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
     ||| compares two types, using the current variance `mode` for universes.
     ||| fails if they are not types, even if they would happen to be equal.
     export covering %inline
-    compareType : EqContext q n -> (s, t : Term q 0 n) -> EqualE q ()
+    compareType : EqContext n -> (s, t : Term 0 n) -> EqualE ()
     compareType ctx s t = do
       let Val n = ctx.termLen
       Element s ns <- whnfT defs s
@@ -293,11 +293,11 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
       compareType' ctx s t
 
     private covering
-    compareType' : EqContext q n -> (s, t : Term q 0 n) ->
+    compareType' : EqContext n -> (s, t : Term 0 n) ->
                    (0 ns : NotRedex defs s) => (0 ts : So (isTyCon s)) =>
                    (0 nt : NotRedex defs t) => (0 tt : So (isTyCon t)) =>
                    (0 st : So (sameTyCon s t)) =>
-                   EqualE q ()
+                   EqualE ()
     -- equality is the same as subtyping, except with the
     -- "≤" in the TYPE rule being replaced with "="
     compareType' ctx (TYPE k) (TYPE l) =
@@ -313,7 +313,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
       --  Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
       expectEqualQ sQty tQty
       local flip $ compareType ctx sArg tArg -- contra
-      compareType (extendTy zero sRes.name sArg ctx) sRes.term tRes.term
+      compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
 
     compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
                      (Sig {fst = tFst, snd = tSnd, _}) = do
@@ -321,7 +321,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
       -- --------------------------------------
       --   Γ ⊢ (x : A₁) × B₁ <: (x : A₂) × B₂
       compareType ctx sFst tFst
-      compareType (extendTy zero sSnd.name sFst ctx) sSnd.term tSnd.term
+      compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term
 
     compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
                      (Eq {ty = tTy, l = tl, r = tr, _}) = do
@@ -361,9 +361,9 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
     |||
     ||| ⚠ **assumes the elim is already typechecked.** ⚠
     private covering
-    computeElimType : EqContext q n -> (e : Elim q 0 n) ->
+    computeElimType : EqContext n -> (e : Elim 0 n) ->
                       (0 ne : NotRedex defs e) ->
-                      EqualE q (Term q 0 n)
+                      EqualE (Term 0 n)
     computeElimType ctx (F x) _ = do
       defs <- lookupFree' defs x
       pure $ injectT ctx defs.type
@@ -381,9 +381,9 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
     computeElimType ctx (_ :# ty) _ = pure ty
 
     private covering
-    replaceEnd : EqContext q n ->
-                 (e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
-                 EqualE q (Elim q 0 n)
+    replaceEnd : EqContext n ->
+                 (e : Elim 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
+                 EqualE (Elim 0 n)
     replaceEnd ctx e p ne = do
       (ty, l, r) <- expectEqE defs ctx !(computeElimType ctx e ne)
       pure $ ends l r p :# dsub1 ty (K p)
@@ -397,7 +397,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
       ||| ⚠ **assumes that they have both been typechecked, and have
       ||| equal types.** ⚠
       export covering %inline
-      compare0 : EqContext q n -> (e, f : Elim q 0 n) -> EqualE q ()
+      compare0 : EqContext n -> (e, f : Elim 0 n) -> EqualE ()
       compare0 ctx e f =
         wrapErr (WhileComparingE ctx !mode e f) $ do
           let Val n = ctx.termLen
@@ -408,10 +408,10 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
             compare0' ctx e f ne nf
 
       private covering
-      compare0' : EqContext q n ->
-                  (e, f : Elim q 0 n) ->
+      compare0' : EqContext n ->
+                  (e, f : Elim 0 n) ->
                   (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
-                  EqualE q ()
+                  EqualE ()
       -- replace applied equalities with the appropriate end first
       -- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
       --
@@ -439,7 +439,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
         local_ Equal $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
-          compareType (extendTy zero eret.name ety ctx) eret.term fret.term
+          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
           (fst, snd) <- expectSigE defs ctx ety
           let [< x, y] = ebody.names
           Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
@@ -453,13 +453,13 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
         local_ Equal $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
-          compareType (extendTy zero eret.name ety ctx) eret.term fret.term
+          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
           for_ !(expectEnumE defs ctx ety) $ \t =>
             compare0 ctx (sub1 eret $ Tag t :# ety)
               !(lookupArm t earms) !(lookupArm t farms)
           expectEqualQ epi fpi
         where
-          lookupArm : TagVal -> CaseEnumArms q d n -> EqualE q (Term q d n)
+          lookupArm : TagVal -> CaseEnumArms d n -> EqualE (Term d n)
           lookupArm t arms = case lookup t arms of
             Just arm => pure arm
             Nothing  => throw $ TagNotIn t (fromList $ keys arms)
@@ -470,7 +470,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
         local_ Equal $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
-          compareType (extendTy zero eret.name ety ctx) eret.term fret.term
+          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
           compare0 ctx (sub1 eret (Zero :# Nat)) ezer fzer
           let [< p, ih] = esuc.names
           compare0 (extendTyN [< (epi, p, Nat), (epi', ih, eret.term)] ctx)
@@ -485,7 +485,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
         local_ Equal $ do
           compare0 ctx e f
           ety <- computeElimType ctx e (noOr1 ne)
-          compareType (extendTy zero eret.name ety ctx) eret.term fret.term
+          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
           (q, ty) <- expectBOXE defs ctx ety
           compare0 (extendTy (epi * q) ebody.name ty ctx)
             (substCaseBoxRet ety eret)
@@ -496,7 +496,7 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
       compare0' ctx (s :# a) (t :# b) _ _ =
           Term.compare0 ctx !(bigger a b) s t
         where
-          bigger : forall a. a -> a -> EqualE q a
+          bigger : forall a. a -> a -> EqualE a
           bigger l r = mode <&> \case Super => l; _ => r
 
       compare0' ctx   (s :# a) f        _ _ = Term.compare0 ctx a s (E f)
@@ -504,16 +504,14 @@ parameters (defs : Definitions' q _) {auto _ : IsQty q}
       compare0' ctx e@(_ :# _) f        _ _ = clashE ctx e f
 
 
-parameters {auto _ : (Has (DefsReader' q _) fs, Has (ErrorEff q) fs)}
-           {auto _ : IsQty q}
-           (ctx : TyContext q d n)
+parameters {auto _ : (Has DefsReader fs, Has ErrorEff fs)} (ctx : TyContext d n)
   -- [todo] only split on the dvars that are actually used anywhere in
   -- the calls to `splits`
 
   parameters (mode : EqMode)
     namespace Term
       export covering
-      compare : (ty, s, t : Term q d n) -> Eff fs ()
+      compare : (ty, s, t : Term d n) -> Eff fs ()
       compare ty s t = do
         defs <- ask
         map fst $ runState @{Z} mode $
@@ -522,7 +520,7 @@ parameters {auto _ : (Has (DefsReader' q _) fs, Has (ErrorEff q) fs)}
             lift $ compare0 defs ectx (ty // th) (s // th) (t // th)
 
       export covering
-      compareType : (s, t : Term q d n) -> Eff fs ()
+      compareType : (s, t : Term d n) -> Eff fs ()
       compareType s t = do
         defs <- ask
         map fst $ runState @{Z} mode $
@@ -534,7 +532,7 @@ parameters {auto _ : (Has (DefsReader' q _) fs, Has (ErrorEff q) fs)}
       ||| you don't have to pass the type in but the arguments must still be
       ||| of the same type!!
       export covering %inline
-      compare : (e, f : Elim q d n) -> Eff fs ()
+      compare : (e, f : Elim d n) -> Eff fs ()
       compare e f = do
         defs <- ask
         map fst $ runState @{Z} mode $
@@ -544,20 +542,20 @@ parameters {auto _ : (Has (DefsReader' q _) fs, Has (ErrorEff q) fs)}
 
   namespace Term
     export covering %inline
-    equal, sub, super : (ty, s, t : Term q d n) -> Eff fs ()
+    equal, sub, super : (ty, s, t : Term d n) -> Eff fs ()
     equal = compare Equal
     sub   = compare Sub
     super = compare Super
 
     export covering %inline
-    equalType, subtype, supertype : (s, t : Term q d n) -> Eff fs ()
+    equalType, subtype, supertype : (s, t : Term d n) -> Eff fs ()
     equalType = compareType Equal
     subtype   = compareType Sub
     supertype = compareType Super
 
   namespace Elim
     export covering %inline
-    equal, sub, super : (e, f : Elim q d n) -> Eff fs ()
+    equal, sub, super : (e, f : Elim d n) -> Eff fs ()
     equal = compare Equal
     sub   = compare Sub
     super = compare Super
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index afe2ae4..c7b7701 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -23,16 +23,8 @@ import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
 
 
 public export
-0 Def : Type
-Def = Definition Three
-
-public export
-0 NDef : Type
-NDef = (Name, Def)
-
-public export
-0 Defs : Type
-Defs = Definitions Three
+0 NDefinition : Type
+NDefinition = (Name, Definition)
 
 public export
 0 IncludePath : Type
@@ -49,7 +41,7 @@ data StateTag = DEFS | NS | SEEN
 public export
 0 FromParserEff : List (Type -> Type)
 FromParserEff =
-  [Except Error, StateL DEFS Defs, StateL NS Mods,
+  [Except Error, StateL DEFS Definitions, StateL NS Mods,
    Reader IncludePath, StateL SEEN SeenFiles, IO]
 
 public export
@@ -76,7 +68,7 @@ fromPDimWith ds (V i) =
 
 private
 avoidDim : Has (Except Error) fs =>
-           Context' BName d -> PName -> Eff fs (Term q d n)
+           Context' BName d -> PName -> Eff fs (Term d n)
 avoidDim ds x =
   fromName (const $ throw $ DimNameInTerm x.base) (pure . FT . fromPName) ds x
 
@@ -85,7 +77,7 @@ mutual
   export
   fromPTermWith : Has (Except Error) fs =>
                   Context' BName d -> Context' BName n ->
-                  PTerm -> Eff fs (Term Three d n)
+                  PTerm -> Eff fs (Term d n)
   fromPTermWith ds ns t0 = case t0 of
     TYPE k =>
       pure $ TYPE $ k
@@ -168,14 +160,14 @@ mutual
   private
   fromPTermEnumArms : Has (Except Error) fs =>
                       Context' BName d -> Context' BName n ->
-                      List (TagVal, PTerm) -> Eff fs (CaseEnumArms Three d n)
+                      List (TagVal, PTerm) -> Eff fs (CaseEnumArms d n)
   fromPTermEnumArms ds ns =
     map SortedMap.fromList . traverse (traverse $ fromPTermWith ds ns)
 
   private
   fromPTermElim : Has (Except Error) fs =>
                   Context' BName d -> Context' BName n ->
-                  PTerm -> Eff fs (Elim Three d n)
+                  PTerm -> Eff fs (Elim d n)
   fromPTermElim ds ns e =
     case !(fromPTermWith ds ns e) of
       E e => pure e
@@ -186,7 +178,7 @@ mutual
   fromPTermTScope : {s : Nat} -> Has (Except Error) fs =>
                     Context' BName d -> Context' BName n ->
                     SnocVect s BName ->
-                    PTerm -> Eff fs (ScopeTermN s Three d n)
+                    PTerm -> Eff fs (ScopeTermN s d n)
   fromPTermTScope ds ns xs t =
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
@@ -198,7 +190,7 @@ mutual
   fromPTermDScope : {s : Nat} -> Has (Except Error) fs =>
                     Context' BName d -> Context' BName n ->
                     SnocVect s BName ->
-                    PTerm -> Eff fs (DScopeTermN s Three d n)
+                    PTerm -> Eff fs (DScopeTermN s d n)
   fromPTermDScope ds ns xs t =
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
@@ -208,16 +200,16 @@ mutual
 
 
 export %inline
-fromPTerm : Has (Except Error) fs => PTerm -> Eff fs (Term Three 0 0)
+fromPTerm : Has (Except Error) fs => PTerm -> Eff fs (Term 0 0)
 fromPTerm = fromPTermWith [<] [<]
 
 
 export
 globalPQty : Has (Except Error) fs =>
-             (q : PQty) -> Eff fs (IsGlobal q)
-globalPQty pi = case isGlobal pi of
-  Yes y => pure y
-  No  n => throw $ QtyNotGlobal pi
+             (q : Qty) -> Eff fs (So $ isGlobal q)
+globalPQty pi = case choose $ isGlobal pi of
+  Left  y => pure y
+  Right _ => throw $ QtyNotGlobal pi
 
 
 export
@@ -225,40 +217,41 @@ fromPNameNS : Has (StateL NS Mods) fs => PName -> Eff fs Name
 fromPNameNS name = pure $ addMods !(getAt NS) $ fromPName name
 
 private
-injTC : (Has (StateL DEFS Defs) fs, Has (Except Error) fs) =>
-        TC Three a -> Eff fs a
+injTC : (Has (StateL DEFS Definitions) fs, Has (Except Error) fs) =>
+        TC a -> Eff fs a
 injTC act = rethrow $ mapFst TypeError $ runTC !(getAt DEFS) act
 
 export covering
-fromPDef : (Has (StateL DEFS Defs) fs,
+fromPDef : (Has (StateL DEFS Definitions) fs,
             Has (StateL NS Mods) fs,
             Has (Except Error) fs) =>
-           PDefinition -> Eff fs NDef
+           PDefinition -> Eff fs NDefinition
 fromPDef (MkPDef qty pname ptype pterm) = do
   name <- fromPNameNS pname
   qtyGlobal <- globalPQty qty
-  let sqty = globalToSubj $ Element qty qtyGlobal
+  let gqty = Element qty qtyGlobal
+  let sqty = globalToSubj gqty
   type <- traverse fromPTerm ptype
   term <- fromPTerm pterm
   case type of
     Just type => do
       injTC $ checkTypeC empty type Nothing
       injTC $ ignore $ checkC empty sqty term type
-      let def = mkDef qty type term
+      let def = mkDef gqty type term
       modifyAt DEFS $ insert name def
       pure (name, def)
     Nothing => do
       let E elim = term | _ => throw $ AnnotationNeeded pterm
       res <- injTC $ inferC empty sqty elim
-      let def = mkDef qty res.type term
+      let def = mkDef gqty res.type term
       modifyAt DEFS $ insert name def
       pure (name, def)
 
 export covering
-fromPDecl : (Has (StateL DEFS Defs) fs,
+fromPDecl : (Has (StateL DEFS Definitions) fs,
              Has (StateL NS Mods) fs,
              Has (Except Error) fs) =>
-            PDecl -> Eff fs (List NDef)
+            PDecl -> Eff fs (List NDefinition)
 fromPDecl (PDef def) = singleton <$> fromPDef def
 fromPDecl (PNs  ns)  =
   localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
@@ -284,11 +277,11 @@ parameters {auto _ : (Has IO fs,
                       Has (StateL SEEN SeenFiles) fs,
                       Has (Reader IncludePath) fs,
                       Has (Except Error) fs,
-                      Has (StateL DEFS Defs) fs,
+                      Has (StateL DEFS Definitions) fs,
                       Has (StateL NS Mods) fs)}
  mutual
   export covering
-  loadProcessFile : String -> Eff fs (List NDef)
+  loadProcessFile : String -> Eff fs (List NDefinition)
   loadProcessFile file =
     case !(loadFile file) of
       Just inp => do
@@ -298,14 +291,14 @@ parameters {auto _ : (Has IO fs,
 
   ||| populates the `defs` field of the state
   export covering
-  fromPTopLevel : PTopLevel -> Eff fs (List NDef)
+  fromPTopLevel : PTopLevel -> Eff fs (List NDefinition)
   fromPTopLevel (PD    decl) = fromPDecl decl
   fromPTopLevel (PLoad file) = loadProcessFile file
 
 
 export
 fromParserIO : (MonadRec io, HasIO io) =>
-               IncludePath -> IORef SeenFiles -> IORef Defs ->
+               IncludePath -> IORef SeenFiles -> IORef Definitions ->
                FromParser a -> io (Either Error a)
 fromParserIO inc seen defs act =
   runIO $
diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr
index 9f7a004..d4d20ec 100644
--- a/lib/Quox/Parser/FromParser/Error.idr
+++ b/lib/Quox/Parser/FromParser/Error.idr
@@ -12,9 +12,9 @@ data Error =
     AnnotationNeeded PTerm
   | DuplicatesInEnum (List TagVal)
   | DimNotInScope PBaseName
-  | QtyNotGlobal PQty
+  | QtyNotGlobal Qty
   | DimNameInTerm PBaseName
-  | TypeError (Typing.Error Three)
+  | TypeError Typing.Error
   | LoadError String FileError
   | ParseError Parser.Error
 %hide Typing.Error
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index 4563b97..fe7d804 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -113,7 +113,7 @@ dimConst = terminal "expecting 0 or 1" $
   \case Nat 0 => Just Zero; Nat 1 => Just One; _ => Nothing
 
 export
-qty : Grammar True PQty
+qty : Grammar True Qty
 qty = terminal "expecting quantity" $
   \case Nat 0 => Just Zero; Nat 1 => Just One; Reserved "ω" => Just Any
         _ => Nothing
@@ -141,7 +141,7 @@ symbolsC lst = symbols lst <* commit
 
 
 private covering
-qtys : Grammar False (List PQty)
+qtys : Grammar False (List Qty)
 qtys = option [] [|toList $ some qty <* res "."|]
 
 
@@ -151,7 +151,7 @@ dim = [|V baseName|] <|> [|K dimConst|]
 
 private
 0 PBinderHead : Nat -> Type
-PBinderHead n = (Vect n PQty, BName, PTerm)
+PBinderHead n = (Vect n Qty, BName, PTerm)
 
 private
 toVect : List a -> (n ** Vect n a)
@@ -164,7 +164,7 @@ lamIntro : Grammar True (BName -> PTerm -> PTerm)
 lamIntro = symbolsC [(Lam, "λ"), (DLam, "δ")]
 
 private covering
-caseIntro : Grammar True PQty
+caseIntro : Grammar True Qty
 caseIntro = symbols [(One, "case1"), (Any, "caseω")]
         <|> resC "case" *>
               (qty <* resC "." <|>
@@ -205,7 +205,7 @@ mutual
     zeroCase : Grammar True PTerm
     zeroCase = (resC "zero" <|> zero) *> darr *> term
 
-    succCase : Grammar True (BName, PQty, BName, PTerm)
+    succCase : Grammar True (BName, Qty, BName, PTerm)
     succCase = do
       resC "succ"
       n  <- bname
@@ -223,7 +223,7 @@ mutual
     pi, sigma : Grammar True PTerm
     pi = [|makePi (qty <* res ".") domain (resC "→" *> term)|]
     where
-      makePi : PQty -> (BName, PTerm) -> PTerm -> PTerm
+      makePi : Qty -> (BName, PTerm) -> PTerm -> PTerm
       makePi q (x, s) t = Pi q x s t
       domain = binderHead <|> [|(Nothing,) aTerm|]
 
@@ -290,7 +290,7 @@ mutual
 
 
 export covering
-defIntro : Grammar True PQty
+defIntro : Grammar True Qty
 defIntro = symbols [(Zero, "def0"), (Any, "defω")]
        <|> resC "def" *> option Any (qty <* resC ".")
 
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index b8a9182..1be0b11 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -1,7 +1,6 @@
 module Quox.Parser.Syntax
 
 import public Quox.Syntax
-import public Quox.Syntax.Qty.Three
 import public Quox.Definition
 
 import Derive.Prelude
@@ -19,10 +18,6 @@ public export
 0 PUniverse : Type
 PUniverse = Nat
 
-public export
-0 PQty : Type
-PQty = Three
-
 namespace PDim
   public export
   data PDim = K DimConst | V PBaseName
@@ -36,13 +31,13 @@ namespace PTerm
     data PTerm =
         TYPE Nat
 
-      | Pi PQty BName PTerm PTerm
+      | Pi Qty BName PTerm PTerm
       | Lam BName PTerm
       | (:@) PTerm PTerm
 
       | Sig BName PTerm PTerm
       | Pair PTerm PTerm
-      | Case PQty PTerm (BName, PTerm) (PCaseBody)
+      | Case Qty PTerm (BName, PTerm) (PCaseBody)
 
       | Enum (List TagVal)
       | Tag TagVal
@@ -54,7 +49,7 @@ namespace PTerm
       | Nat
       | Zero | Succ PTerm
 
-      | BOX PQty PTerm
+      | BOX Qty PTerm
       | Box PTerm
 
       | V PName
@@ -65,7 +60,7 @@ namespace PTerm
     data PCaseBody =
         CasePair (BName, BName) PTerm
       | CaseEnum (List (TagVal, PTerm))
-      | CaseNat PTerm (BName, PQty, BName, PTerm)
+      | CaseNat PTerm (BName, Qty, BName, PTerm)
       | CaseBox BName PTerm
     %name PCaseBody body
 
@@ -75,7 +70,7 @@ namespace PTerm
 public export
 record PDefinition where
   constructor MkPDef
-  qty  : PQty
+  qty  : Qty
   name : PName
   type : Maybe PTerm
   term : PTerm
@@ -117,14 +112,14 @@ mutual
   namespace Term
     export
     toPTermWith : Context' PBaseName d -> Context' PBaseName n ->
-                  Term Three d n -> PTerm
+                  Term d n -> PTerm
     toPTermWith ds ns t =
       let Element t _ = pushSubsts t in
       toPTermWith' ds ns t
 
     private
     toPTermWith' : Context' PBaseName d -> Context' PBaseName n ->
-                   (t : Term Three d n) -> (0 _ : NotClo t) =>
+                   (t : Term d n) -> (0 _ : NotClo t) =>
                    PTerm
     toPTermWith' ds ns s = case s of
       TYPE l =>
@@ -162,14 +157,14 @@ mutual
   namespace Elim
     export
     toPTermWith : Context' PBaseName d -> Context' PBaseName n ->
-                  Elim Three d n -> PTerm
+                  Elim d n -> PTerm
     toPTermWith ds ns e =
       let Element e _ = pushSubsts e in
       toPTermWith' ds ns e
 
     private
     toPTermWith' : Context' PBaseName d -> Context' PBaseName n ->
-                   (e : Elim Three d n) -> (0 _ : NotClo e) =>
+                   (e : Elim d n) -> (0 _ : NotClo e) =>
                    PTerm
     toPTermWith' ds ns e = case e of
       F x =>
@@ -205,12 +200,12 @@ mutual
 
 namespace Term
   export
-  toPTerm : Term Three 0 0 -> PTerm
+  toPTerm : Term 0 0 -> PTerm
   toPTerm = toPTermWith [<] [<]
 
 namespace Elim
   export
-  toPTerm : Elim Three 0 0 -> PTerm
+  toPTerm : Elim 0 0 -> PTerm
   toPTerm = toPTermWith [<] [<]
 
 public export
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index aba7d69..7c0a7a8 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -18,31 +18,30 @@ data WhnfError = MissingEnumArm TagVal (List TagVal)
 
 public export
 0 RedexTest : TermLike -> Type
-RedexTest tm = forall q, g. {d, n : Nat} -> Definitions' q g -> tm q d n -> Bool
+RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
 
 public export
 interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) (0 err : Type) | tm
 where
-  whnf : {d, n : Nat} -> (defs : Definitions' q g) ->
-         tm q d n -> Either err (Subset (tm q d n) (No . isRedex defs))
+  whnf : {d, n : Nat} -> (defs : Definitions) ->
+         tm d n -> Either err (Subset (tm d n) (No . isRedex defs))
 
 public export
 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex err =>
-                      Definitions' q g -> Pred (tm q d n)
+                      Definitions -> Pred (tm d n)
 IsRedex  defs = So . isRedex defs
 NotRedex defs = No . isRedex defs
 
 public export
 0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
              Whnf tm isRedex err =>
-             (q : Type) -> (d, n : Nat) -> {g : _} ->
-             (defs : Definitions' q g) -> Type
-NonRedex tm q d n defs = Subset (tm q d n) (NotRedex defs)
+             (d, n : Nat) -> (defs : Definitions) -> Type
+NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
 
 public export %inline
 nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex err) =>
-       (t : tm q d n) -> (0 nr : NotRedex defs t) =>
-       NonRedex tm q d n defs
+       (t : tm d n) -> (0 nr : NotRedex defs t) =>
+       NonRedex tm d n defs
 nred t = Element t nr
 
 
diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index 1612e75..856c4ea 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -1,91 +1,144 @@
+||| quantities count how many times a bound variable is used [@nuttin; @qtt].
+|||
+||| i tried grtt [@grtt] for a bit but i think it was more complex than
+||| it's worth in a language that has other stuff going on too
 module Quox.Syntax.Qty
 
 import Quox.Pretty
-import Quox.Name
-import public Quox.Decidable
+import Quox.Decidable
 import Data.DPair
+import Derive.Prelude
 
 %default total
+%language ElabReflection
 
 
+||| the possibilities we care about are:
+|||
+||| - 0: a variable is used only at compile time, not run time
+||| - 1: a variable is used exactly once at run time
+||| - ω (or #): don't care. an ω variable *can* also be used 0/1 time
+public export
+data Qty = Zero | One | Any
+%name Qty.Qty pi, rh
+
+%runElab derive "Qty" [Eq, Ord, Show]
+
+
+export
+PrettyHL Qty where
+  prettyM pi = hl Qty <$>
+    case pi of
+      Zero => pure "0"
+      One  => pure "1"
+      Any  => ifUnicode "ω" "#"
+
+||| prints in a form that can be a suffix of "case"
+public export
+prettySuffix : Pretty.HasEnv m => Qty -> m (Doc HL)
+prettySuffix = prettyM
+
 public export
-interface Eq q => IsQty q where
-  zero, one, any : q
+DecEq Qty where
+  decEq Zero Zero = Yes Refl
+  decEq Zero One  = No $ \case _ impossible
+  decEq Zero Any  = No $ \case _ impossible
+  decEq One  Zero = No $ \case _ impossible
+  decEq One  One  = Yes Refl
+  decEq One  Any  = No $ \case _ impossible
+  decEq Any  Zero = No $ \case _ impossible
+  decEq Any  One  = No $ \case _ impossible
+  decEq Any  Any  = Yes Refl
 
-  (+), (*) : q -> q -> q
-  lub      : q -> q -> Maybe q
 
-  ||| true if bindings of this quantity will be erased
-  ||| and must not be runtime relevant
-  IsZero : Pred q
-  isZero : Dec1 IsZero
-  zeroIsZero : IsZero zero
+||| e.g. if in the expression `(s, t)`, the variable `x` is
+||| used π times in `s` and ρ times in `t`, then it's used
+||| (π + ρ) times in the whole expression
+public export
+(+) : Qty -> Qty -> Qty
+Zero + rh   = rh
+pi   + Zero = pi
+_    + _    = Any
 
-  ||| true if bindings of this quantity can be used any number of times.
-  ||| this is needed for natural elimination
-  IsAny : Pred q
-  isAny : Dec1 IsAny
-  anyIsAny : IsAny any
+||| e.g. if a function `f` uses its argument π times,
+||| and `f x` occurs in a σ context, then `x` is used `πσ` times overall
+public export
+(*) : Qty -> Qty -> Qty
+Zero * _    = Zero
+_    * Zero = Zero
+One  * rh   = rh
+pi   * One  = pi
+Any  * Any  = Any
 
-  ||| ``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` ω``.
-  ||| if ``π `lub` ρ`` exists, then both `π` and `ρ` must be compatible with it
-  Compat : Rel q
-  compat : Dec2 Compat
+||| "π ≤ ρ"
+|||
+||| if a variable is bound with quantity ρ, then it can be used with a total
+||| quantity π as long as π ≤ ρ. for example, an ω variable can be used any
+||| number of times, so π ≤ ω for any π.
+public export
+compat : Qty -> Qty -> Bool
+compat pi Any = True
+compat pi rh  = pi == rh
 
-  ||| true if it is ok for this quantity to appear for the
-  ||| subject of a typing judgement [@qtt, §2.3].
-  IsSubj : Pred q
-  isSubj : Dec1 IsSubj
-  zeroIsSubj : forall pi. IsZero pi -> IsSubj pi
-  oneIsSubj  : IsSubj one
-  timesSubj  : forall pi, rh. IsSubj pi -> IsSubj rh -> IsSubj (pi * rh)
 
-  ||| true if it is ok for a global definition to have this
-  ||| quantity. so not exact usage counts, maybe.
-  IsGlobal : Pred q
-  isGlobal : Dec1 IsGlobal
-  zeroIsGlobal : forall pi. IsZero pi -> IsGlobal pi
-  anyIsGlobal : forall pi. IsAny pi -> IsGlobal pi
+||| "π ∧ ρ"
+|||
+||| returns some quantity τ where π ≤ τ and ρ ≤ τ, if one exists.
+public export
+lub : Qty -> Qty -> Maybe Qty
+lub p q =
+  if p == Any || q == Any then Just Any
+  else if p == q then Just p
+  else Nothing
 
-  ||| prints in a form that can be a suffix of "case"
-  prettySuffix : Pretty.HasEnv m => q -> m (Doc HL)
+
+||| to maintain subject reduction, only 0 or 1 can occur
+||| for the subject of a typing judgment. see @qtt, §2.3 for more detail
+public export
+isSubj : Qty -> Bool
+isSubj Zero = True
+isSubj One  = True
+isSubj Any  = False
 
 public export
-0 SQty : (q : Type) -> IsQty q => Type
-SQty q = Subset q IsSubj
+SQty : Type
+SQty = Subset Qty $ So . isSubj
 
 public export %inline
-szero : IsQty q => SQty q
-szero = Element zero $ zeroIsSubj zeroIsZero
-
-public export %inline
-sone : IsQty q => SQty q
-sone = Element one oneIsSubj
+szero, sone : SQty
+szero = Element Zero Oh
+sone  = Element One  Oh
 
 ||| "σ ⨴ π"
 |||
-||| ``sg `subjMult` pi`` is equal to `pi` if it is zero, otherwise it
-||| is equal to `sg`.
-public export %inline
-subjMult : IsQty q => SQty q -> q -> SQty q
-subjMult sg pi = case isZero pi of
-  Yes y => Element pi $ zeroIsSubj y
-  No  _ => sg
+||| σ ⨭ π is 0 if either of σ or π are, otherwise it is σ.
+public export
+subjMult : SQty -> Qty -> SQty
+subjMult _  Zero = szero
+subjMult sg _    = sg
 
 
+||| it doesn't make much sense for a top level declaration to have a
+||| quantity of 1, so the only distinction is whether it is present
+||| at runtime at all or not
+public export
+isGlobal : Qty -> Bool
+isGlobal Zero = True
+isGlobal One  = False
+isGlobal Any  = True
+
 public export
-0 GQty : (q : Type) -> IsQty q => Type
-GQty q = Subset q IsGlobal
+GQty : Type
+GQty = Subset Qty $ So . isGlobal
 
+public export
+gzero, gany : GQty
+gzero = Element Zero Oh
+gany  = Element Any  Oh
+
+||| when checking a definition, a 0 definition is checked at 0,
+||| but an ω definition is checked at 1 since ω isn't a subject quantity
 public export %inline
-gzero : IsQty q => GQty q
-gzero = Element zero $ zeroIsGlobal zeroIsZero
-
-public export %inline
-gany : IsQty q => GQty q
-gany = Element any $ anyIsGlobal anyIsAny
-
-export %inline
-globalToSubj : IsQty q => GQty q -> SQty q
-globalToSubj q = if isYes $ isZero q.fst then szero else sone
+globalToSubj : GQty -> SQty
+globalToSubj (Element Zero _) = szero
+globalToSubj (Element Any  _) = sone
diff --git a/lib/Quox/Syntax/Qty/Three.idr b/lib/Quox/Syntax/Qty/Three.idr
deleted file mode 100644
index 2a7d64a..0000000
--- a/lib/Quox/Syntax/Qty/Three.idr
+++ /dev/null
@@ -1,143 +0,0 @@
-module Quox.Syntax.Qty.Three
-
-import Quox.Pretty
-import public Quox.Syntax.Qty
-import Derive.Prelude
-
-%default total
-%language ElabReflection
-
-
-public export
-data Three = Zero | One | Any
-%name Three pi, rh
-
-%runElab derive "Three" [Eq, Ord, Show]
-
-
-export
-PrettyHL Three where
-  prettyM pi = hl Qty <$>
-    case pi of
-      Zero => pure "0"
-      One  => pure "1"
-      Any  => ifUnicode "ω" "#"
-
-public export
-DecEq Three where
-  decEq Zero Zero = Yes Refl
-  decEq Zero One  = No $ \case _ impossible
-  decEq Zero Any  = No $ \case _ impossible
-  decEq One  Zero = No $ \case _ impossible
-  decEq One  One  = Yes Refl
-  decEq One  Any  = No $ \case _ impossible
-  decEq Any  Zero = No $ \case _ impossible
-  decEq Any  One  = No $ \case _ impossible
-  decEq Any  Any  = Yes Refl
-
-
-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
-lub3 : Three -> Three -> Maybe Three
-lub3 p q =
-  if p == Any || q == Any then Just Any
-  else if p == q then Just p
-  else Nothing
-
-public export
-data Compat3 : Rel Three where
-  CmpRefl : Compat3 rh rh
-  CmpAny  : Compat3 rh Any
-
-public export
-compat3 : Dec2 Compat3
-compat3 pi rh with (decEq pi rh) | (decEq rh Any)
-  compat3 pi pi  | Yes Refl | _        = Yes CmpRefl
-  compat3 pi Any | No  _    | Yes Refl = Yes CmpAny
-  compat3 pi rh  | No  ne   | No  na   =
-    No $ \case CmpRefl => ne Refl; CmpAny => na Refl
-
-
-public export
-data IsSubj3 : Pred Three where
-  SZero : IsSubj3 Zero
-  SOne  : IsSubj3 One
-
-public export
-isSubj3 : Dec1 IsSubj3
-isSubj3 Zero = Yes SZero
-isSubj3 One  = Yes SOne
-isSubj3 Any  = No $ \case _ impossible
-
-public export
-timesSubj3 : forall pi, rh. IsSubj3 pi -> IsSubj3 rh -> IsSubj3 (times pi rh)
-timesSubj3 SZero SZero = SZero
-timesSubj3 SZero SOne  = SZero
-timesSubj3 SOne  SZero = SZero
-timesSubj3 SOne  SOne  = SOne
-
-
-public export
-data IsGlobal3 : Pred Three where
-  GZero : IsGlobal3 Zero
-  GAny  : IsGlobal3 Any
-
-public export
-isGlobal3 : Dec1 IsGlobal3
-isGlobal3 Zero = Yes GZero
-isGlobal3 One  = No $ \case _ impossible
-isGlobal3 Any  = Yes GAny
-
-
-public export
-IsQty Three where
-  zero = Zero
-  one  = One
-  any  = Any
-
-  (+) = plus
-  (*) = times
-
-  lub = lub3
-
-  IsZero     = Equal Zero
-  isZero     = decEq Zero
-  zeroIsZero = Refl
-
-  IsAny    = Equal Three.Any
-  isAny    = decEq Any
-  anyIsAny = Refl
-
-  Compat = Compat3
-  compat = compat3
-
-  IsSubj     = IsSubj3
-  isSubj     = isSubj3
-  zeroIsSubj = \Refl => SZero
-  oneIsSubj  = SOne
-  timesSubj  = timesSubj3
-
-  IsGlobal     = IsGlobal3
-  isGlobal     = isGlobal3
-  zeroIsGlobal = \Refl => GZero
-  anyIsGlobal  = \Refl => GAny
-
-  prettySuffix = pretty0M
-
-
-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 be74279..be74c2a 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -7,7 +7,6 @@ import public Quox.Syntax.Qty
 import public Quox.Syntax.Dim
 import public Quox.Name
 import public Quox.Context
--- import public Quox.OPE
 
 import Quox.Pretty
 
@@ -25,11 +24,11 @@ import public Data.SortedSet
 
 public export
 0 TermLike : Type
-TermLike = Type -> Nat -> Nat -> Type
+TermLike = Nat -> Nat -> Type
 
 public export
 0 TSubstLike : Type
-TSubstLike = Type -> Nat -> Nat -> Nat -> Type
+TSubstLike = Nat -> Nat -> Nat -> Type
 
 public export
 0 Universe : Type
@@ -44,112 +43,111 @@ infixl 9 :@, :%
 mutual
   public export
   0 TSubst : TSubstLike
-  TSubst q d = Subst $ Elim q d
+  TSubst d = Subst $ Elim d
 
-  ||| first argument `q` is quantity type;
-  ||| second argument `d` is dimension scope size;
-  ||| third `n` is term scope size
+  ||| first argument `d` is dimension scope size;
+  ||| second `n` is term scope size
   public export
   data Term : TermLike where
     ||| type of types
-    TYPE : (l : Universe) -> Term q d n
+    TYPE : (l : Universe) -> Term d n
 
     ||| function type
-    Pi  : (qty : q) -> (arg : Term q d n) ->
-          (res : ScopeTerm q d n) -> Term q d n
+    Pi  : (qty : Qty) -> (arg : Term d n) ->
+          (res : ScopeTerm d n) -> Term d n
     ||| function term
-    Lam : (body : ScopeTerm q d n) -> Term q d n
+    Lam : (body : ScopeTerm d n) -> Term d n
 
     ||| pair type
-    Sig : (fst : Term q d n) -> (snd : ScopeTerm q d n) -> Term q d n
+    Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> Term d n
     ||| pair value
-    Pair : (fst, snd : Term q d n) -> Term q d n
+    Pair : (fst, snd : Term d n) -> Term d n
 
     ||| enumeration type
-    Enum : (cases : SortedSet TagVal) -> Term q d n
+    Enum : (cases : SortedSet TagVal) -> Term d n
     ||| enumeration value
-    Tag : (tag : TagVal) -> Term q d n
+    Tag : (tag : TagVal) -> Term d n
 
     ||| equality type
-    Eq : (ty : DScopeTerm q d n) -> (l, r : Term q d n) -> Term q d n
+    Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> Term d n
     ||| equality term
-    DLam : (body : DScopeTerm q d n) -> Term q d n
+    DLam : (body : DScopeTerm d n) -> Term d n
 
     ||| natural numbers (temporary until 𝐖 gets added)
-    Nat  : Term q d n
+    Nat  : Term d n
     -- [todo] can these be elims?
-    Zero : Term q d n
-    Succ : (p : Term q d n) -> Term q d n
+    Zero : Term d n
+    Succ : (p : Term d n) -> Term d n
 
     ||| "box" (package a value up with a certain quantity)
-    BOX : (qty : q) -> (ty : Term q d n) -> Term q d n
-    Box : (val : Term q d n) -> Term q d n
+    BOX : (qty : Qty) -> (ty : Term d n) -> Term d n
+    Box : (val : Term d n) -> Term d n
 
     ||| elimination
-    E : (e : Elim q d n) -> Term q d n
+    E : (e : Elim d n) -> Term d n
 
     ||| term closure/suspended substitution
-    CloT  : (tm : Term q d from) -> (th : Lazy (TSubst q d from to)) ->
-            Term q d to
+    CloT  : (tm : Term d from) -> (th : Lazy (TSubst d from to)) ->
+            Term d to
     ||| dimension closure/suspended substitution
-    DCloT : (tm : Term q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
-            Term q dto n
+    DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
+            Term dto n
 
   ||| first argument `d` is dimension scope size, second `n` is term scope size
   public export
   data Elim : TermLike where
     ||| free variable
-    F : (x : Name) -> Elim q d n
+    F : (x : Name) -> Elim d n
     ||| bound variable
-    B : (i : Var n) -> Elim q d n
+    B : (i : Var n) -> Elim d n
 
     ||| term application
-    (:@) : (fun : Elim q d n) -> (arg : Term q d n) -> Elim q d n
+    (:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
 
     ||| pair destruction
     |||
     ||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
     ||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
-    CasePair : (qty : q) -> (pair : Elim q d n) ->
-               (ret : ScopeTerm q d n) ->
-               (body : ScopeTermN 2 q d n) ->
-               Elim q d n
+    CasePair : (qty : Qty) -> (pair : Elim d n) ->
+               (ret : ScopeTerm d n) ->
+               (body : ScopeTermN 2 d n) ->
+               Elim d n
 
     ||| enum matching
-    CaseEnum : (qty : q) -> (tag : Elim q d n) ->
-               (ret : ScopeTerm q d n) ->
-               (arms : CaseEnumArms q d n) ->
-               Elim q d n
+    CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
+               (ret : ScopeTerm d n) ->
+               (arms : CaseEnumArms d n) ->
+               Elim d n
 
     ||| nat matching
-    CaseNat : (qty, qtyIH : q) -> (nat : Elim q d n) ->
-              (ret : ScopeTerm q d n) ->
-              (zero : Term q d n) ->
-              (succ : ScopeTermN 2 q d n) ->
-              Elim q d n
+    CaseNat : (qty, qtyIH : Qty) -> (nat : Elim d n) ->
+              (ret : ScopeTerm d n) ->
+              (zero : Term d n) ->
+              (succ : ScopeTermN 2 d n) ->
+              Elim d n
 
     ||| unboxing
-    CaseBox : (qty : q) -> (box : Elim q d n) ->
-              (ret : ScopeTerm q d n) ->
-              (body : ScopeTerm q d n) ->
-              Elim q d n
+    CaseBox : (qty : Qty) -> (box : Elim d n) ->
+              (ret : ScopeTerm d n) ->
+              (body : ScopeTerm d n) ->
+              Elim d n
 
     ||| dim application
-    (:%) : (fun : Elim q d n) -> (arg : Dim d) -> Elim q d n
+    (:%) : (fun : Elim d n) -> (arg : Dim d) -> Elim d n
 
     ||| type-annotated term
-    (:#) : (tm, ty : Term q d n) -> Elim q d n
+    (:#) : (tm, ty : Term d n) -> Elim d n
 
     ||| term closure/suspended substitution
-    CloE  : (el : Elim q d from) -> (th : Lazy (TSubst q d from to)) ->
-            Elim q d to
+    CloE  : (el : Elim d from) -> (th : Lazy (TSubst d from to)) ->
+            Elim d to
     ||| dimension closure/suspended substitution
-    DCloE : (el : Elim q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
-            Elim q dto n
+    DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
+            Elim dto n
 
   public export
   0 CaseEnumArms : TermLike
-  CaseEnumArms q d n = SortedMap TagVal (Term q d n)
+  CaseEnumArms d n = SortedMap TagVal (Term d n)
 
   ||| a scoped term with names
   public export
@@ -165,8 +163,8 @@ mutual
 
   public export
   0 ScopeTermN, DScopeTermN : Nat -> TermLike
-  ScopeTermN  s q d n = Scoped s (Term q d) n
-  DScopeTermN s q d n = Scoped s (\d => Term q d n) d
+  ScopeTermN  s d n = Scoped s (Term d) n
+  DScopeTermN s d n = Scoped s (\d => Term d n) d
 
   public export
   0 ScopeTerm, DScopeTerm : TermLike
@@ -198,58 +196,58 @@ s.name = name s
 
 ||| more convenient Pi
 public export %inline
-Pi_ : (qty : q) -> (x : BaseName) ->
-      (arg : Term q d n) -> (res : Term q d (S n)) -> Term q d n
+Pi_ : (qty : Qty) -> (x : BaseName) ->
+      (arg : Term d n) -> (res : Term d (S n)) -> Term d n
 Pi_ {qty, x, arg, res} = Pi {qty, arg, res = S [< x] $ Y res}
 
 ||| non dependent function type
 public export %inline
-Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n
+Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
 Arr {qty, arg, res} = Pi {qty, arg, res = SN res}
 
 ||| more convenient Sig
 public export %inline
-Sig_ : (x : BaseName) -> (fst : Term q d n) ->
-       (snd : Term q d (S n)) -> Term q d n
+Sig_ : (x : BaseName) -> (fst : Term d n) ->
+       (snd : Term d (S n)) -> Term d n
 Sig_ {x, fst, snd} = Sig {fst, snd = S [< x] $ Y snd}
 
 ||| non dependent pair type
 public export %inline
-And : (fst, snd : Term q d n) -> Term q d n
+And : (fst, snd : Term d n) -> Term d n
 And {fst, snd} = Sig {fst, snd = SN snd}
 
 ||| more convenient Eq
 public export %inline
-Eq_ : (i : BaseName) -> (ty : Term q (S d) n) ->
-      (l, r : Term q d n) -> Term q d n
+Eq_ : (i : BaseName) -> (ty : Term (S d) n) ->
+      (l, r : Term d n) -> Term d n
 Eq_ {i, ty, l, r} = Eq {ty = S [< i] $ Y ty, l, r}
 
 ||| non dependent equality type
 public export %inline
-Eq0 : (ty, l, r : Term q d n) -> Term q d n
+Eq0 : (ty, l, r : Term d n) -> Term d n
 Eq0 {ty, l, r} = Eq {ty = SN ty, l, r}
 
 ||| same as `F` but as a term
 public export %inline
-FT : Name -> Term q d n
+FT : Name -> Term 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 q d n
+BV : (i : Nat) -> (0 _ : LT i n) => Elim 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 q d n
+BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
 BVT i = E $ BV i
 
 public export
-makeNat : Nat -> Term q d n
+makeNat : Nat -> Term d n
 makeNat 0 = Zero
 makeNat (S k) = Succ $ makeNat k
 
 public export
-enum : List TagVal -> Term q d n
+enum : List TagVal -> Term d n
 enum = Enum . SortedSet.fromList
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index e60e348..c3c3a8c 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -54,10 +54,10 @@ prettyUniverse = hl Syntax . pretty
 
 
 public export
-data WithQty q a = MkWithQty q a
+data WithQty a = MkWithQty Qty a
 
 export
-PrettyHL q => PrettyHL a => PrettyHL (WithQty q a) where
+PrettyHL a => PrettyHL (WithQty a) where
   prettyM (MkWithQty q x) = do
     q <- pretty0M q
     x <- withPrec Arg $ prettyM x
@@ -76,9 +76,9 @@ PrettyHL a => PrettyHL (Binder a) where
 
 
 export
-prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q =>
+prettyBindType : PrettyHL a => PrettyHL b =>
                  Pretty.HasEnv m =>
-                 Maybe q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
+                 Maybe Qty -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
 prettyBindType q x s arr t = do
   bind <- case q of
     Nothing => pretty0M $ MkBinder x s
@@ -128,9 +128,9 @@ prettyArms =
   traverse (\(xs, l, r) => prettyArm T xs l r)
 
 export
-prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => IsQty q =>
-             Pretty.HasEnv m =>
-             q -> a -> BaseName -> b -> List (SnocList BaseName, Doc HL, c) ->
+prettyCase : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
+             Qty -> a -> BaseName -> b ->
+             List (SnocList BaseName, Doc HL, c) ->
              m (Doc HL)
 prettyCase pi elim r ret arms = do
   caseq <- (caseD <+>) <$> prettySuffix pi
@@ -167,20 +167,20 @@ prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
 prettyBoxVal val = bracks <$> pretty0M val
 
 export
-toNatLit : Term q d n -> Maybe Nat
+toNatLit : Term d n -> Maybe Nat
 toNatLit Zero     = Just 0
 toNatLit (Succ n) = [|S $ toNatLit n|]
 toNatLit _        = Nothing
 
 private
-eterm : Term q d n -> Exists (Term q d)
+eterm : Term d n -> Exists (Term d)
 eterm = Evidence n
 
 
 parameters (showSubsts : Bool)
  mutual
   export covering
-  [TermSubst] IsQty q => PrettyHL q => PrettyHL (Term q d n) using ElimSubst
+  [TermSubst] PrettyHL (Term d n) using ElimSubst
   where
     prettyM (TYPE l) =
       parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
@@ -198,7 +198,7 @@ parameters (showSubsts : Bool)
       t <- withPrec Times   $ prettyM t
       parensIfM Times $ asep [s <++> !timesD, t]
     prettyM (Sig s (S [< x] (Y t))) =
-      prettyBindType {q} Nothing x s !timesD t
+      prettyBindType Nothing x s !timesD t
     prettyM (Pair s t) =
       let GotPairs {init, last, _} = getPairs' [< s] t in
       prettyTuple $ toList $ init :< last
@@ -248,7 +248,7 @@ parameters (showSubsts : Bool)
         prettyM $ pushSubstsWith' th id s
 
   export covering
-  [ElimSubst] IsQty q => PrettyHL q => PrettyHL (Elim q d n) using TermSubst
+  [ElimSubst] PrettyHL (Elim d n) using TermSubst
   where
     prettyM (F x) =
       hl' Free <$> prettyM x
@@ -297,23 +297,20 @@ parameters (showSubsts : Bool)
         prettyM $ pushSubstsWith' th id e
 
   export covering
-  prettyTSubst : Pretty.HasEnv m => IsQty q => PrettyHL q =>
-                 TSubst q d from to -> m (Doc HL)
+  prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
   prettyTSubst s =
     prettySubstM (prettyM @{ElimSubst}) (!ask).tnames TVar "[" "]" s
 
 export covering %inline
-IsQty q => PrettyHL q => PrettyHL (Term q d n) where
-  prettyM = prettyM @{TermSubst False}
+PrettyHL (Term d n) where prettyM = prettyM @{TermSubst False}
 
 export covering %inline
-IsQty q => PrettyHL q => PrettyHL (Elim q d n) where
-  prettyM = prettyM @{ElimSubst False}
+PrettyHL (Elim d n) where prettyM = prettyM @{ElimSubst False}
 
 
 export covering
-prettyTerm : IsQty q => PrettyHL q => (unicode : Bool) ->
+prettyTerm : (unicode : Bool) ->
              (dnames : NContext d) -> (tnames : NContext n) ->
-             Term q d n -> Doc HL
+             Term d n -> Doc HL
 prettyTerm unicode dnames tnames term =
   pretty0With unicode (toSnocList' dnames) (toSnocList' tnames) term
diff --git a/lib/Quox/Syntax/Term/Split.idr b/lib/Quox/Syntax/Term/Split.idr
index 8126c42..36574b8 100644
--- a/lib/Quox/Syntax/Term/Split.idr
+++ b/lib/Quox/Syntax/Term/Split.idr
@@ -63,26 +63,26 @@ NotDApp = No . isDApp
 infixl 9 :@@
 ||| apply multiple arguments at once
 public export %inline
-(:@@) : Elim q d n -> List (Term q d n) -> Elim q d n
+(:@@) : Elim d n -> List (Term d n) -> Elim d n
 f :@@ ss = foldl (:@) f ss
 
 public export
-record GetArgs q d n where
+record GetArgs d n where
   constructor GotArgs
-  fun      : Elim q d n
-  args     : List (Term q d n)
+  fun      : Elim d n
+  args     : List (Term d n)
   0 notApp : NotApp fun
 
 mutual
   export %inline
-  getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
+  getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
   getArgs' fun0 args =
     let Element fun nc = pushSubsts fun0 in
     getArgsNc (assert_smaller fun0 fun) args
 
   private
-  getArgsNc : (e : Elim q d n) -> (0 nc : NotClo e) =>
-              List (Term q d n) -> GetArgs q d n
+  getArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
+              List (Term d n) -> GetArgs d n
   getArgsNc fun args = case nchoose $ isApp fun of
     Left  y => let f :@ a = fun in getArgs' f (a :: args)
     Right n => GotArgs {fun, args, notApp = n}
@@ -91,33 +91,33 @@ mutual
 ||| application then the list is just empty.
 ||| looks through substitutions for applications.
 export %inline
-getArgs : Elim q d n -> GetArgs q d n
+getArgs : Elim d n -> GetArgs d n
 getArgs e = getArgs' e []
 
 
 infixl 9 :%%
 ||| apply multiple dimension arguments at once
 public export %inline
-(:%%) : Elim q d n -> List (Dim d) -> Elim q d n
+(:%%) : Elim d n -> List (Dim d) -> Elim d n
 f :%% ss = foldl (:%) f ss
 
 public export
-record GetDArgs q d n where
+record GetDArgs d n where
   constructor GotDArgs
-  fun       : Elim q d n
+  fun       : Elim d n
   args      : List (Dim d)
   0 notDApp : NotDApp fun
 
 mutual
   export %inline
-  getDArgs' : Elim q d n -> List (Dim d) -> GetDArgs q d n
+  getDArgs' : Elim d n -> List (Dim d) -> GetDArgs d n
   getDArgs' fun0 args =
     let Element fun nc = pushSubsts fun0 in
     getDArgsNc (assert_smaller fun0 fun) args
 
   private
-  getDArgsNc : (e : Elim q d n) -> (0 nc : NotClo e) =>
-               List (Dim d) -> GetDArgs q d n
+  getDArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
+               List (Dim d) -> GetDArgs d n
   getDArgsNc fun args = case nchoose $ isDApp fun of
     Left  y => let f :% d = fun in getDArgs' f (d :: args)
     Right n => GotDArgs {fun, args, notDApp = n}
@@ -125,46 +125,46 @@ mutual
 ||| splits a dimension application into its head and arguments. if it's not an
 ||| d application then the list is just empty
 export %inline
-getDArgs : Elim q d n -> GetDArgs q d n
+getDArgs : Elim d n -> GetDArgs d n
 getDArgs e = getDArgs' e []
 
 
 infixr 1 :\\
 public export
-absN : NContext m -> Term q d (m + n) -> Term q d n
+absN : NContext m -> Term d (m + n) -> Term d n
 absN [<]       s = s
 absN (xs :< x) s = absN xs $ Lam $ SY [< x] s
 
 public export %inline
-(:\\) : NContext m -> Term q d (m + n) -> Term q d n
+(:\\) : NContext m -> Term d (m + n) -> Term d n
 (:\\) = absN
 
 
 infixr 1 :\\%
 public export
-dabsN : NContext m -> Term q (m + d) n -> Term q d n
+dabsN : NContext m -> Term (m + d) n -> Term d n
 dabsN [<]       s = s
 dabsN (xs :< x) s = dabsN xs $ DLam $ SY [< x] s
 
 public export %inline
-(:\\%) : NContext m -> Term q (m + d) n -> Term q d n
+(:\\%) : NContext m -> Term (m + d) n -> Term d n
 (:\\%) = dabsN
 
 
 public export
-record GetLams q d n where
+record GetLams d n where
   constructor GotLams
   {0 lams, rest : Nat}
   names    : NContext lams
-  body     : Term q d rest
+  body     : Term d rest
   0 eq     : lams + n = rest
   0 notLam : NotLam body
 
 mutual
   export %inline
   getLams' : forall lams, rest.
-             NContext lams -> Term q d rest -> (0 eq : lams + n = rest) ->
-             GetLams q d n
+             NContext lams -> Term d rest -> (0 eq : lams + n = rest) ->
+             GetLams d n
   getLams' xs s0 eq =
     let Element s nc = pushSubsts s0 in
     getLamsNc xs (assert_smaller s0 s) eq
@@ -172,33 +172,33 @@ mutual
   private
   getLamsNc : forall lams, rest.
               NContext lams ->
-              (t : Term q d rest) -> (0 nc : NotClo t) =>
+              (t : Term d rest) -> (0 nc : NotClo t) =>
               (0 eq : lams + n = rest) ->
-              GetLams q d n
+              GetLams d n
   getLamsNc xs s Refl = case nchoose $ isLam s of
     Left  y => let Lam (S [< x] body) = s in
                getLams' (xs :< x) (assert_smaller s body.term) Refl
     Right n => GotLams xs s Refl n
 
 export %inline
-getLams : Term q d n -> GetLams q d n
+getLams : Term d n -> GetLams d n
 getLams s = getLams' [<] s Refl
 
 
 public export
-record GetDLams q d n where
+record GetDLams d n where
   constructor GotDLams
   {0 lams, rest : Nat}
   names     : NContext lams
-  body      : Term q rest n
+  body      : Term rest n
   0 eq      : lams + d = rest
   0 notDLam : NotDLam body
 
 mutual
   export %inline
   getDLams' : forall lams, rest.
-              NContext lams -> Term q rest n -> (0 eq : lams + d = rest) ->
-              GetDLams q d n
+              NContext lams -> Term rest n -> (0 eq : lams + d = rest) ->
+              GetDLams d n
   getDLams' xs s0 eq =
     let Element s nc = pushSubsts s0 in
     getDLamsNc xs (assert_smaller s0 s) eq
@@ -206,41 +206,41 @@ mutual
   private
   getDLamsNc : forall lams, rest.
                NContext lams ->
-               (t : Term q rest n) -> (0 nc : NotClo t) =>
+               (t : Term rest n) -> (0 nc : NotClo t) =>
                (0 eq : lams + d = rest) ->
-               GetDLams q d n
+               GetDLams d n
   getDLamsNc is s Refl = case nchoose $ isDLam s of
     Left  y => let DLam (S [< i] body) = s in
                getDLams' (is :< i) (assert_smaller s body.term) Refl
     Right n => GotDLams is s Refl n
 
 export %inline
-getDLams : Term q d n -> GetDLams q d n
+getDLams : Term d n -> GetDLams d n
 getDLams s = getDLams' [<] s Refl
 
 
 public export
-record GetPairs q d n where
+record GetPairs d n where
   constructor GotPairs
-  init : SnocList $ Term q d n
-  last : Term q d n
+  init : SnocList $ Term d n
+  last : Term d n
   notPair : NotPair last
 
 mutual
   export %inline
-  getPairs' : SnocList (Term q d n) -> Term q d n -> GetPairs q d n
+  getPairs' : SnocList (Term d n) -> Term d n -> GetPairs d n
   getPairs' ss t0 =
     let Element t nc = pushSubsts t0 in getPairsNc ss (assert_smaller t0 t)
 
   private
-  getPairsNc : SnocList (Term q d n) ->
-               (t : Term q d n) -> (0 nc : NotClo t) =>
-               GetPairs q d n
+  getPairsNc : SnocList (Term d n) ->
+               (t : Term d n) -> (0 nc : NotClo t) =>
+               GetPairs d n
   getPairsNc ss t = case nchoose $ isPair t of
     Left  y => let Pair s t = t in
                getPairs' (ss :< s) t
     Right n => GotPairs ss t n
 
 export
-getPairs : Term q d n -> GetPairs q d n
+getPairs : Term d n -> GetPairs d n
 getPairs = getPairs' [<]
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 03ed211..99c4b51 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -8,7 +8,7 @@ import Data.SnocVect
 
 namespace CanDSubst
   public export
-  interface CanDSubst (0 tm : Nat -> Nat -> Type) where
+  interface CanDSubst (0 tm : TermLike) where
     (//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
 
 ||| does the minimal reasonable work:
@@ -17,14 +17,14 @@ namespace CanDSubst
 ||| - composes (lazily) with an existing top-level dim-closure
 ||| - otherwise, wraps in a new closure
 export
-CanDSubst (Term q) where
+CanDSubst Term where
   s          // Shift SZ = s
   TYPE l     // _        = TYPE l
   DCloT s ph // th       = DCloT s $ ph . th
   s          // th       = DCloT s th
 
 private
-subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
+subDArgs : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
 subDArgs (f :% d) th = subDArgs f th :% (d // th)
 subDArgs e        th = DCloE e th
 
@@ -36,7 +36,7 @@ subDArgs e        th = DCloE e th
 |||   top-level sequence of dimension applications
 ||| - otherwise, wraps in a new closure
 export
-CanDSubst (Elim q) where
+CanDSubst Elim where
   e          // Shift SZ = e
   F x        // _        = F x
   B i        // _        = B i
@@ -46,22 +46,22 @@ CanDSubst (Elim q) where
 
 namespace DSubst.ScopeTermN
   export %inline
-  (//) : ScopeTermN s q dfrom n -> Lazy (DSubst dfrom dto) ->
-         ScopeTermN s q dto n
+  (//) : ScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
+         ScopeTermN s dto n
   S ns (Y body) // th = S ns $ Y $ body // th
   S ns (N body) // th = S ns $ N $ body // th
 
 namespace DSubst.DScopeTermN
   export %inline
   (//) : {s : Nat} ->
-         DScopeTermN s q dfrom n -> Lazy (DSubst dfrom dto) ->
-         DScopeTermN s q dto n
+         DScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
+         DScopeTermN s dto n
   S ns (Y body) // th = S ns $ Y $ body // pushN s th
   S ns (N body) // th = S ns $ N $ body // th
 
 
-export %inline FromVar (Elim q d) where fromVar = B
-export %inline FromVar (Term q d) where fromVar = E . fromVar
+export %inline FromVar (Elim d) where fromVar = B
+export %inline FromVar (Term d) where fromVar = E . fromVar
 
 
 ||| does the minimal reasonable work:
@@ -71,7 +71,7 @@ export %inline FromVar (Term q d) where fromVar = E . fromVar
 ||| - immediately looks up a bound variable
 ||| - otherwise, wraps in a new closure
 export
-CanSubstSelf (Elim q d) where
+CanSubstSelf (Elim d) where
   F x       // _  = F x
   B i       // th = th !! i
   CloE e ph // th = assert_total CloE e $ ph . th
@@ -82,7 +82,7 @@ CanSubstSelf (Elim q d) where
 namespace CanTSubst
   public export
   interface CanTSubst (0 tm : TermLike) where
-    (//) : tm q d from -> Lazy (TSubst q d from to) -> tm q d to
+    (//) : tm d from -> Lazy (TSubst d from to) -> tm d to
 
 ||| does the minimal reasonable work:
 ||| - deletes the closure around an atomic constant like `TYPE`
@@ -102,135 +102,135 @@ CanTSubst Term where
 namespace ScopeTermN
   export %inline
   (//) : {s : Nat} ->
-         ScopeTermN s q d from -> Lazy (TSubst q d from to) ->
-         ScopeTermN s q d to
+         ScopeTermN s d from -> Lazy (TSubst d from to) ->
+         ScopeTermN s d to
   S ns (Y body) // th = S ns $ Y $ body // pushN s th
   S ns (N body) // th = S ns $ N $ body // th
 
 namespace DScopeTermN
   export %inline
   (//) : {s : Nat} ->
-         DScopeTermN s q d from -> Lazy (TSubst q d from to) ->
-         DScopeTermN s q d to
+         DScopeTermN s d from -> Lazy (TSubst d from to) ->
+         DScopeTermN s d to
   S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
   S ns (N body) // th = S ns $ N $ body // th
 
-export %inline CanShift (Term q d) where s // by = s // Shift by
-export %inline CanShift (Elim q d) where e // by = e // Shift by
+export %inline CanShift (Term d) where s // by = s // Shift by
+export %inline CanShift (Elim d) where e // by = e // Shift by
 
 export %inline
-{s : Nat} -> CanShift (ScopeTermN s q d) where
+{s : Nat} -> CanShift (ScopeTermN s d) where
   b // by = b // Shift by
 
 
 export %inline
-comp : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
-       TSubst q dto from to
+comp : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
+       TSubst dto from to
 comp th ps ph = map (// th) ps . ph
 
 
 public export %inline
-dweakT : {by : Nat} -> Term q d n -> Term q (by + d) n
+dweakT : {by : Nat} -> Term d n -> Term (by + d) n
 dweakT t = t // shift by
 
 public export %inline
-dweakE : {by : Nat} -> Elim q d n -> Elim q (by + d) n
+dweakE : {by : Nat} -> Elim d n -> Elim (by + d) n
 dweakE t = t // shift by
 
 
 public export %inline
-weakT : {default 1 by : Nat} -> Term q d n -> Term q d (by + n)
+weakT : {default 1 by : Nat} -> Term d n -> Term d (by + n)
 weakT t = t // shift by
 
 public export %inline
-weakE : {default 1 by : Nat} -> Elim q d n -> Elim q d (by + n)
+weakE : {default 1 by : Nat} -> Elim d n -> Elim d (by + n)
 weakE t = t // shift by
 
 
 parameters {s : Nat}
   namespace ScopeTermBody
     export %inline
-    (.term) : ScopedBody s (Term q d) n -> Term q d (s + n)
+    (.term) : ScopedBody s (Term d) n -> Term d (s + n)
     (Y b).term = b
     (N b).term = weakT b {by = s}
 
   namespace ScopeTermN
     export %inline
-    (.term) : ScopeTermN s q d n -> Term q d (s + n)
+    (.term) : ScopeTermN s d n -> Term d (s + n)
     t.term = t.body.term
 
   namespace DScopeTermBody
     export %inline
-    (.term) : ScopedBody s (\d => Term q d n) d -> Term q (s + d) n
+    (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
     (Y b).term = b
     (N b).term = dweakT b {by = s}
 
   namespace DScopeTermN
     export %inline
-    (.term) : DScopeTermN s q d n -> Term q (s + d) n
+    (.term) : DScopeTermN s d n -> Term (s + d) n
     t.term = t.body.term
 
 
 export %inline
-subN : ScopeTermN s q d n -> SnocVect s (Elim q d n) -> Term q d n
+subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
 subN (S _ (Y body)) es = body // fromSnocVect es
 subN (S _ (N body)) _  = body
 
 export %inline
-sub1 : ScopeTerm q d n -> Elim q d n -> Term q d n
+sub1 : ScopeTerm d n -> Elim d n -> Term d n
 sub1 t e = subN t [< e]
 
 export %inline
-dsubN : DScopeTermN s q d n -> SnocVect s (Dim d) -> Term q d n
+dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
 dsubN (S _ (Y body)) ps = body // fromSnocVect ps
 dsubN (S _ (N body)) _  = body
 
 export %inline
-dsub1 : DScopeTerm q d n -> Dim d -> Term q d n
+dsub1 : DScopeTerm d n -> Dim d -> Term d n
 dsub1 t p = dsubN t [< p]
 
 
 public export %inline
-(.zero) : DScopeTerm q d n -> Term q d n
+(.zero) : DScopeTerm d n -> Term d n
 body.zero = dsub1 body $ K Zero
 
 public export %inline
-(.one) : DScopeTerm q d n -> Term q d n
+(.one) : DScopeTerm d n -> Term d n
 body.one = dsub1 body $ K One
 
 
 public export
 0 CloTest : TermLike -> Type
-CloTest tm = forall q, d, n. tm q d n -> Bool
+CloTest tm = forall d, n. tm d n -> Bool
 
 interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
-  pushSubstsWith : DSubst dfrom dto -> TSubst q dto from to ->
-                   tm q dfrom from -> Subset (tm q dto to) (No . isClo)
+  pushSubstsWith : DSubst dfrom dto -> TSubst dto from to ->
+                   tm dfrom from -> Subset (tm dto to) (No . isClo)
 
 public export
-0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm q d n)
+0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
 NotClo = No . isClo
 
 public export
 0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
            PushSubsts tm isClo => TermLike
-NonClo tm q d n = Subset (tm q d n) NotClo
+NonClo tm d n = Subset (tm d n) NotClo
 
 public export %inline
 nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
-       (t : tm q d n) -> (0 nc : NotClo t) => NonClo tm q d n
+       (t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
 nclo t = Element t nc
 
 parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
   ||| if the input term has any top-level closures, push them under one layer of
   ||| syntax
   export %inline
-  pushSubsts : tm q d n -> NonClo tm q d n
+  pushSubsts : tm d n -> NonClo tm d n
   pushSubsts s = pushSubstsWith id id s
 
   export %inline
-  pushSubstsWith' : DSubst dfrom dto -> TSubst q dto from to ->
-                    tm q dfrom from -> tm q dto to
+  pushSubstsWith' : DSubst dfrom dto -> TSubst dto from to ->
+                    tm dfrom from -> tm dto to
   pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
 
 mutual
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index e5126bf..078030f 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -12,44 +12,41 @@ import Quox.EffExtra
 
 
 public export
-0 TCEff : (q : Type) -> IsQty q => List (Type -> Type)
-TCEff q = [ErrorEff q, DefsReader q]
+0 TCEff : List (Type -> Type)
+TCEff = [ErrorEff, DefsReader]
 
 public export
-0 TC : (q : Type) -> IsQty q => Type -> Type
-TC q = Eff $ TCEff q
+0 TC : Type -> Type
+TC = Eff TCEff
 
 export
-runTC : (0 _ : IsQty q) => Definitions q -> TC q a -> Either (Error q) a
+runTC : Definitions -> TC a -> Either Error a
 runTC defs = extract . runExcept . runReader defs
 
 
 export
-popQs : IsQty q => Has (ErrorEff q) fs =>
-        QOutput q s -> QOutput q (s + n) -> Eff fs (QOutput q n)
+popQs : Has ErrorEff fs => QOutput s -> QOutput (s + n) -> Eff fs (QOutput n)
 popQs [<]         qout         = pure qout
 popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
 
 export %inline
-popQ : IsQty q => Has (ErrorEff q) fs =>
-       q -> QOutput q (S n) -> Eff fs (QOutput q n)
+popQ : Has ErrorEff fs => Qty -> QOutput (S n) -> Eff fs (QOutput n)
 popQ pi = popQs [< pi]
 
 export
-lubs1 : IsQty q => List1 (QOutput q n) -> Maybe (QOutput q n)
+lubs1 : List1 (QOutput n) -> Maybe (QOutput n)
 lubs1 ([<] ::: _) = Just [<]
 lubs1 ((qs :< p) ::: pqs) =
   let (qss, ps) = unzip $ map unsnoc pqs in
   [|lubs1 (qs ::: qss) :< foldlM lub p ps|]
 
 export
-lubs : IsQty q => TyContext q d n -> List (QOutput q n) -> Maybe (QOutput q n)
+lubs : TyContext d n -> List (QOutput n) -> Maybe (QOutput n)
 lubs ctx []        = Just $ zeroFor ctx
 lubs ctx (x :: xs) = lubs1 $ x ::: xs
 
 
-parameters {auto _ : IsQty q}
- mutual
+mutual
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
   |||
   ||| `check ctx sg subj ty` checks that in the context `ctx`, the term
@@ -59,22 +56,22 @@ parameters {auto _ : IsQty q}
   ||| if the dimension context is inconsistent, then return `Nothing`, without
   ||| doing any further work.
   export covering %inline
-  check : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
-          TC q (CheckResult ctx.dctx q n)
+  check : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
+          TC (CheckResult ctx.dctx n)
   check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty
 
   ||| "Ψ | Γ ⊢₀ s ⇐ A"
   |||
   ||| `check0 ctx subj ty` checks a term (as `check`) in a zero context.
   export covering %inline
-  check0 : TyContext q d n -> Term q d n -> Term q d n -> TC q ()
+  check0 : TyContext d n -> Term d n -> Term d n -> TC ()
   check0 ctx tm ty = ignore $ check ctx szero tm ty
     -- the output will always be 𝟎 because the subject quantity is 0
 
   ||| `check`, assuming the dimension context is consistent
   export covering %inline
-  checkC : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
-           TC q (CheckResult' q n)
+  checkC : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
+           TC (CheckResult' n)
   checkC ctx sg subj ty =
     wrapErr (WhileChecking ctx sg.fst subj ty) $
       let Element subj nc = pushSubsts subj in
@@ -85,16 +82,16 @@ parameters {auto _ : IsQty q}
   ||| `checkType ctx subj ty` checks a type (in a zero context). sometimes the
   ||| universe doesn't matter, only that a term is _a_ type, so it is optional.
   export covering %inline
-  checkType : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
+  checkType : TyContext d n -> Term d n -> Maybe Universe -> TC ()
   checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l
 
   export covering %inline
-  checkTypeC : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
+  checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> TC ()
   checkTypeC ctx subj l =
     wrapErr (WhileCheckingTy ctx subj l) $ checkTypeNoWrap ctx subj l
 
   export covering %inline
-  checkTypeNoWrap : TyContext q d n -> Term q d n -> Maybe Universe -> TC q ()
+  checkTypeNoWrap : TyContext d n -> Term d n -> Maybe Universe -> TC ()
   checkTypeNoWrap ctx subj l =
     let Element subj nc = pushSubsts subj in
     checkType' ctx subj l
@@ -107,14 +104,14 @@ parameters {auto _ : IsQty q}
   ||| if the dimension context is inconsistent, then return `Nothing`, without
   ||| doing any further work.
   export covering %inline
-  infer : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
-          TC q (InferResult ctx.dctx q d n)
+  infer : (ctx : TyContext d n) -> SQty -> Elim d n ->
+          TC (InferResult ctx.dctx d n)
   infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj
 
   ||| `infer`, assuming the dimension context is consistent
   export covering %inline
-  inferC : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
-           TC q (InferResult' q d n)
+  inferC : (ctx : TyContext d n) -> SQty -> Elim d n ->
+           TC (InferResult' d n)
   inferC ctx sg subj =
     wrapErr (WhileInferring ctx sg.fst subj) $
       let Element subj nc = pushSubsts subj in
@@ -122,19 +119,19 @@ parameters {auto _ : IsQty q}
 
 
   private covering
-  toCheckType : TyContext q d n -> SQty q ->
-                (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
-                TC q (CheckResult' q n)
+  toCheckType : TyContext d n -> SQty ->
+                (subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
+                TC (CheckResult' n)
   toCheckType ctx sg t ty = do
     u <- expectTYPE !ask ctx ty
-    expectEqualQ zero sg.fst
+    expectEqualQ Zero sg.fst
     checkTypeNoWrap ctx t (Just u)
     pure $ zeroFor ctx
 
   private covering
-  check' : TyContext q d n -> SQty q ->
-           (subj : Term q d n) -> (0 nc : NotClo subj) => Term q d n ->
-           TC q (CheckResult' q n)
+  check' : TyContext d n -> SQty ->
+           (subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
+           TC (CheckResult' n)
 
   check' ctx sg t@(TYPE _) ty = toCheckType ctx sg t ty
 
@@ -211,9 +208,9 @@ parameters {auto _ : IsQty q}
     pure infres.qout
 
   private covering
-  checkType' : TyContext q d n ->
-               (subj : Term q d n) -> (0 nc : NotClo subj) =>
-               Maybe Universe -> TC q ()
+  checkType' : TyContext d n ->
+               (subj : Term d n) -> (0 nc : NotClo subj) =>
+               Maybe Universe -> TC ()
 
   checkType' ctx (TYPE k) u = do
     -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
@@ -226,7 +223,7 @@ parameters {auto _ : IsQty q}
     checkTypeC ctx arg u
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
     case res.body of
-      Y res' => checkTypeC (extendTy zero res.name arg ctx) res' u
+      Y res' => checkTypeC (extendTy Zero res.name arg ctx) res' u
       N res' => checkTypeC ctx                              res' u
     -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
 
@@ -238,7 +235,7 @@ parameters {auto _ : IsQty q}
     checkTypeC ctx fst u
     -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
     case snd.body of
-      Y snd' => checkTypeC (extendTy zero snd.name fst ctx) snd' u
+      Y snd' => checkTypeC (extendTy Zero snd.name fst ctx) snd' u
       N snd' => checkTypeC ctx                              snd' u
     -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
 
@@ -283,19 +280,19 @@ parameters {auto _ : IsQty q}
 
 
   private covering
-  infer' : TyContext q d n -> SQty q ->
-           (subj : Elim q d n) -> (0 nc : NotClo subj) =>
-           TC q (InferResult' q d n)
+  infer' : TyContext d n -> SQty ->
+           (subj : Elim d n) -> (0 nc : NotClo subj) =>
+           TC (InferResult' d n)
 
   infer' ctx sg (F x) = do
     -- if π·x : A {≔ s} in global context
     g <- lookupFree x
     -- if σ ≤ π
-    expectCompatQ sg.fst g.qty
+    expectCompatQ sg.fst g.qty.fst
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
     pure $ InfRes {type = injectT ctx g.type, qout = zeroFor ctx}
    where
-    lookupFree : Name -> TC q (Definition q)
+    lookupFree : Name -> TC Definition
     lookupFree x = lookupFree' !ask x
 
   infer' ctx sg (B i) =
@@ -303,12 +300,12 @@ parameters {auto _ : IsQty q}
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
     pure $ lookupBound sg.fst i ctx.tctx
    where
-    lookupBound : q -> Var n -> TContext q d n -> InferResult' q d n
+    lookupBound : forall n. Qty -> Var n -> TContext d n -> InferResult' d n
     lookupBound pi VZ (ctx :< ty) =
       InfRes {type = weakT ty, qout = zeroFor ctx :< pi}
     lookupBound pi (VS i) (ctx :< _) =
       let InfRes {type, qout} = lookupBound pi i ctx in
-      InfRes {type = weakT type, qout = qout :< zero}
+      InfRes {type = weakT type, qout = qout :< Zero}
 
   infer' ctx sg (fun :@ arg) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
@@ -329,7 +326,7 @@ parameters {auto _ : IsQty q}
     -- if Ψ | Γ ⊢ σ · pair ⇒ (x : A) × B ⊳ Σ₁
     pairres <- inferC ctx sg pair
     -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
-    checkTypeC (extendTy zero ret.name pairres.type ctx) ret.term Nothing
+    checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
     (tfst, tsnd) <- expectSig !ask ctx pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
@@ -350,9 +347,9 @@ parameters {auto _ : IsQty q}
     tres <- inferC ctx sg t
     ttags <- expectEnum !ask ctx tres.type
     -- if 1 ≤ π, OR there is only zero or one option
-    unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ one pi
+    unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ One pi
     -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
-    checkTypeC (extendTy zero ret.name tres.type ctx) ret.term Nothing
+    checkTypeC (extendTy Zero ret.name tres.type ctx) ret.term Nothing
     -- if for each "a ⇒ s" in arms,
     --   Ψ | Γ ⊢ σ · s ⇐ A[a ∷ {ts}/x] ⊳ Σᵢ
     -- with Σ₂ = lubs Σᵢ
@@ -371,12 +368,12 @@ parameters {auto _ : IsQty q}
 
   infer' ctx sg (CaseNat pi pi' n ret zer suc) = do
     -- if 1 ≤ π
-    expectCompatQ one pi
+    expectCompatQ One pi
     -- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
     nres <- inferC ctx sg n
     expectNat !ask ctx nres.type
     -- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
-    checkTypeC (extendTy zero ret.name Nat ctx) ret.term Nothing
+    checkTypeC (extendTy Zero ret.name Nat ctx) ret.term Nothing
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
     zerout <- checkC ctx sg zer (sub1 ret (Zero :# Nat))
     -- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
@@ -392,7 +389,7 @@ parameters {auto _ : IsQty q}
     -- then Ψ | Γ ⊢ case ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
     pure $ InfRes {
       type = sub1 ret n,
-      qout = pi * nres.qout + zerout + any * sucout
+      qout = pi * nres.qout + zerout + Any * sucout
     }
 
   infer' ctx sg (CaseBox pi box ret body) = do
@@ -400,7 +397,7 @@ parameters {auto _ : IsQty q}
     boxres <- inferC ctx sg box
     (q, ty) <- expectBOX !ask ctx boxres.type
     -- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
-    checkTypeC (extendTy zero ret.name boxres.type ctx) ret.term Nothing
+    checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
     -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
     --   with ς ≤ ρπσ
     let qpisg    = q * pi * sg.fst
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 1ae82c7..b8321c4 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -14,27 +14,26 @@ import Control.Eff
 
 
 public export
-CheckResult' : Type -> Nat -> Type
+CheckResult' : Nat -> Type
 CheckResult' = QOutput
 
 public export
-CheckResult : DimEq d -> Type -> Nat -> Type
-CheckResult eqs q n = IfConsistent eqs $ CheckResult' q n
+CheckResult : DimEq d -> Nat -> Type
+CheckResult eqs n = IfConsistent eqs $ CheckResult' n
 
 public export
-record InferResult' q d n where
+record InferResult' d n where
   constructor InfRes
-  type : Term q d n
-  qout : QOutput q n
+  type : Term d n
+  qout : QOutput n
 
 public export
 InferResult : DimEq d -> TermLike
-InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n
+InferResult eqs d n = IfConsistent eqs $ InferResult' d n
 
 
 export
-lookupFree' : Has (ErrorEff q) fs =>
-              Definitions' q g -> Name -> Eff fs (Definition' q g)
+lookupFree' : Has ErrorEff fs => Definitions -> Name -> Eff fs Definition
 lookupFree' defs x =
   case lookup x defs of
     Just d  => pure d
@@ -42,68 +41,68 @@ lookupFree' defs x =
 
 
 public export
-substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n)
+substCasePairRet : Term d n -> ScopeTerm d n -> Term d (2 + n)
 substCasePairRet dty retty =
   let arg = Pair (BVT 1) (BVT 0) :# (dty // fromNat 2) in
   retty.term // (arg ::: shift 2)
 
 public export
-substCaseSuccRet : ScopeTerm q d n -> Term q d (2 + n)
+substCaseSuccRet : ScopeTerm d n -> Term d (2 + n)
 substCaseSuccRet retty = retty.term // (Succ (BVT 1) :# Nat ::: shift 2)
 
 public export
-substCaseBoxRet : Term q d n -> ScopeTerm q d n -> Term q d (S n)
+substCaseBoxRet : Term d n -> ScopeTerm d n -> Term d (S n)
 substCaseBoxRet dty retty =
   retty.term // (Box (BVT 0) :# weakT dty ::: shift 1)
 
 
-parameters (defs : Definitions' q _) {auto _ : Has (ErrorEff q) fs}
+parameters (defs : Definitions) {auto _ : Has ErrorEff fs}
   export covering %inline
   whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError =>
-          {d, n : Nat} -> tm q d n -> Eff fs (NonRedex tm q d n defs)
+          {d, n : Nat} -> tm d n -> Eff fs (NonRedex tm d n defs)
   whnfT = either (throw . WhnfError) pure . whnf defs
 
-  parameters {d2, n : Nat} (ctx : Lazy (TyContext q d1 n))
+  parameters {d2, n : Nat} (ctx : Lazy (TyContext d1 n))
              (th : Lazy (DSubst d2 d1))
     export covering %inline
-    expectTYPE_ : Term q d2 n -> Eff fs Universe
+    expectTYPE_ : Term d2 n -> Eff fs Universe
     expectTYPE_ s = case fst !(whnfT s) of
       TYPE l => pure l
       _      => throw $ ExpectedTYPE ctx (s // th)
 
     export covering %inline
-    expectPi_ : Term q d2 n -> Eff fs (q, Term q d2 n, ScopeTerm q d2 n)
+    expectPi_ : Term d2 n -> Eff fs (Qty, Term d2 n, ScopeTerm d2 n)
     expectPi_ s = case fst !(whnfT s) of
       Pi {qty, arg, res, _} => pure (qty, arg, res)
       _                     => throw $ ExpectedPi ctx (s // th)
 
     export covering %inline
-    expectSig_ : Term q d2 n -> Eff fs (Term q d2 n, ScopeTerm q d2 n)
+    expectSig_ : Term d2 n -> Eff fs (Term d2 n, ScopeTerm d2 n)
     expectSig_ s = case fst !(whnfT s) of
       Sig {fst, snd, _} => pure (fst, snd)
       _                 => throw $ ExpectedSig ctx (s // th)
 
     export covering %inline
-    expectEnum_ : Term q d2 n -> Eff fs (SortedSet TagVal)
+    expectEnum_ : Term d2 n -> Eff fs (SortedSet TagVal)
     expectEnum_ s = case fst !(whnfT s) of
       Enum tags => pure tags
       _         => throw $ ExpectedEnum ctx (s // th)
 
     export covering %inline
-    expectEq_ : Term q d2 n ->
-                Eff fs (DScopeTerm q d2 n, Term q d2 n, Term q d2 n)
+    expectEq_ : Term d2 n ->
+                Eff fs (DScopeTerm d2 n, Term d2 n, Term d2 n)
     expectEq_ s = case fst !(whnfT s) of
       Eq {ty, l, r, _} => pure (ty, l, r)
       _                => throw $ ExpectedEq ctx (s // th)
 
     export covering %inline
-    expectNat_ : Term q d2 n -> Eff fs ()
+    expectNat_ : Term d2 n -> Eff fs ()
     expectNat_ s = case fst !(whnfT s) of
       Nat => pure ()
       _   => throw $ ExpectedNat ctx (s // th)
 
     export covering %inline
-    expectBOX_ : Term q d2 n -> Eff fs (q, Term q d2 n)
+    expectBOX_ : Term d2 n -> Eff fs (Qty, Term d2 n)
     expectBOX_ s = case fst !(whnfT s) of
       BOX q a => pure (q, a)
       _       => throw $ ExpectedBOX ctx (s // th)
@@ -111,89 +110,89 @@ parameters (defs : Definitions' q _) {auto _ : Has (ErrorEff q) fs}
 
   -- [fixme] refactor this stuff
 
-  parameters (ctx : TyContext q d n)
+  parameters (ctx : TyContext d n)
     export covering %inline
-    expectTYPE : Term q d n -> Eff fs Universe
+    expectTYPE : Term d n -> Eff fs Universe
     expectTYPE =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectTYPE_ ctx id
 
     export covering %inline
-    expectPi : Term q d n -> Eff fs (q, Term q d n, ScopeTerm q d n)
+    expectPi : Term d n -> Eff fs (Qty, Term d n, ScopeTerm d n)
     expectPi =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectPi_ ctx id
 
     export covering %inline
-    expectSig : Term q d n -> Eff fs (Term q d n, ScopeTerm q d n)
+    expectSig : Term d n -> Eff fs (Term d n, ScopeTerm d n)
     expectSig =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectSig_ ctx id
 
     export covering %inline
-    expectEnum : Term q d n -> Eff fs (SortedSet TagVal)
+    expectEnum : Term d n -> Eff fs (SortedSet TagVal)
     expectEnum =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectEnum_ ctx id
 
     export covering %inline
-    expectEq : Term q d n -> Eff fs (DScopeTerm q d n, Term q d n, Term q d n)
+    expectEq : Term d n -> Eff fs (DScopeTerm d n, Term d n, Term d n)
     expectEq =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectEq_ ctx id
 
     export covering %inline
-    expectNat : Term q d n -> Eff fs ()
+    expectNat : Term d n -> Eff fs ()
     expectNat =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectNat_ ctx id
 
     export covering %inline
-    expectBOX : Term q d n -> Eff fs (q, Term q d n)
+    expectBOX : Term d n -> Eff fs (Qty, Term d n)
     expectBOX =
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectBOX_ ctx id
 
 
-  parameters (ctx : EqContext q n)
+  parameters (ctx : EqContext n)
     export covering %inline
-    expectTYPEE : Term q 0 n -> Eff fs Universe
+    expectTYPEE : Term 0 n -> Eff fs Universe
     expectTYPEE t =
       let Val n = ctx.termLen in
       expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectPiE : Term q 0 n -> Eff fs (q, Term q 0 n, ScopeTerm q 0 n)
+    expectPiE : Term 0 n -> Eff fs (Qty, Term 0 n, ScopeTerm 0 n)
     expectPiE t =
       let Val n = ctx.termLen in
       expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectSigE : Term q 0 n -> Eff fs (Term q 0 n, ScopeTerm q 0 n)
+    expectSigE : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
     expectSigE t =
       let Val n = ctx.termLen in
       expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectEnumE : Term q 0 n -> Eff fs (SortedSet TagVal)
+    expectEnumE : Term 0 n -> Eff fs (SortedSet TagVal)
     expectEnumE t =
       let Val n = ctx.termLen in
       expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectEqE : Term q 0 n -> Eff fs (DScopeTerm q 0 n, Term q 0 n, Term q 0 n)
+    expectEqE : Term 0 n -> Eff fs (DScopeTerm 0 n, Term 0 n, Term 0 n)
     expectEqE t =
       let Val n = ctx.termLen in
       expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectNatE : Term q 0 n -> Eff fs ()
+    expectNatE : Term 0 n -> Eff fs ()
     expectNatE t =
       let Val n = ctx.termLen in
       expectNat_ (toTyContext ctx) (shift0 ctx.dimLen) t
 
     export covering %inline
-    expectBOXE : Term q 0 n -> Eff fs (q, Term q 0 n)
+    expectBOXE : Term 0 n -> Eff fs (Qty, Term 0 n)
     expectBOXE t =
       let Val n = ctx.termLen in
       expectBOX_ (toTyContext ctx) (shift0 ctx.dimLen) t
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 31c851b..45deb46 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -9,16 +9,16 @@ import public Data.Singleton
 
 
 public export
-QContext : Type -> Nat -> Type
-QContext = Context'
+QContext : Nat -> Type
+QContext = Context' Qty
 
 public export
-TContext : Type -> Nat -> Nat -> Type
-TContext q d = Context (Term q d)
+TContext : TermLike
+TContext d = Context (Term d)
 
 public export
-QOutput : Type -> Nat -> Type
-QOutput = Context'
+QOutput : Nat -> Type
+QOutput = Context' Qty
 
 public export
 DimAssign : Nat -> Type
@@ -26,39 +26,39 @@ DimAssign = Context' DimConst
 
 
 public export
-record TyContext q d n where
+record TyContext d n where
   constructor MkTyContext
   {auto dimLen  : Singleton d}
   {auto termLen : Singleton n}
   dctx   : DimEq d
   dnames : NContext d
-  tctx   : TContext q d n
+  tctx   : TContext d n
   tnames : NContext n
-  qtys   : QContext q n -- only used for printing
+  qtys   : QContext n -- only used for printing
 %name TyContext ctx
 
 
 public export
-record EqContext q n where
+record EqContext n where
   constructor MkEqContext
   {dimLen : Nat}
   {auto termLen : Singleton n}
   dassign : DimAssign dimLen -- only used for printing
   dnames  : NContext dimLen -- only used for printing
-  tctx    : TContext q 0 n
+  tctx    : TContext 0 n
   tnames  : NContext n
-  qtys    : QContext q n -- only used for printing
+  qtys    : QContext n -- only used for printing
 %name EqContext ctx
 
 
 namespace TContext
   export %inline
-  pushD : TContext q d n -> TContext q (S d) n
+  pushD : TContext d n -> TContext (S d) n
   pushD tel = map (// shift 1) tel
 
   export %inline
-  zeroFor : IsQty q => Context tm n -> QOutput q n
-  zeroFor ctx = zero <$ ctx
+  zeroFor : Context tm n -> QOutput n
+  zeroFor ctx = Zero <$ ctx
 
 private
 extendLen : Telescope a from to -> Singleton from -> Singleton to
@@ -67,17 +67,17 @@ extendLen (tel :< _) x = [|S $ extendLen tel x|]
 
 namespace TyContext
   public export %inline
-  empty : TyContext q 0 0
+  empty : TyContext 0 0
   empty =
     MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]}
 
   public export %inline
-  null : TyContext q d n -> Bool
+  null : TyContext d n -> Bool
   null ctx = null ctx.dnames && null ctx.tnames
 
   export %inline
-  extendTyN : Telescope (\n => (q, BaseName, Term q d n)) from to ->
-              TyContext q d from -> TyContext q d to
+  extendTyN : Telescope (\n => (Qty, BaseName, Term d n)) from to ->
+              TyContext d from -> TyContext d to
   extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
     let (qs, xs, ss) = unzip3 xss in
     MkTyContext {
@@ -89,12 +89,12 @@ namespace TyContext
     }
 
   export %inline
-  extendTy : q -> BaseName -> Term q d n -> TyContext q d n ->
-             TyContext q d (S n)
+  extendTy : Qty -> BaseName -> Term d n -> TyContext d n ->
+             TyContext d (S n)
   extendTy q x s = extendTyN [< (q, x, s)]
 
   export %inline
-  extendDim : BaseName -> TyContext q d n -> TyContext q (S d) n
+  extendDim : BaseName -> TyContext d n -> TyContext (S d) n
   extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) =
     MkTyContext {
       dctx   = dctx :<? Nothing,
@@ -105,33 +105,32 @@ namespace TyContext
     }
 
   export %inline
-  eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
+  eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
   eqDim p q = {dctx $= set p q, dimLen $= id, termLen $= id}
 
   export
-  injectT : TyContext q d n -> Term q 0 0 -> Term q d n
+  injectT : TyContext d n -> Term 0 0 -> Term d n
   injectT (MkTyContext {dimLen = Val d, termLen = Val n, _}) tm =
     tm // shift0 d // shift0 n
 
   export
-  injectE : TyContext q d n -> Elim q 0 0 -> Elim q d n
+  injectE : TyContext d n -> Elim 0 0 -> Elim d n
   injectE (MkTyContext {dimLen = Val d, termLen = Val n, _}) el =
     el // shift0 d // shift0 n
 
 
 namespace QOutput
-  parameters {auto _ : IsQty q}
-    export %inline
-    (+) : QOutput q n -> QOutput q n -> QOutput q n
-    (+) = zipWith (+)
+  export %inline
+  (+) : QOutput n -> QOutput n -> QOutput n
+  (+) = zipWith (+)
 
-    export %inline
-    (*) : q -> QOutput q n -> QOutput q n
-    (*) pi = map (pi *)
+  export %inline
+  (*) : Qty -> QOutput n -> QOutput n
+  (*) pi = map (pi *)
 
-    export %inline
-    zeroFor : TyContext q _ n -> QOutput q n
-    zeroFor ctx = zeroFor ctx.tctx
+  export %inline
+  zeroFor : TyContext _ n -> QOutput n
+  zeroFor ctx = zeroFor ctx.tctx
 
 
 export
@@ -140,7 +139,7 @@ makeDAssign (Shift SZ)   = [<]
 makeDAssign (K e ::: th) = makeDAssign th :< e
 
 export
-makeEqContext' : {d : Nat} -> TyContext q d n -> DSubst d 0 -> EqContext q n
+makeEqContext' : {d : Nat} -> TyContext d n -> DSubst d 0 -> EqContext n
 makeEqContext' ctx th = MkEqContext {
   termLen = ctx.termLen,
   dassign = makeDAssign th,
@@ -151,24 +150,24 @@ makeEqContext' ctx th = MkEqContext {
 }
 
 export
-makeEqContext : TyContext q d n -> DSubst d 0 -> EqContext q n
+makeEqContext : TyContext d n -> DSubst d 0 -> EqContext n
 makeEqContext ctx@(MkTyContext {dnames, _}) th =
   let (d' ** Refl) = lengthPrf0 dnames in makeEqContext' ctx th
 
 namespace EqContext
   public export %inline
-  empty : EqContext q 0
+  empty : EqContext 0
   empty = MkEqContext {
     dassign = [<], dnames = [<], tctx = [<], tnames = [<], qtys = [<]
   }
 
   public export %inline
-  null : EqContext q n -> Bool
+  null : EqContext n -> Bool
   null ctx = null ctx.dnames && null ctx.tnames
 
   export %inline
-  extendTyN : Telescope (\n => (q, BaseName, Term q 0 n)) from to ->
-              EqContext q from -> EqContext q to
+  extendTyN : Telescope (\n => (Qty, BaseName, Term 0 n)) from to ->
+              EqContext from -> EqContext to
   extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
     let (qs, xs, ss) = unzip3 xss in
     MkEqContext {
@@ -180,17 +179,17 @@ namespace EqContext
     }
 
   export %inline
-  extendTy : q -> BaseName -> Term q 0 n -> EqContext q n -> EqContext q (S n)
+  extendTy : Qty -> BaseName -> Term 0 n -> EqContext n -> EqContext (S n)
   extendTy q x s = extendTyN [< (q, x, s)]
 
   export %inline
-  extendDim : BaseName -> DimConst -> EqContext q n -> EqContext q n
+  extendDim : BaseName -> DimConst -> EqContext n -> EqContext n
   extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) =
     MkEqContext {dassign = dassign :< e, dnames = dnames :< x,
                  tctx, tnames, qtys}
 
   export
-  toTyContext : (e : EqContext q n) -> TyContext q e.dimLen n
+  toTyContext : (e : EqContext n) -> TyContext e.dimLen n
   toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
     MkTyContext {
       dctx = fromGround dassign,
@@ -199,11 +198,11 @@ namespace EqContext
     }
 
   export
-  injectT : EqContext q n -> Term q 0 0 -> Term q 0 n
+  injectT : EqContext n -> Term 0 0 -> Term 0 n
   injectT (MkEqContext {termLen = Val n, _}) tm = tm // shift0 n
 
   export
-  injectE : EqContext q n -> Elim q 0 0 -> Elim q 0 n
+  injectE : EqContext n -> Elim 0 0 -> Elim 0 n
   injectE (MkEqContext {termLen = Val n, _}) el = el // shift0 n
 
 
@@ -214,17 +213,17 @@ PrettyHL a => PrettyHL (CtxBinder a) where
   prettyM (MkCtxBinder x t) = pure $
     sep [hsep [!(pretty0M $ TV x), colonD], !(pretty0M t)]
 
-parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
+parameters (unicode : Bool)
   private
   pipeD : Doc HL
   pipeD = hl Syntax "|"
 
   export covering
   prettyTContext : NContext d ->
-                   QContext q n -> NContext n ->
-                   TContext q d n -> Doc HL
+                   QContext n -> NContext n ->
+                   TContext d n -> Doc HL
   prettyTContext ds qs xs ctx = separate comma $ toList $ go qs xs ctx where
-    go : QContext q m -> NContext m -> TContext q d m -> SnocList (Doc HL)
+    go : QContext m -> NContext m -> TContext d m -> SnocList (Doc HL)
     go [<]       [<]       [<] = [<]
     go (qs :< q) (xs :< x) (ctx :< t) =
       let bind = MkWithQty q $ MkCtxBinder x t in
@@ -232,7 +231,7 @@ parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
       runPrettyWith unicode (toSnocList' ds) (toSnocList' xs) (pretty0M bind)
 
   export covering
-  prettyTyContext : TyContext q d n -> Doc HL
+  prettyTyContext : TyContext d n -> Doc HL
   prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
     case dctx of
       C [<] => prettyTContext dnames qtys tnames tctx
@@ -240,7 +239,7 @@ parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
                     prettyTContext dnames qtys tnames tctx]
 
   export covering
-  prettyEqContext : EqContext q n -> Doc HL
+  prettyEqContext : EqContext n -> Doc HL
   prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
     case dassign of
       [<] => prettyTContext [<] qtys tnames tctx
diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr
index 634240c..14eea35 100644
--- a/lib/Quox/Typing/Error.idr
+++ b/lib/Quox/Typing/Error.idr
@@ -11,67 +11,67 @@ import Control.Eff
 
 
 public export
-data Error q
-= ExpectedTYPE (TyContext q d n) (Term q d n)
-| ExpectedPi   (TyContext q d n) (Term q d n)
-| ExpectedSig  (TyContext q d n) (Term q d n)
-| ExpectedEnum (TyContext q d n) (Term q d n)
-| ExpectedEq   (TyContext q d n) (Term q d n)
-| ExpectedNat  (TyContext q d n) (Term q d n)
-| ExpectedBOX  (TyContext q d n) (Term q d n)
+data Error
+= ExpectedTYPE (TyContext d n) (Term d n)
+| ExpectedPi   (TyContext d n) (Term d n)
+| ExpectedSig  (TyContext d n) (Term d n)
+| ExpectedEnum (TyContext d n) (Term d n)
+| ExpectedEq   (TyContext d n) (Term d n)
+| ExpectedNat  (TyContext d n) (Term d n)
+| ExpectedBOX  (TyContext d n) (Term d n)
 | BadUniverse  Universe Universe
 | TagNotIn     TagVal (SortedSet TagVal)
 | BadCaseEnum  (SortedSet TagVal) (SortedSet TagVal)
-| BadCaseQtys  (TyContext q d n) (List (QOutput q n, Term q d n))
+| BadCaseQtys  (TyContext d n) (List (QOutput n, Term d n))
 
 -- first term arg of ClashT is the type
-| ClashT  (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) (Term q 0 n)
-| ClashTy (EqContext q n) EqMode (Term q 0 n) (Term q 0 n)
-| ClashE  (EqContext q n) EqMode (Elim q 0 n) (Elim q 0 n)
+| ClashT  (EqContext n) EqMode (Term 0 n) (Term 0 n) (Term 0 n)
+| ClashTy (EqContext n) EqMode (Term 0 n) (Term 0 n)
+| ClashE  (EqContext n) EqMode (Elim 0 n) (Elim 0 n)
 | ClashU  EqMode Universe Universe
-| ClashQ  q q
+| ClashQ  Qty Qty
 | NotInScope Name
 
-| NotType (TyContext q d n) (Term q d n)
-| WrongType (EqContext q n) (Term q 0 n) (Term q 0 n)
+| NotType (TyContext d n) (Term d n)
+| WrongType (EqContext n) (Term 0 n) (Term 0 n)
 
 -- extra context
 | WhileChecking
-    (TyContext q d n) q
-    (Term q d n) -- term
-    (Term q d n) -- type
-    (Error q)
+    (TyContext d n) Qty
+    (Term d n) -- term
+    (Term d n) -- type
+    Error
 | WhileCheckingTy
-    (TyContext q d n)
-    (Term q d n)
+    (TyContext d n)
+    (Term d n)
     (Maybe Universe)
-    (Error q)
+    Error
 | WhileInferring
-    (TyContext q d n) q
-    (Elim q d n)
-    (Error q)
+    (TyContext d n) Qty
+    (Elim d n)
+    Error
 | WhileComparingT
-    (EqContext q n) EqMode
-    (Term q 0 n) -- type
-    (Term q 0 n) (Term q 0 n) -- lhs/rhs
-    (Error q)
+    (EqContext n) EqMode
+    (Term 0 n) -- type
+    (Term 0 n) (Term 0 n) -- lhs/rhs
+    Error
 | WhileComparingE
-    (EqContext q n) EqMode
-    (Elim q 0 n) (Elim q 0 n)
-    (Error q)
+    (EqContext n) EqMode
+    (Elim 0 n) (Elim 0 n)
+    Error
 
 | WhnfError WhnfError
 %name Error err
 
 public export
-ErrorEff : Type -> Type -> Type
-ErrorEff q = Except $ Error q
+ErrorEff : Type -> Type
+ErrorEff = Except Error
 
 
 ||| whether the error is surrounded in some context
 ||| (e.g. "while checking s : A, …")
 public export
-isErrorContext : Error q -> Bool
+isErrorContext : Error -> Bool
 isErrorContext (WhileChecking   {}) = True
 isErrorContext (WhileCheckingTy {}) = True
 isErrorContext (WhileInferring  {}) = True
@@ -81,8 +81,8 @@ isErrorContext _                    = False
 
 ||| remove one layer of context
 export
-peelContext : (e : Error q) -> (0 _ : So (isErrorContext e)) =>
-              (Error q -> Error q, Error q)
+peelContext : (e : Error) -> (0 _ : So (isErrorContext e)) =>
+              (Error -> Error, Error)
 peelContext (WhileChecking ctx x s t err) =
   (WhileChecking ctx x s t, err)
 peelContext (WhileCheckingTy ctx s k err) =
@@ -97,7 +97,7 @@ peelContext (WhileComparingE ctx x e f err) =
 ||| separates out all the error context layers
 ||| (e.g. "while checking s : A, …")
 export
-explodeContext : Error q -> (List (Error q -> Error q), Error q)
+explodeContext : Error -> (List (Error -> Error), Error)
 explodeContext err =
   case choose $ isErrorContext err of
     Left y =>
@@ -109,7 +109,7 @@ explodeContext err =
 ||| leaves the outermost context layer, and the innermost (up to) n, and removes
 ||| the rest if there are more than n+1 in total
 export
-trimContext : Nat -> Error q -> Error q
+trimContext : Nat -> Error -> Error
 trimContext n err =
   case explodeContext err of
     ([],      err) => err
@@ -124,14 +124,14 @@ expect : Has (Except e) fs =>
          (a -> a -> e) -> (a -> a -> Bool) -> a -> a -> Eff fs ()
 expect err cmp x y = unless (x `cmp` y) $ throw $ err x y
 
-parameters {auto _ : Has (Except $ Error q) fs}
+parameters {auto _ : Has ErrorEff fs}
   export %inline
-  expectEqualQ : Eq q => q -> q -> Eff fs ()
+  expectEqualQ : Qty -> Qty -> Eff fs ()
   expectEqualQ = expect ClashQ (==)
 
   export %inline
-  expectCompatQ : IsQty q => q -> q -> Eff fs ()
-  expectCompatQ = expect ClashQ $ \pi, rh => isYes $ pi `compat` rh
+  expectCompatQ : Qty -> Qty -> Eff fs ()
+  expectCompatQ = expect ClashQ compat
 
   export %inline
   expectModeU : EqMode -> Universe -> Universe -> Eff fs ()
@@ -155,18 +155,18 @@ isTypeInUniverse : Maybe Universe -> Doc HL
 isTypeInUniverse Nothing  = "is a type"
 isTypeInUniverse (Just k) = "is a type in universe" <++> prettyUniverse k
 
-parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
+parameters (unicode : Bool)
   private
-  termt : TyContext q d n -> Term q d n -> Doc HL
+  termt : TyContext d n -> Term d n -> Doc HL
   termt ctx = hang 4 . prettyTerm unicode ctx.dnames ctx.tnames
 
   private
-  terme : EqContext q n -> Term q 0 n -> Doc HL
+  terme : EqContext n -> Term 0 n -> Doc HL
   terme ctx = hang 4 . prettyTerm unicode [<] ctx.tnames
 
   private
-  dissectCaseQtys : TyContext q d n ->
-                    NContext n' -> List (QOutput q n', z) ->
+  dissectCaseQtys : TyContext d n ->
+                    NContext n' -> List (QOutput n', z) ->
                     List (Doc HL)
   dissectCaseQtys ctx [<]        arms = []
   dissectCaseQtys ctx (tel :< x) arms =
@@ -177,7 +177,7 @@ parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
     ("-" <++> asep [hsep [pretty0 unicode $ TV x, "is used with quantities"],
                     hseparate comma $ map (pretty0 unicode) qs]) :: tl
   where
-    allSame : List q -> Bool
+    allSame : List Qty -> Bool
     allSame []        = True
     allSame (q :: qs) = all (== q) qs
 
@@ -190,7 +190,7 @@ parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
 
   -- [todo] only show some contexts, probably
   export
-  prettyError : (showContext : Bool) -> Error q -> Doc HL
+  prettyError : (showContext : Bool) -> Error -> Doc HL
   prettyError showContext = \case
     ExpectedTYPE ctx s =>
       sep ["expected a type universe, but got", termt ctx s]
@@ -208,7 +208,7 @@ parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
       sep ["expected an equality type, but got", termt ctx s]
 
     ExpectedNat ctx s {d, n} =>
-      sep ["expected the type", pretty0 unicode $ Nat {q, d, n},
+      sep ["expected the type", pretty0 unicode $ Nat {d, n},
            "but got", termt ctx s]
 
     ExpectedBOX ctx s =>
@@ -301,13 +301,13 @@ parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
 
     WhnfError err => prettyWhnfError err
   where
-    inTContext : TyContext q d n -> Doc HL -> Doc HL
+    inTContext : TyContext d n -> Doc HL -> Doc HL
     inTContext ctx doc =
       if showContext && not (null ctx) then
         vsep [sep ["in context", prettyTyContext unicode ctx], doc]
       else doc
 
-    inEContext : EqContext q n -> Doc HL -> Doc HL
+    inEContext : EqContext n -> Doc HL -> Doc HL
     inEContext ctx doc =
       if showContext && not (null ctx) then
         vsep [sep ["in context", prettyEqContext unicode ctx], doc]
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 9d87e7b..0d73bbe 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -18,7 +18,6 @@ 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 820fa04..ae899c1 100644
--- a/tests/TermImpls.idr
+++ b/tests/TermImpls.idr
@@ -20,7 +20,7 @@ eqSubstLen _          _          = Nothing
 
 mutual
   export covering
-  Eq q => Eq (Term q d n) where
+  Eq (Term d n) where
     TYPE k == TYPE l = k == l
     TYPE _ == _ = False
 
@@ -82,7 +82,7 @@ mutual
     DCloT {} == _ = False
 
   export covering
-  Eq q => Eq (Elim q d n) where
+  Eq (Elim d n) where
     F x == F y = x == y
     F _ == _ = False
 
@@ -128,9 +128,9 @@ mutual
     DCloE {} == _ = False
 
 export covering
-IsQty q => PrettyHL q => Show (Term q d n) where
+Show (Term d n) where
   showPrec d t = showParens (d /= Open) $ prettyStr True t
 
 export covering
-IsQty q => PrettyHL q => Show (Elim q d n) where
+Show (Elim 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 54dc143..edb2eae 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -2,28 +2,24 @@ module Tests.Equal
 
 import Quox.Equal
 import Quox.Typechecker
-import Quox.Syntax.Qty.Three
 import public TypingImpls
 import TAP
 import Quox.EffExtra
 
-0 M : Type -> Type
-M = TC Three
-
-defGlobals : Definitions Three
+defGlobals : Definitions
 defGlobals = fromList
-  [("A", mkPostulate Zero $ TYPE 0),
-   ("B", mkPostulate Zero $ TYPE 0),
-   ("a", mkPostulate Any $ FT "A"),
-   ("a'", mkPostulate Any $ FT "A"),
-   ("b", mkPostulate Any $ FT "B"),
-   ("f", mkPostulate Any $ Arr One (FT "A") (FT "A")),
-   ("id", mkDef Any (Arr One (FT "A") (FT "A")) ([< "x"] :\\ BVT 0)),
-   ("eq-AB", mkPostulate Zero $ Eq0 (TYPE 0) (FT "A") (FT "B")),
-   ("two", mkDef Any Nat (Succ (Succ Zero)))]
+  [("A", mkPostulate gzero $ TYPE 0),
+   ("B", mkPostulate gzero $ TYPE 0),
+   ("a", mkPostulate gany $ FT "A"),
+   ("a'", mkPostulate gany $ FT "A"),
+   ("b", mkPostulate gany $ FT "B"),
+   ("f", mkPostulate gany $ Arr One (FT "A") (FT "A")),
+   ("id", mkDef gany (Arr One (FT "A") (FT "A")) ([< "x"] :\\ BVT 0)),
+   ("eq-AB", mkPostulate gzero $ Eq0 (TYPE 0) (FT "A") (FT "B")),
+   ("two", mkDef gany Nat (Succ (Succ Zero)))]
 
-parameters (label : String) (act : Lazy (M ()))
-           {default defGlobals globals : Definitions Three}
+parameters (label : String) (act : Lazy (TC ()))
+           {default defGlobals globals : Definitions}
   testEq : Test
   testEq = test label $ runTC globals act
 
@@ -31,29 +27,29 @@ parameters (label : String) (act : Lazy (M ()))
   testNeq = testThrows label (const True) $ runTC globals act $> "()"
 
 
-parameters (0 d : Nat) (ctx : TyContext Three d n)
-  subTD, equalTD : Term Three d n -> Term Three d n -> Term Three d n -> M ()
+parameters (0 d : Nat) (ctx : TyContext d n)
+  subTD, equalTD : Term d n -> Term d n -> Term d n -> TC ()
   subTD ty s t = Term.sub ctx ty s t
   equalTD ty s t = Term.equal ctx ty s t
-  equalTyD : Term Three d n -> Term Three d n -> M ()
+  equalTyD : Term d n -> Term d n -> TC ()
   equalTyD s t = Term.equalType ctx s t
 
-  subED, equalED : Elim Three d n -> Elim Three d n -> M ()
+  subED, equalED : Elim d n -> Elim d n -> TC ()
   subED e f = Elim.sub ctx e f
   equalED e f = Elim.equal ctx e f
 
-parameters (ctx : TyContext Three 0 n)
-  subT, equalT : Term Three 0 n -> Term Three 0 n -> Term Three 0 n -> M ()
+parameters (ctx : TyContext 0 n)
+  subT, equalT : Term 0 n -> Term 0 n -> Term 0 n -> TC ()
   subT = subTD 0 ctx
   equalT = equalTD 0 ctx
-  equalTy : Term Three 0 n -> Term Three 0 n -> M ()
+  equalTy : Term 0 n -> Term 0 n -> TC ()
   equalTy = equalTyD 0 ctx
 
-  subE, equalE : Elim Three 0 n -> Elim Three 0 n -> M ()
+  subE, equalE : Elim 0 n -> Elim 0 n -> TC ()
   subE = subED 0 ctx
   equalE = equalED 0 ctx
 
-empty01 : TyContext q 0 0
+empty01 : TyContext 0 0
 empty01 = eqDim (K Zero) (K One) empty
 
 
@@ -166,7 +162,7 @@ tests = "equality & subtyping" :- [
       let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in
       equalT empty (TYPE 2) tm tm,
     testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)"
-        {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $
+        {globals = fromList [("A", mkDef gzero (TYPE 2) (TYPE 1))]} $
       equalT empty (TYPE 2)
         (Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
         (Eq0 (FT "A") (TYPE 0) (TYPE 0)),
@@ -174,7 +170,7 @@ tests = "equality & subtyping" :- [
   ],
 
   "equalities and uip" :-
-  let refl : Term q d n -> Term q d n -> Elim q d n
+  let refl : Term d n -> Term d n -> Elim d n
       refl a x = (DLam $ S [< "_"] $ N x) :# (Eq0 a x x)
   in
   [
@@ -185,53 +181,53 @@ tests = "equality & subtyping" :- [
 
     testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q  (free)"
            {globals =
-              let def = mkPostulate Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in
+              let def = mkPostulate gzero $ Eq0 (FT "A") (FT "a") (FT "a'") in
               defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
       equalE empty (F "p") (F "q"),
 
     testEq "∥ x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x = y  (bound)" $
-      let ty : forall n. Term Three 0 n := Eq0 (FT "A") (FT "a") (FT "a'") in
+      let ty : forall n. Term 0 n := Eq0 (FT "A") (FT "a") (FT "a'") in
       equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
         (BV 0) (BV 1),
 
     testEq "∥ x : [(a ≡ a' : A) ∷ Type 0], y : [ditto] ⊢ x = y" $
-      let ty : forall n. Term Three 0 n :=
+      let ty : forall n. Term 0 n :=
             E (Eq0 (FT "A") (FT "a") (FT "a'") :# TYPE 0) in
       equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
         (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
-               ("EE", mkDef zero (TYPE 0) (FT "E"))]} $
+              [("E", mkDef gzero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
+               ("EE", mkDef gzero (TYPE 0) (FT "E"))]} $
       equalE (extendTyN [< (Any, "x", FT "EE"), (Any, "y", FT "EE")] empty)
         (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
-               ("EE", mkDef zero (TYPE 0) (FT "E"))]} $
+              [("E", mkDef gzero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
+               ("EE", mkDef gzero (TYPE 0) (FT "E"))]} $
       equalE (extendTyN [< (Any, "x", FT "EE"), (Any, "y", FT "E")] empty)
         (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
+              [("E", mkDef gzero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
       equalE (extendTyN [< (Any, "x", FT "E"), (Any, "y", FT "E")] empty)
         (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
-      let ty : forall n. Term Three 0 n :=
+              [("E", mkDef gzero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
+      let ty : forall n. Term 0 n :=
             Sig (FT "E") $ S [< "_"] $ N $ FT "E" in
       equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
         (BV 0) (BV 1),
 
     testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : W ⊢ x = y"
            {globals = defGlobals `mergeLeft` fromList
-              [("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
-               ("W", mkDef zero (TYPE 0) (FT "E" `And` FT "E"))]} $
+              [("E", mkDef gzero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
+               ("W", mkDef gzero (TYPE 0) (FT "E" `And` FT "E"))]} $
       equalE
         (extendTyN [< (Any, "x", FT "W"), (Any, "y", FT "W")] empty)
         (BV 0) (BV 1)
@@ -281,11 +277,11 @@ tests = "equality & subtyping" :- [
 
   "free var" :-
   let au_bu = fromList
-        [("A", mkDef Any (TYPE 1) (TYPE 0)),
-         ("B", mkDef Any (TYPE 1) (TYPE 0))]
+        [("A", mkDef gany (TYPE 1) (TYPE 0)),
+         ("B", mkDef gany (TYPE 1) (TYPE 0))]
       au_ba = fromList
-        [("A", mkDef Any (TYPE 1) (TYPE 0)),
-         ("B", mkDef Any (TYPE 1) (FT "A"))]
+        [("A", mkDef gany (TYPE 1) (TYPE 0)),
+         ("B", mkDef gany (TYPE 1) (FT "A"))]
   in [
     testEq "A = A" $
       equalE empty (F "A") (F "A"),
@@ -306,13 +302,13 @@ tests = "equality & subtyping" :- [
     testNeq "A ≮: B" $
       subE empty (F "A") (F "B"),
     testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
-        {globals = fromList [("A", mkDef Any (TYPE 3) (TYPE 0)),
-                             ("B", mkDef Any (TYPE 3) (TYPE 2))]} $
+        {globals = fromList [("A", mkDef gany (TYPE 3) (TYPE 0)),
+                             ("B", mkDef gany (TYPE 3) (TYPE 2))]} $
       subE empty (F "A") (F "B"),
     note "(A and B in different universes)",
     testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
-        {globals = fromList [("A", mkDef Any (TYPE 1) (TYPE 0)),
-                             ("B", mkDef Any (TYPE 3) (TYPE 2))]} $
+        {globals = fromList [("A", mkDef gany (TYPE 1) (TYPE 0)),
+                             ("B", mkDef gany (TYPE 3) (TYPE 2))]} $
       subE empty (F "A") (F "B"),
     testEq "0=1 ⊢ A <: B" $
       subE empty01 (F "A") (F "B")
diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index ddcacff..0c56a82 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -2,25 +2,24 @@ module Tests.PrettyTerm
 
 import TAP
 import Quox.Syntax
-import Quox.Syntax.Qty.Three
 import PrettyExtra
 
 
 parameters (ds : NContext d) (ns : NContext n)
-  testPrettyT : Term Three d n -> (uni, asc : String) ->
+  testPrettyT : Term d n -> (uni, asc : String) ->
                 {default uni label : String} -> Test
   testPrettyT t uni asc {label} =
     testPretty (toSnocList' ds) (toSnocList' ns) t uni asc {label}
 
-  testPrettyT1 : Term Three d n -> (str : String) ->
+  testPrettyT1 : Term d n -> (str : String) ->
                  {default str label : String} -> Test
   testPrettyT1 t str {label} = testPrettyT t str str {label}
 
-  testPrettyE : Elim Three d n -> (uni, asc : String) ->
+  testPrettyE : Elim d n -> (uni, asc : String) ->
                 {default uni label : String} -> Test
   testPrettyE e uni asc {label} = testPrettyT (E e) uni asc {label}
 
-  testPrettyE1 : Elim Three d n -> (str : String) ->
+  testPrettyE1 : Elim d n -> (str : String) ->
                  {default str label : String} -> Test
   testPrettyE1 e str {label} = testPrettyT1 (E e) str {label}
 
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index ade9237..e1e5bf7 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -1,7 +1,6 @@
 module Tests.Reduce
 
 import Quox.Syntax as Lib
-import Quox.Syntax.Qty.Three
 import Quox.Equal
 import TermImpls
 import TypingImpls
@@ -10,16 +9,16 @@ import TAP
 
 parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex err}
            {auto _ : ToInfo err}
-           {auto _ : forall d, n. Eq   (tm Three d n)}
-           {auto _ : forall d, n. Show (tm Three d n)}
-           {default empty defs : Definitions Three}
+           {auto _ : forall d, n. Eq   (tm d n)}
+           {auto _ : forall d, n. Show (tm d n)}
+           {default empty defs : Definitions}
            {default 0 d, n : Nat}
-  testWhnf : String -> tm Three d n -> tm Three d n -> Test
+  testWhnf : String -> tm d n -> tm d n -> Test
   testWhnf label from to = test "\{label}  (whnf)" $ do
     result <- bimap toInfo fst $ whnf defs from
     unless (result == to) $ Left [("exp", show to), ("got", show result)]
 
-  testNoStep : String -> tm Three d n -> Test
+  testNoStep : String -> tm d n -> Test
   testNoStep label e = testWhnf label e e
 
 
@@ -57,7 +56,7 @@ tests = "whnf" :- [
 
   "definitions" :- [
     testWhnf "a  (transparent)"
-      {defs = fromList [("a", mkDef Zero (TYPE 1) (TYPE 0))]}
+      {defs = fromList [("a", mkDef gzero (TYPE 1) (TYPE 0))]}
       (F "a") (TYPE 0 :# TYPE 1)
   ],
 
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index eb99ca8..d5b5e27 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -1,7 +1,6 @@
 module Tests.Typechecker
 
 import Quox.Syntax
-import Quox.Syntax.Qty.Three
 import Quox.Typechecker as Lib
 import public TypingImpls
 import TAP
@@ -9,9 +8,9 @@ import Quox.EffExtra
 
 
 data Error'
-  = TCError (Typing.Error Three)
-  | WrongInfer (Term Three d n) (Term Three d n)
-  | WrongQOut (QOutput Three n) (QOutput Three n)
+  = TCError Typing.Error
+  | WrongInfer (Term d n) (Term d n)
+  | WrongQOut (QOutput n) (QOutput n)
 
 export
 ToInfo Error' where
@@ -26,41 +25,41 @@ ToInfo Error' where
      ("wanted", prettyStr True bad)]
 
 0 M : Type -> Type
-M = Eff [Except Error', DefsReader Three]
+M = Eff [Except Error', DefsReader]
 
-inj : TC Three a -> M a
+inj : TC a -> M a
 inj = rethrow . mapFst TCError <=< lift . runExcept
 
 
-reflTy : IsQty q => Term q d n
+reflTy : Term d n
 reflTy =
-  Pi_ zero "A" (TYPE 0) $
-  Pi_ one  "x" (BVT 0)  $
+  Pi_ Zero "A" (TYPE 0) $
+  Pi_ One  "x" (BVT 0)  $
   Eq0 (BVT 1) (BVT 0) (BVT 0)
 
-reflDef : IsQty q => Term q d n
+reflDef : Term d n
 reflDef = [< "A","x"] :\\ [< "i"] :\\% BVT 0
 
 
-fstTy : Term Three d n
+fstTy : Term d n
 fstTy =
   (Pi_ Zero "A" (TYPE 1) $
    Pi_ Zero "B" (Arr Any (BVT 0) (TYPE 1)) $
    Arr Any (Sig_ "x" (BVT 1) $ E $ BV 1 :@ BVT 0) (BVT 1))
 
-fstDef : Term Three d n
+fstDef : Term d n
 fstDef =
   ([< "A","B","p"] :\\
     E (CasePair Any (BV 0) (SN $ BVT 2) (SY [< "x","y"] $ BVT 1)))
 
-sndTy : Term Three d n
+sndTy : Term d n
 sndTy =
   (Pi_ Zero "A" (TYPE 1) $
    Pi_ Zero "B" (Arr Any (BVT 0) (TYPE 1)) $
    Pi_ Any  "p" (Sig_ "x" (BVT 1) $ E $ BV 1 :@ BVT 0) $
    E (BV 1 :@ E (F "fst" :@@ [BVT 2, BVT 1, BVT 0])))
 
-sndDef : Term Three d n
+sndDef : Term d n
 sndDef =
   ([< "A","B","p"] :\\
     E (CasePair Any (BV 0)
@@ -68,27 +67,27 @@ sndDef =
         (SY [< "x","y"] $ BVT 0)))
 
 
-defGlobals : Definitions Three
+defGlobals : Definitions
 defGlobals = fromList
-  [("A",  mkPostulate Zero $ TYPE 0),
-   ("B",  mkPostulate Zero $ TYPE 0),
-   ("C",  mkPostulate Zero $ TYPE 1),
-   ("D",  mkPostulate Zero $ TYPE 1),
-   ("P",  mkPostulate Zero $ Arr Any (FT "A") (TYPE 0)),
-   ("a",  mkPostulate Any  $ FT "A"),
-   ("a'", mkPostulate Any  $ FT "A"),
-   ("b",  mkPostulate Any  $ FT "B"),
-   ("f",  mkPostulate Any  $ Arr One (FT "A") (FT "A")),
-   ("g",  mkPostulate Any  $ Arr One (FT "A") (FT "B")),
-   ("f2", mkPostulate Any  $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")),
-   ("p",  mkPostulate Any  $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
-   ("q",  mkPostulate Any  $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
-   ("refl", mkDef Any reflTy reflDef),
-   ("fst",  mkDef Any fstTy fstDef),
-   ("snd",  mkDef Any sndTy sndDef)]
+  [("A",  mkPostulate gzero $ TYPE 0),
+   ("B",  mkPostulate gzero $ TYPE 0),
+   ("C",  mkPostulate gzero $ TYPE 1),
+   ("D",  mkPostulate gzero $ TYPE 1),
+   ("P",  mkPostulate gzero $ Arr Any (FT "A") (TYPE 0)),
+   ("a",  mkPostulate gany  $ FT "A"),
+   ("a'", mkPostulate gany  $ FT "A"),
+   ("b",  mkPostulate gany  $ FT "B"),
+   ("f",  mkPostulate gany  $ Arr One (FT "A") (FT "A")),
+   ("g",  mkPostulate gany  $ Arr One (FT "A") (FT "B")),
+   ("f2", mkPostulate gany  $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")),
+   ("p",  mkPostulate gany  $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
+   ("q",  mkPostulate gany  $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
+   ("refl", mkDef gany reflTy reflDef),
+   ("fst",  mkDef gany fstTy fstDef),
+   ("snd",  mkDef gany sndTy sndDef)]
 
 parameters (label : String) (act : Lazy (M ()))
-           {default defGlobals globals : Definitions Three}
+           {default defGlobals globals : Definitions}
   testTC : Test
   testTC = test label {e = Error', a = ()} $
     extract $ runExcept $ runReader globals act
@@ -98,36 +97,35 @@ parameters (label : String) (act : Lazy (M ()))
     (extract $ runExcept $ runReader globals act) $> "()"
 
 
-anys : {n : Nat} -> QContext Three n
+anys : {n : Nat} -> QContext n
 anys {n = 0}   = [<]
 anys {n = S n} = anys :< Any
 
-ctx, ctx01 : {n : Nat} -> Context (\n => (BaseName, Term Three 0 n)) n ->
-             TyContext Three 0 n
+ctx, ctx01 : {n : Nat} -> Context (\n => (BaseName, Term 0 n)) n ->
+             TyContext 0 n
 ctx tel = let (ns, ts) = unzip tel in
           MkTyContext new [<] ts ns anys
 ctx01 tel = let (ns, ts) = unzip tel in
             MkTyContext ZeroIsOne [<] ts ns anys
 
-empty01 : TyContext Three 0 0
+empty01 : TyContext 0 0
 empty01 = eqDim (K Zero) (K One) empty
 
-inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
+inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> M ()
 inferredTypeEq ctx exp got =
   wrapErr (const $ WrongInfer exp got) $ inj $ equalType ctx exp got
 
-qoutEq : (exp, got : QOutput Three n) -> M ()
+qoutEq : (exp, got : QOutput n) -> M ()
 qoutEq qout res = unless (qout == res) $ throw $ WrongQOut qout res
 
-inferAs : TyContext Three d n -> (sg : SQty Three) ->
-          Elim Three d n -> Term Three d n -> M ()
+inferAs : TyContext d n -> (sg : SQty) -> Elim d n -> Term d n -> M ()
 inferAs ctx@(MkTyContext {dctx, _}) sg e ty = do
   case !(inj $ infer ctx sg e) of
     Just res => inferredTypeEq ctx ty res.type
     Nothing  => pure ()
 
-inferAsQ : TyContext Three d n -> (sg : SQty Three) ->
-           Elim Three d n -> Term Three d n -> QOutput Three n -> M ()
+inferAsQ : TyContext d n -> (sg : SQty) ->
+           Elim d n -> Term d n -> QOutput n -> M ()
 inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do
   case !(inj $ infer ctx sg e) of
     Just res => do
@@ -135,30 +133,23 @@ inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do
       qoutEq qout res.qout
     Nothing => pure ()
 
-infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
+infer_ : TyContext d n -> (sg : SQty) -> Elim d n -> M ()
 infer_ ctx sg e = ignore $ inj $ infer ctx sg e
 
-checkQ : TyContext Three d n -> SQty Three ->
-         Term Three d n -> Term Three d n -> QOutput Three n -> M ()
+checkQ : TyContext d n -> SQty ->
+         Term d n -> Term d n -> QOutput n -> M ()
 checkQ ctx@(MkTyContext {dctx, _}) sg s ty qout = do
   case !(inj $ check ctx sg s ty) of
     Just res => qoutEq qout res
     Nothing  => pure ()
 
-check_ : TyContext Three d n -> SQty Three ->
-         Term Three d n -> Term Three d n -> M ()
+check_ : TyContext d n -> SQty -> Term d n -> Term d n -> M ()
 check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty
 
-checkType_ : TyContext Three d n -> Term Three d n -> Maybe Universe -> M ()
+checkType_ : TyContext d n -> Term d n -> Maybe Universe -> M ()
 checkType_ ctx s u = inj $ checkType ctx s u
 
 
--- ω is not a subject qty
-failing "Can't find an implementation"
-  sany : SQty Three
-  sany = Element Any %search
-
-
 export
 tests : Test
 tests = "typechecker" :- [
@@ -253,9 +244,9 @@ tests = "typechecker" :- [
   "bound vars" :- [
     testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
       inferAsQ {n = 1} (ctx [< ("x", FT "A")]) sone
-        (BV 0) (FT "A") [< one],
+        (BV 0) (FT "A") [< One],
     testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
-      checkQ {n = 1} (ctx [< ("x", FT "A")]) sone (BVT 0) (FT "A") [< one],
+      checkQ {n = 1} (ctx [< ("x", FT "A")]) sone (BVT 0) (FT "A") [< One],
     note "f2 : A ⊸ A ⊸ B",
     testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ B ⊳ ω·x" $
       inferAsQ {n = 1} (ctx [< ("x", FT "A")]) sone
@@ -371,24 +362,30 @@ tests = "typechecker" :- [
   ],
 
   "equality types" :- [
-    testTC "0 · ℕ = ℕ : ★₀ ⇐ ★₁" $
+    testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ Type" $
+      checkType_ empty (Eq0 (TYPE 0) Nat Nat) Nothing,
+    testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ ★₁" $
       check_ empty szero (Eq0 (TYPE 0) Nat Nat) (TYPE 1),
-    testTC "0 · ℕ = ℕ : ★₀ ⇐ ★₂" $
+    testTCFail "1 · ℕ ≡ ℕ : ★₀ ⇍ ★₁" $
+      check_ empty sone (Eq0 (TYPE 0) Nat Nat) (TYPE 1),
+    testTC "0 · ℕ ≡ ℕ : ★₀ ⇐ ★₂" $
       check_ empty szero (Eq0 (TYPE 0) Nat Nat) (TYPE 2),
-    testTC "0 · ℕ = ℕ : ★₁ ⇐ ★₂" $
+    testTC "0 · ℕ ≡ ℕ : ★₁ ⇐ ★₂" $
       check_ empty szero (Eq0 (TYPE 1) Nat Nat) (TYPE 2),
-    testTCFail "0 · ℕ = ℕ : ★₁ ⇍ ★₁" $
+    testTCFail "0 · ℕ ≡ ℕ : ★₁ ⇍ ★₁" $
       check_ empty szero (Eq0 (TYPE 1) Nat Nat) (TYPE 1),
-    testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] x y ⇐ ★₀" $
+    testTCFail "0 ≡ 'beep : {beep} ⇍ Type" $
+      checkType_ empty (Eq0 (enum ["beep"]) Zero (Tag "beep")) Nothing,
+    testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ 0 · Eq [i ⇒ ab i] x y ⇐ ★₀" $
       check_ (ctx [< ("ab", Eq0 (TYPE 0) (FT "A") (FT "B")),
                      ("x", FT "A"), ("y", FT "B")]) szero
         (Eq (SY [< "i"] $ E $ BV 2 :% BV 0) (BVT 1) (BVT 0))
         (TYPE 0),
-    testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ ★₀" $
-      check_ (ctx [< ("ab", Eq0 (TYPE 0) (FT "A") (FT "B")),
-                     ("x", FT "A"), ("y", FT "B")]) szero
+    testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ Type" $
+      checkType_ (ctx [< ("ab", Eq0 (TYPE 0) (FT "A") (FT "B")),
+                         ("x", FT "A"), ("y", FT "B")])
         (Eq (SY [< "i"] $ E $ BV 2 :% BV 0) (BVT 0) (BVT 1))
-        (TYPE 0)
+        Nothing
   ],
 
   "equalities" :- [
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index 41044fa..04d68f7 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -10,18 +10,9 @@ import Derive.Prelude
 
 
 %runElab derive "Reduce.WhnfError" [Show]
-
-export %hint
-showTyContext : (IsQty q, PrettyHL q, Show q) => Show (TyContext q d n)
-showTyContext = deriveShow
-
-export %hint
-showEqContext : (IsQty q, PrettyHL q, Show q) => Show (EqContext q n)
-showEqContext = deriveShow
-
-export %hint
-showTypingError : (IsQty q, PrettyHL q, Show q) => Show (Error q)
-showTypingError = deriveShow
+%runElab deriveIndexed "TyContext" [Show]
+%runElab deriveIndexed "EqContext" [Show]
+%runElab derive "Error" [Show]
 
 export
 ToInfo WhnfError where
@@ -31,5 +22,4 @@ ToInfo WhnfError where
      ("list", show ts)]
 
 export
-(IsQty q, PrettyHL q) => ToInfo (Error q) where
-  toInfo err = [("err", show $ prettyError True True err)]
+ToInfo Error where toInfo err = [("err", show $ prettyError True True err)]