diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 6d65ad0..e71e9cf 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -54,14 +54,41 @@ isZero : Definition -> Bool
 isZero g = g.qty.fst == Zero
 
 
+public export
+data DefEnvTag = NS | DEFS
+
 public export
 Definitions : Type
 Definitions = SortedMap Name Definition
 
 public export
-0 DefsReader : Type -> Type
-DefsReader = Reader Definitions
+0 CurNSReader : Type -> Type
+CurNSReader = ReaderL NS Mods
 
-public export %inline
-lookupElim : {d, n : Nat} -> Name -> Definitions -> Maybe (Elim d n)
-lookupElim x defs = toElim !(lookup x defs)
+public export
+0 DefsReader : Type -> Type
+DefsReader = ReaderL DEFS Definitions
+
+export
+ns : Has CurNSReader fs => Eff fs Mods
+ns = askAt NS
+
+export
+defs : Has DefsReader fs => Eff fs Definitions
+defs = askAt DEFS
+
+
+public export
+lookupNS : Mods -> Name -> Definitions -> Maybe Definition
+lookupNS [<]           x defs = lookup x defs
+lookupNS mms@(ms :< _) x defs =
+  lookup (addMods mms x) defs <|> lookupNS ms x defs
+
+parameters {d, n : Nat}
+  public export %inline
+  lookupElim : Name -> Definitions -> Maybe (Elim d n)
+  lookupElim x defs = toElim !(lookup x defs)
+
+  public export %inline
+  lookupElimNS : Mods -> Name -> Definitions -> Maybe (Elim d n)
+  lookupElimNS mods x defs = toElim !(lookupNS mods x defs)
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 0092376..511813c 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -81,19 +81,19 @@ sameTyCon (E    {}) _         = False
 ||| * a box type is a subsingleton if its content is
 public export covering
 isSubSing : Has ErrorEff fs => {n : Nat} ->
-            Definitions -> EqContext n -> Term 0 n -> Eff fs Bool
-isSubSing defs ctx ty0 = do
-  Element ty0 nc <- whnf defs ctx ty0
+            Mods -> Definitions -> EqContext n -> Term 0 n -> Eff fs Bool
+isSubSing ns defs ctx ty0 = do
+  Element ty0 nc <- whnf ns defs ctx ty0
   case ty0 of
     TYPE _        => pure False
-    Pi _ arg res  => isSubSing defs (extendTy Zero res.name arg ctx) res.term
-    Sig  fst snd  => isSubSing defs ctx fst `andM`
-                     isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
+    Pi _ arg res  => isSubSing ns defs (extendTy Zero res.name arg ctx) res.term
+    Sig  fst snd  => isSubSing ns defs ctx fst `andM`
+                     isSubSing ns defs (extendTy Zero snd.name fst ctx) snd.term
     Enum tags     => pure $ length (SortedSet.toList tags) <= 1
     Eq   {}       => pure True
     Nat           => pure False
-    BOX  _ ty     => isSubSing defs ctx ty
-    E    (s :# _) => isSubSing defs ctx s
+    BOX  _ ty     => isSubSing ns defs ctx ty
+    E    (s :# _) => isSubSing ns defs ctx s
     E    _   => pure False
     Lam  _   => pure False
     Pair _ _ => pure False
@@ -116,14 +116,14 @@ ensureTyCon ctx t = case nchoose $ isTyConE t of
 |||
 ||| ⚠ **assumes the elim is already typechecked.** ⚠
 private covering
-computeElimTypeE : (defs : Definitions) -> EqContext n ->
-                   (e : Elim 0 n) -> (0 ne : NotRedex defs e) =>
+computeElimTypeE : (ns : Mods) -> (defs : Definitions) -> EqContext n ->
+                   (e : Elim 0 n) -> (0 ne : NotRedex ns defs e) =>
                    Equal (Term 0 n)
-computeElimTypeE defs ectx e =
+computeElimTypeE ns defs ectx e =
   let Val n = ectx.termLen in
-  rethrow $ computeElimType defs (toWhnfContext ectx) e
+  rethrow $ computeElimType ns defs (toWhnfContext ectx) e
 
-parameters (defs : Definitions)
+parameters (ns : Mods) (defs : Definitions)
   mutual
     namespace Term
       ||| `compare0 ctx ty s t` compares `s` and `t` at type `ty`, according to
@@ -135,9 +135,9 @@ parameters (defs : Definitions)
       compare0 ctx ty s t =
         wrapErr (WhileComparingT ctx !mode ty s t) $ do
           let Val n = ctx.termLen
-          Element ty nty <- whnf defs ctx ty
-          Element s  ns  <- whnf defs ctx s
-          Element t  nt  <- whnf defs ctx t
+          Element ty _ <- whnf ns defs ctx ty
+          Element s  _ <- whnf ns defs ctx s
+          Element t  _ <- whnf ns defs ctx t
           tty <- ensureTyCon ctx ty
           compare0' ctx ty s t
 
@@ -150,8 +150,8 @@ parameters (defs : Definitions)
       private covering
       compare0' : EqContext n ->
                   (ty, s, t : Term 0 n) ->
-                  (0 nty : NotRedex defs ty) => (0 tty : So (isTyConE ty)) =>
-                  (0 ns  : NotRedex defs s)  => (0 nt  : NotRedex defs t) =>
+                  (0 _ : NotRedex ns defs ty) => (0 _ : So (isTyConE ty)) =>
+                  (0 _ : NotRedex ns defs s)  => (0 _ : NotRedex ns defs t) =>
                   Equal ()
       compare0' ctx (TYPE _) s t = compareType ctx s t
 
@@ -275,19 +275,18 @@ parameters (defs : Definitions)
     compareType : EqContext n -> (s, t : Term 0 n) -> Equal ()
     compareType ctx s t = do
       let Val n = ctx.termLen
-      Element s ns <- whnf defs ctx s
-      Element t nt <- whnf defs ctx t
+      Element s _ <- whnf ns defs ctx s
+      Element t _ <- whnf ns defs ctx t
       ts <- ensureTyCon ctx s
       tt <- ensureTyCon ctx t
-      st <- either pure (const $ clashTy ctx s t) $
-            nchoose $ sameTyCon s t
+      st <- either pure (const $ clashTy ctx s t) $ nchoose $ sameTyCon s t
       compareType' ctx s t
 
     private covering
     compareType' : EqContext n -> (s, t : Term 0 n) ->
-                   (0 ns : NotRedex defs s) => (0 ts : So (isTyConE s)) =>
-                   (0 nt : NotRedex defs t) => (0 tt : So (isTyConE t)) =>
-                   (0 st : So (sameTyCon s t)) =>
+                   (0 _ : NotRedex ns defs s) => (0 _ : So (isTyConE s)) =>
+                   (0 _ : NotRedex ns defs t) => (0 _ : So (isTyConE t)) =>
+                   (0 _ : So (sameTyCon s t)) =>
                    Equal ()
     -- equality is the same as subtyping, except with the
     -- "≤" in the TYPE rule being replaced with "="
@@ -350,10 +349,10 @@ parameters (defs : Definitions)
 
     private covering
     replaceEnd : EqContext n ->
-                 (e : Elim 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
+                 (e : Elim 0 n) -> DimConst -> (0 ne : NotRedex ns defs e) ->
                  Equal (Elim 0 n)
     replaceEnd ctx e p ne = do
-      (ty, l, r) <- expectEq defs ctx !(computeElimTypeE defs ctx e)
+      (ty, l, r) <- expectEq ns defs ctx !(computeElimTypeE ns defs ctx e)
       pure $ ends l r p :# dsub1 ty (K p)
 
     namespace Elim
@@ -369,16 +368,16 @@ parameters (defs : Definitions)
       compare0 ctx e f =
         wrapErr (WhileComparingE ctx !mode e f) $ do
           let Val n = ctx.termLen
-          Element e ne <- whnf defs ctx e
-          Element f nf <- whnf defs ctx f
+          Element e ne <- whnf ns defs ctx e
+          Element f nf <- whnf ns defs ctx f
           -- [fixme] there is a better way to do this "isSubSing" stuff for sure
-          unless !(isSubSing defs ctx !(computeElimTypeE defs ctx e)) $
+          unless !(isSubSing ns defs ctx !(computeElimTypeE ns defs ctx e)) $
             compare0' ctx e f ne nf
 
       private covering
       compare0' : EqContext n ->
                   (e, f : Elim 0 n) ->
-                  (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
+                  (0 ne : NotRedex ns defs e) -> (0 nf : NotRedex ns defs f) ->
                   Equal ()
       -- replace applied equalities with the appropriate end first
       -- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
@@ -398,8 +397,8 @@ parameters (defs : Definitions)
       compare0' ctx (e :@ s) (f :@ t) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          (_, arg, _) <- expectPi defs ctx =<<
-                         computeElimTypeE defs ctx e @{noOr1 ne}
+          (_, arg, _) <- expectPi ns defs ctx =<<
+                         computeElimTypeE ns defs ctx e @{noOr1 ne}
           Term.compare0 ctx arg s t
       compare0' ctx e@(_ :@ _) f _ _ = clashE ctx e f
 
@@ -407,9 +406,9 @@ parameters (defs : Definitions)
                     (CasePair fpi f fret fbody) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
+          ety <- computeElimTypeE ns defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          (fst, snd) <- expectSig defs ctx ety
+          (fst, snd) <- expectSig ns defs ctx ety
           let [< x, y] = ebody.names
           Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
                         (substCasePairRet ety eret)
@@ -421,9 +420,9 @@ parameters (defs : Definitions)
                     (CaseEnum fpi f fret farms) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
+          ety <- computeElimTypeE ns defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          for_ !(expectEnum defs ctx ety) $ \t =>
+          for_ !(expectEnum ns defs ctx ety) $ \t =>
             compare0 ctx (sub1 eret $ Tag t :# ety)
               !(lookupArm t earms) !(lookupArm t farms)
           expectEqualQ epi fpi
@@ -438,7 +437,7 @@ parameters (defs : Definitions)
                     (CaseNat fpi fpi' f fret fzer fsuc) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
+          ety <- computeElimTypeE ns defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
           compare0 ctx (sub1 eret (Zero :# Nat)) ezer fzer
           let [< p, ih] = esuc.names
@@ -453,9 +452,9 @@ parameters (defs : Definitions)
                     (CaseBox fpi f fret fbody) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
+          ety <- computeElimTypeE ns defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          (q, ty) <- expectBOX defs ctx ety
+          (q, ty) <- expectBOX ns defs ctx ety
           compare0 (extendTy (epi * q) ebody.name ty ctx)
             (substCaseBoxRet ety eret)
             ebody.term fbody.term
@@ -481,8 +480,8 @@ parameters (defs : Definitions)
                     ne _ =
         local_ Equal $ do
           compare0 ctx ty1 ty2
-          u <- expectTYPE defs ctx =<<
-               computeElimTypeE defs ctx ty1 @{noOr1 ne}
+          u <- expectTYPE ns defs ctx =<<
+               computeElimTypeE ns defs ctx ty1 @{noOr1 ne}
           compareType ctx ret1 ret2
           compareType ctx def1 def2
           for_ allKinds $ \k =>
@@ -551,7 +550,8 @@ parameters (defs : Definitions)
         compare0 ctx (weakT 1 ret) b1.term b1.term
 
 
-parameters {auto _ : (Has DefsReader fs, Has ErrorEff fs)} (ctx : TyContext d n)
+parameters {auto _ : (Has DefsReader fs, Has CurNSReader fs, Has ErrorEff fs)}
+           (ctx : TyContext d n)
   -- [todo] only split on the dvars that are actually used anywhere in
   -- the calls to `splits`
 
@@ -559,33 +559,30 @@ parameters {auto _ : (Has DefsReader fs, Has ErrorEff fs)} (ctx : TyContext d n)
     namespace Term
       export covering
       compare : (ty, s, t : Term d n) -> Eff fs ()
-      compare ty s t = do
-        defs <- ask
+      compare ty s t =
         map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            lift $ compare0 defs ectx (ty // th) (s // th) (t // th)
+            lift $ compare0 !ns !defs ectx (ty // th) (s // th) (t // th)
 
       export covering
       compareType : (s, t : Term d n) -> Eff fs ()
-      compareType s t = do
-        defs <- ask
+      compareType s t =
         map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            lift $ compareType defs ectx (s // th) (t // th)
+            lift $ compareType !ns !defs ectx (s // th) (t // th)
 
     namespace Elim
       ||| 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 d n) -> Eff fs ()
-      compare e f = do
-        defs <- ask
+      compare e f =
         map fst $ runState @{Z} mode $
           for_ (splits ctx.dctx) $ \th =>
             let ectx = makeEqContext ctx th in
-            lift $ compare0 defs ectx (e // th) (f // th)
+            lift $ compare0 !ns !defs ectx (e // th) (f // th)
 
   namespace Term
     export covering %inline
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 34bc3ba..9ccd9d4 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -20,6 +20,8 @@ import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
 %hide Typing.Error
 %hide Lexer.Error
 %hide Parser.Error
+%hide Definition.DEFS
+%hide Definition.NS
 
 
 public export
@@ -234,9 +236,10 @@ fromPNameNS : Has (StateL NS Mods) fs => PName -> Eff fs Name
 fromPNameNS name = pure $ addMods !(getAt NS) $ fromPName name
 
 private
-injTC : (Has (StateL DEFS Definitions) fs, Has (Except Error) fs) =>
+injTC : (Has (StateL DEFS Definitions) fs, Has (StateL NS Mods) fs,
+         Has (Except Error) fs) =>
         TC a -> Eff fs a
-injTC act = rethrow $ mapFst TypeError $ runTC !(getAt DEFS) act
+injTC act = rethrow $ mapFst TypeError $ runTC !(getAt NS) !(getAt DEFS) act
 
 export covering
 fromPDef : (Has (StateL DEFS Definitions) fs,
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index abcbe76..d9499d0 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -14,35 +14,37 @@ import Data.List
 
 public export
 0 RedexTest : TermLike -> Type
-RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
+RedexTest tm = {d, n : Nat} -> Mods -> Definitions -> tm d n -> Bool
 
 public export
 interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
-  whnf : {d, n : Nat} -> (defs : Definitions) -> (ctx : WhnfContext d n) ->
-         tm d n -> Either Error (Subset (tm d n) (No . isRedex defs))
+  whnf : {d, n : Nat} -> (ns : Mods) -> (defs : Definitions) ->
+         (ctx : WhnfContext d n) ->
+         tm d n -> Either Error (Subset (tm d n) (No . isRedex ns defs))
 
 public export %inline
 whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
-        (defs : Definitions) -> WhnfContext d n -> tm d n ->
-        Either Error (tm d n)
-whnf0 defs ctx t = fst <$> whnf defs ctx t
+        (ns : Mods) -> (defs : Definitions) ->
+        WhnfContext d n -> tm d n -> Either Error (tm d n)
+whnf0 ns defs ctx t = fst <$> whnf ns defs ctx t
 
 public export
 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex =>
-                      Definitions -> Pred (tm d n)
-IsRedex  defs = So . isRedex defs
-NotRedex defs = No . isRedex defs
+                      Mods -> Definitions -> Pred (tm d n)
+IsRedex  ns defs = So . isRedex ns defs
+NotRedex ns defs = No . isRedex ns defs
 
 public export
 0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
-             Whnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
-NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
+             Whnf tm isRedex => (d, n : Nat) ->
+             (ns : Mods) -> (defs : Definitions) -> Type
+NonRedex tm d n ns defs = Subset (tm d n) (NotRedex ns defs)
 
 public export %inline
 nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) =>
-       (t : tm d n) -> (0 nr : NotRedex defs t) =>
-       NonRedex tm d n defs
+       (t : tm d n) -> (0 nr : NotRedex ns defs t) =>
+       NonRedex tm d n ns defs
 nred t = Element t nr
 
 
@@ -134,38 +136,38 @@ isK _     = False
 mutual
   public export
   isRedexE : RedexTest Elim
-  isRedexE defs (F x) {d, n} =
-    isJust $ lookupElim x defs {d, n}
-  isRedexE _ (B _) = False
-  isRedexE defs (f :@ _) =
-    isRedexE defs f || isLamHead f
-  isRedexE defs (CasePair {pair, _}) =
-    isRedexE defs pair || isPairHead pair
-  isRedexE defs (CaseEnum {tag, _}) =
-    isRedexE defs tag || isTagHead tag
-  isRedexE defs (CaseNat {nat, _}) =
-    isRedexE defs nat || isNatHead nat
-  isRedexE defs (CaseBox {box, _}) =
-    isRedexE defs box || isBoxHead box
-  isRedexE defs (f :% p) =
-    isRedexE defs f || isDLamHead f || isK p
-  isRedexE defs (t :# a) =
-    isE t || isRedexT defs t || isRedexT defs a
-  isRedexE defs (Coe {val, _}) =
-    isRedexT defs val || not (isE val)
-  isRedexE defs (Comp {ty, r, _}) =
-    isRedexT defs ty || isK r
-  isRedexE defs (TypeCase {ty, ret, _}) =
-    isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
-  isRedexE _ (CloE  {}) = True
-  isRedexE _ (DCloE {}) = True
+  isRedexE ns defs (F x) {d, n} =
+    isJust $ lookupElimNS ns x defs {d, n}
+  isRedexE _ _ (B _) = False
+  isRedexE ns defs (f :@ _) =
+    isRedexE ns defs f || isLamHead f
+  isRedexE ns defs (CasePair {pair, _}) =
+    isRedexE ns defs pair || isPairHead pair
+  isRedexE ns defs (CaseEnum {tag, _}) =
+    isRedexE ns defs tag || isTagHead tag
+  isRedexE ns defs (CaseNat {nat, _}) =
+    isRedexE ns defs nat || isNatHead nat
+  isRedexE ns defs (CaseBox {box, _}) =
+    isRedexE ns defs box || isBoxHead box
+  isRedexE ns defs (f :% p) =
+    isRedexE ns defs f || isDLamHead f || isK p
+  isRedexE ns defs (t :# a) =
+    isE t || isRedexT ns defs t || isRedexT ns defs a
+  isRedexE ns defs (Coe {val, _}) =
+    isRedexT ns defs val || not (isE val)
+  isRedexE ns defs (Comp {ty, r, _}) =
+    isRedexT ns defs ty || isK r
+  isRedexE ns defs (TypeCase {ty, ret, _}) =
+    isRedexE ns defs ty || isRedexT ns defs ret || isAnnTyCon ty
+  isRedexE _ _ (CloE  {}) = True
+  isRedexE _ _ (DCloE {}) = True
 
   public export
   isRedexT : RedexTest Term
-  isRedexT _    (CloT  {})         = True
-  isRedexT _    (DCloT {})         = True
-  isRedexT defs (E e)              = isAnn e || isRedexE defs e
-  isRedexT _    _                  = False
+  isRedexT _  _    (CloT  {}) = True
+  isRedexT _  _    (DCloT {}) = True
+  isRedexT ns defs (E e)      = isAnn e || isRedexE ns defs e
+  isRedexT _  _    _          = False
 
 
 public export
@@ -211,21 +213,23 @@ coeScoped ty p q (S names (N body)) =
 
 
 mutual
-  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
+  parameters {d, n : Nat} (ns : Mods) (defs : Definitions)
+             (ctx : WhnfContext d n)
     ||| performs the minimum work required to recompute the type of an elim.
     |||
     ||| ⚠ **assumes the elim is already typechecked.** ⚠
     export covering
-    computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
+    computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE ns defs e)) =>
                       Either Error (Term d n)
     computeElimType (F x) = do
-      let Just def = lookup x defs | Nothing => Left $ NotInScope x
+      let Just def = lookupNS ns x defs | Nothing => Left $ NotInScope x
       pure $ def.type
     computeElimType (B i) = pure $ ctx.tctx !! i
     computeElimType (f :@ s) {ne} = do
       -- can't use `expectPi` (or `expectEq` below) without making this
       -- mutual block from hell even worse lol
-      Pi {arg, res, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
+      Pi {arg, res, _} <- whnf0 ns defs ctx =<<
+                          computeElimType f {ne = noOr1 ne}
         | t => Left $ ExpectedPi ctx.names t
       pure $ sub1 res (s :# arg)
     computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair
@@ -233,7 +237,7 @@ mutual
     computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat
     computeElimType (CaseBox {box, ret, _}) = pure $ sub1 ret box
     computeElimType (f :% p) {ne} = do
-      Eq {ty, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
+      Eq {ty, _} <- whnf0 ns defs ctx =<< computeElimType f {ne = noOr1 ne}
         | t => Left $ ExpectedEq ctx.names t
       pure $ dsub1 ty p
     computeElimType (Coe {ty, q, _}) = pure $ dsub1 ty q
@@ -241,16 +245,17 @@ mutual
     computeElimType (TypeCase {ret, _}) = pure ret
     computeElimType (_ :# ty) = pure ty
 
-  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
+  parameters {d, n : Nat} (ns : Mods) (defs : Definitions)
+             (ctx : WhnfContext (S d) n)
     ||| for π.(x : A) → B, returns (A, B);
     ||| for an elim returns a pair of type-cases that will reduce to that;
     ||| for other intro forms error
     private covering
-    tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
+    tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT ns defs t)) =>
                Either Error (Term (S d) n, ScopeTerm (S d) n)
     tycasePi (Pi {arg, res, _}) = pure (arg, res)
     tycasePi (E e) {tnf} = do
-      ty <- computeElimType defs ctx e @{noOr2 tnf}
+      ty <- computeElimType ns defs ctx e @{noOr2 tnf}
       let arg  = E $ typeCase1Y e ty KPi [< "Arg", "Ret"] (BVT 1)
           res' = typeCase1Y e (Arr Zero arg ty) KPi [< "Arg", "Ret"] (BVT 0)
           res  = SY [< "Arg"] $ E $ weakE 1 res' :@ BVT 0
@@ -261,11 +266,11 @@ mutual
     ||| for an elim returns a pair of type-cases that will reduce to that;
     ||| for other intro forms error
     private covering
-    tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
+    tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT ns defs t)) =>
                 Either Error (Term (S d) n, ScopeTerm (S d) n)
     tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
     tycaseSig (E e) {tnf} = do
-      ty <- computeElimType defs ctx e @{noOr2 tnf}
+      ty <- computeElimType ns defs ctx e @{noOr2 tnf}
       let fst  = E $ typeCase1Y e ty KSig [< "Fst", "Snd"] (BVT 1)
           snd' = typeCase1Y e (Arr Zero fst ty) KSig [< "Fst", "Snd"] (BVT 0)
           snd  = SY [< "Fst"] $ E $ weakE 1 snd' :@ BVT 0
@@ -276,11 +281,11 @@ mutual
     ||| for an elim returns a type-case that will reduce to that;
     ||| for other intro forms error
     private covering
-    tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
+    tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT ns defs t)) =>
                 Either Error (Term (S d) n)
     tycaseBOX (BOX _ a) = pure a
     tycaseBOX (E e) {tnf} = do
-      ty <- computeElimType defs ctx e @{noOr2 tnf}
+      ty <- computeElimType ns defs ctx e @{noOr2 tnf}
       pure $ E $ typeCase1Y e ty KBOX [< "Ty"] (BVT 0)
     tycaseBOX t = Left $ ExpectedBOX ctx.names t
 
@@ -288,12 +293,12 @@ mutual
     ||| for an elim returns five type-cases that will reduce to that;
     ||| for other intro forms error
     private covering
-    tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
+    tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT ns defs t)) =>
                Either Error (Term (S d) n, Term (S d) n, DScopeTerm (S d) n,
                              Term (S d) n, Term (S d) n)
     tycaseEq (Eq {ty, l, r}) = pure (ty.zero, ty.one, ty, l, r)
     tycaseEq (E e) {tnf} = do
-      ty <- computeElimType defs ctx e @{noOr2 tnf}
+      ty <- computeElimType ns defs ctx e @{noOr2 tnf}
       let names = [< "A0", "A1", "A", "L", "R"]
           a0 = E $ typeCase1Y e ty KEq names (BVT 4)
           a1 = E $ typeCase1Y e ty KEq names (BVT 3)
@@ -304,12 +309,14 @@ mutual
       pure (a0, a1, a, l, r)
     tycaseEq t = Left $ ExpectedEq ctx.names t
 
-
-  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
+  -- new block because the functions below might pass a different ctx
+  -- into the ones above
+  parameters {d, n : Nat} (ns : Mods) (defs : Definitions)
+             (ctx : WhnfContext d n)
     ||| reduce a function application `Coe ty p q val :@ s`
     private covering
     piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val, s : Term d n) ->
-            Either Error (Subset (Elim d n) (No . isRedexE defs))
+            Either Error (Subset (Elim d n) (No . isRedexE ns defs))
     piCoe sty@(S [< i] ty) p q val s = do
       -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
       -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
@@ -317,20 +324,20 @@ mutual
       --
       -- type-case is used to expose A,B if the type is neutral
       let ctx1 = extendDim i ctx
-      Element ty tynf <- whnf defs ctx1 ty.term
-      (arg, res) <- tycasePi defs ctx1 ty
+      Element ty tynf <- whnf ns defs ctx1 ty.term
+      (arg, res) <- tycasePi ns defs ctx1 ty
       let s0   = CoeT i arg q p s
           body = E $ (val :# (ty // one p)) :@ E s0
           s1   = CoeT i (arg // (BV 0 ::: shift 2)) (weakD 1 q) (BV 0)
                       (s // shift 1)
-      whnf defs ctx $ CoeT i (sub1 res s1) p q body
+      whnf ns defs ctx $ CoeT i (sub1 res s1) p q body
 
     ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body`
     private covering
     sigCoe : (qty : Qty) ->
              (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
              (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) ->
-             Either Error (Subset (Elim d n) (No . isRedexE defs))
+             Either Error (Subset (Elim d n) (No . isRedexE ns defs))
     sigCoe qty sty@(S [< i] ty) p q val ret body = do
       -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
       -- ⇝
@@ -341,101 +348,101 @@ mutual
       --
       -- type-case is used to expose A,B if the type is neutral
       let ctx1 = extendDim i ctx
-      Element ty tynf <- whnf defs ctx1 ty.term
-      (tfst, tsnd) <- tycaseSig defs ctx1 ty
+      Element ty tynf <- whnf ns defs ctx1 ty.term
+      (tfst, tsnd) <- tycaseSig ns defs ctx1 ty
       let a' = CoeT i (weakT 2 tfst) p q (BVT 1)
           tsnd' = tsnd.term //
             (CoeT i (weakT 2 $ tfst // (BV 0 ::: shift 2))
               (weakD 1 p) (BV 0) (BVT 1) ::: shift 2)
           b' = CoeT i tsnd' p q (BVT 0)
-      whnf defs ctx $ CasePair qty (val :# (ty // one p)) ret $
+      whnf ns defs ctx $ CasePair qty (val :# (ty // one p)) ret $
         ST body.names $ body.term // (a' ::: b' ::: shift 2)
 
     ||| reduce a dimension application `Coe ty p q val :% r`
     private covering
     eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
             (r : Dim d) ->
-            Either Error (Subset (Elim d n) (No . isRedexE defs))
+            Either Error (Subset (Elim d n) (No . isRedexE ns defs))
     eqCoe sty@(S [< j] ty) p q val r = do
       -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
       -- ⇝
       -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
       --   { (r=0) j ⇒ L; (r=1) j ⇒ R }
       let ctx1 = extendDim j ctx
-      Element ty tynf <- whnf defs ctx1 ty.term
-      (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
+      Element ty tynf <- whnf ns defs ctx1 ty.term
+      (a0, a1, a, s, t) <- tycaseEq ns defs ctx1 ty
       let a'   = dsub1 a (weakD 1 r)
           val' = E $ (val :# (ty // one p)) :% r
-      whnf defs ctx $ CompH j a' p q val' r j s j t
+      whnf ns defs ctx $ CompH j a' p q val' r j s j t
 
     ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
     private covering
     boxCoe : (qty : Qty) ->
              (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
              (ret : ScopeTerm d n) -> (body : ScopeTerm d n) ->
-             Either Error (Subset (Elim d n) (No . isRedexE defs))
+             Either Error (Subset (Elim d n) (No . isRedexE ns defs))
     boxCoe qty sty@(S [< i] ty) p q val ret body = do
       -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
       -- ⇝
       -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C
       -- of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
       let ctx1 = extendDim i ctx
-      Element ty tynf <- whnf defs ctx1 ty.term
-      ta <- tycaseBOX defs ctx1 ty
+      Element ty tynf <- whnf ns defs ctx1 ty.term
+      ta <- tycaseBOX ns defs ctx1 ty
       let a' = CoeT i (weakT 1 ta) p q $ BVT 0
-      whnf defs ctx $ CaseBox qty (val :# (ty // one p)) ret $
+      whnf ns defs ctx $ CaseBox qty (val :# (ty // one p)) ret $
         ST body.names $ body.term // (a' ::: shift 1)
 
 
   export covering
   Whnf Elim Reduce.isRedexE where
-    whnf defs ctx (F x) with (lookupElim x defs) proof eq
-      _ | Just y  = whnf defs ctx y
+    whnf ns defs ctx (F x) with (lookupElimNS ns x defs) proof eq
+      _ | Just y  = whnf ns defs ctx y
       _ | Nothing = pure $ Element (F x) $ rewrite eq in Ah
 
-    whnf _ _ (B i) = pure $ nred $ B i
+    whnf _ _ _ (B i) = pure $ nred $ B i
 
     -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
-    whnf defs ctx (f :@ s) = do
-      Element f fnf <- whnf defs ctx f
+    whnf ns defs ctx (f :@ s) = do
+      Element f fnf <- whnf ns defs ctx f
       case nchoose $ isLamHead f of
         Left _ => case f of
           Lam body :# Pi {arg, res, _} =>
             let s = s :# arg in
-            whnf defs ctx $ sub1 body s :# sub1 res s
-          Coe ty p q val => piCoe defs ctx ty p q val s
+            whnf ns defs ctx $ sub1 body s :# sub1 res s
+          Coe ty p q val => piCoe ns defs ctx ty p q val s
         Right nlh => pure $ Element (f :@ s) $ fnf `orNo` nlh
 
     -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
     -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
-    whnf defs ctx (CasePair pi pair ret body) = do
-      Element pair pairnf <- whnf defs ctx pair
+    whnf ns defs ctx (CasePair pi pair ret body) = do
+      Element pair pairnf <- whnf ns defs ctx pair
       case nchoose $ isPairHead pair of
         Left _ => case pair of
           Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} =>
             let fst = fst :# tfst
                 snd = snd :# sub1 tsnd fst
             in
-            whnf defs ctx $ subN body [< fst, snd] :# sub1 ret pair
+            whnf ns defs ctx $ subN body [< fst, snd] :# sub1 ret pair
           Coe ty p q val => do
-            sigCoe defs ctx pi ty p q val ret body
+            sigCoe ns defs ctx pi ty p q val ret body
         Right np =>
           pure $ Element (CasePair pi pair ret body) $ pairnf `orNo` np
 
     -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
     -- u ∷ C['a∷{a,…}/p]
-    whnf defs ctx (CaseEnum pi tag ret arms) = do
-      Element tag tagnf <- whnf defs ctx tag
+    whnf ns defs ctx (CaseEnum pi tag ret arms) = do
+      Element tag tagnf <- whnf ns defs ctx tag
       case nchoose $ isTagHead tag of
         Left t => case tag of
           Tag t :# Enum ts =>
             let ty = sub1 ret tag in
             case lookup t arms of
-              Just arm => whnf defs ctx $ arm :# ty
+              Just arm => whnf ns defs ctx $ arm :# ty
               Nothing  => Left $ MissingEnumArm t (keys arms)
           Coe ty p q val =>
             -- there is nowhere an equality can be hiding inside an Enum
-            whnf defs ctx $ CaseEnum pi (val :# dsub1 ty q) ret arms
+            whnf ns defs ctx $ CaseEnum pi (val :# dsub1 ty q) ret arms
         Right nt =>
           pure $ Element (CaseEnum pi tag ret arms) $ tagnf `orNo` nt
 
@@ -444,35 +451,35 @@ mutual
     --
     -- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
     --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
-    whnf defs ctx (CaseNat pi piIH nat ret zer suc) = do
-      Element nat natnf <- whnf defs ctx nat
+    whnf ns defs ctx (CaseNat pi piIH nat ret zer suc) = do
+      Element nat natnf <- whnf ns defs ctx nat
       case nchoose $ isNatHead nat of
         Left _ =>
           let ty = sub1 ret nat in
           case nat of
-            Zero :# Nat => whnf defs ctx (zer :# ty)
+            Zero :# Nat => whnf ns defs ctx (zer :# ty)
             Succ n :# Nat =>
               let nn = n :# Nat
                   tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc]
               in
-              whnf defs ctx $ tm :# ty
+              whnf ns defs ctx $ tm :# ty
             Coe ty p q val =>
               -- same deal as Enum
-              whnf defs ctx $ CaseNat pi piIH (val :# dsub1 ty q) ret zer suc
+              whnf ns defs ctx $ CaseNat pi piIH (val :# dsub1 ty q) ret zer suc
         Right nn =>
           pure $ Element (CaseNat pi piIH nat ret zer suc) $ natnf `orNo` nn
 
     -- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
     --   u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
-    whnf defs ctx (CaseBox pi box ret body) = do
-      Element box boxnf <- whnf defs ctx box
+    whnf ns defs ctx (CaseBox pi box ret body) = do
+      Element box boxnf <- whnf ns defs ctx box
       case nchoose $ isBoxHead box of
         Left _ => case box of
           Box val :# BOX q bty =>
             let ty = sub1 ret box in
-            whnf defs ctx $ sub1 body (val :# bty) :# ty
+            whnf ns defs ctx $ sub1 body (val :# bty) :# ty
           Coe ty p q val =>
-            boxCoe defs ctx pi ty p q val ret body
+            boxCoe ns defs ctx pi ty p q val ret body
         Right nb =>
           pure $ Element (CaseBox pi box ret body) $ boxnf `orNo` nb
 
@@ -480,102 +487,104 @@ mutual
     -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @1 ⇝ u ∷ A‹1/𝑗›
     -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
     --   (if 𝑘 is a variable)
-    whnf defs ctx (f :% p) = do
-      Element f fnf <- whnf defs ctx f
+    whnf ns defs ctx (f :% p) = do
+      Element f fnf <- whnf ns defs ctx f
       case nchoose $ isDLamHead f of
         Left _ => case f of
           DLam body :# Eq {ty = ty, l, r, _} =>
             let body = endsOr l r (dsub1 body p) p in
-            whnf defs ctx $ body :# dsub1 ty p
+            whnf ns defs ctx $ body :# dsub1 ty p
           Coe ty p' q' val =>
-            eqCoe defs ctx ty p' q' val p
+            eqCoe ns defs ctx ty p' q' val p
         Right ndlh => case p of
           K e => do
-            Eq {l, r, ty, _} <- whnf0 defs ctx =<< computeElimType defs ctx f
+            Eq {l, r, ty, _} <- whnf0 ns defs ctx =<<
+                                computeElimType ns defs ctx f
               | ty => Left $ ExpectedEq ctx.names ty
-            whnf defs ctx $ ends (l :# ty.zero) (r :# ty.one) e
+            whnf ns defs ctx $ ends (l :# ty.zero) (r :# ty.one) e
           B _ => pure $ Element (f :% p) $ fnf `orNo` ndlh `orNo` Ah
 
     -- e ∷ A ⇝ e
-    whnf defs ctx (s :# a) = do
-      Element s snf <- whnf defs ctx s
+    whnf ns defs ctx (s :# a) = do
+      Element s snf <- whnf ns defs ctx s
       case nchoose $ isE s of
         Left  _  => let E e = s in pure $ Element e $ noOr2 snf
         Right ne => do
-          Element a anf <- whnf defs ctx a
+          Element a anf <- whnf ns defs ctx a
           pure $ Element (s :# a) $ ne `orNo` snf `orNo` anf
 
-    whnf defs ctx (Coe (S _ (N ty)) _ _ val) =
-      whnf defs ctx $ val :# ty
-    whnf defs ctx (Coe (S [< i] ty) p q val) = do
-      Element ty  tynf  <- whnf defs (extendDim i ctx) ty.term
-      Element val valnf <- whnf defs ctx val
-      pushCoe defs ctx i ty p q val
+    whnf ns defs ctx (Coe (S _ (N ty)) _ _ val) =
+      whnf ns defs ctx $ val :# ty
+    whnf ns defs ctx (Coe (S [< i] ty) p q val) = do
+      Element ty  tynf  <- whnf ns defs (extendDim i ctx) ty.term
+      Element val valnf <- whnf ns defs ctx val
+      pushCoe ns defs ctx i ty p q val
 
-    whnf defs ctx (Comp ty p q val r zero one) =
+    whnf ns defs ctx (Comp ty p q val r zero one) =
       -- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
-      if p == q then whnf defs ctx $ val :# ty else
+      if p == q then whnf ns defs ctx $ val :# ty else
       case nchoose (isK r) of
         -- comp [A] @p @q s { (0=0) j ⇒ t; ⋯ } ⇝ t‹q/j› ∷ A
         -- comp [A] @p @q s { (1=1) j ⇒ t; ⋯ } ⇝ t‹q/j› ∷ A
         Left y => case r of
-          K Zero => whnf defs ctx $ dsub1 zero q :# ty
-          K One  => whnf defs ctx $ dsub1 one  q :# ty
+          K Zero => whnf ns defs ctx $ dsub1 zero q :# ty
+          K One  => whnf ns defs ctx $ dsub1 one  q :# ty
         Right nk => do
-          Element ty tynf <- whnf defs ctx ty
+          Element ty tynf <- whnf ns defs ctx ty
           pure $ Element (Comp ty p q val r zero one) $ tynf `orNo` nk
       -- [todo] anything other than just the boundaries??
 
-    whnf defs ctx (TypeCase ty ret arms def) = do
-      Element ty  tynf  <- whnf defs ctx ty
-      Element ret retnf <- whnf defs ctx ret
+    whnf ns defs ctx (TypeCase ty ret arms def) = do
+      Element ty  tynf  <- whnf ns defs ctx ty
+      Element ret retnf <- whnf ns defs ctx ret
       case nchoose $ isAnnTyCon ty of
         Left  y  => let ty :# TYPE u = ty in
-                    reduceTypeCase defs ctx ty u ret arms def
+                    reduceTypeCase ns defs ctx ty u ret arms def
         Right nt => pure $ Element (TypeCase ty ret arms def) $
                              tynf `orNo` retnf `orNo` nt
 
-    whnf defs ctx (CloE  el th) = whnf defs ctx $ pushSubstsWith' id th el
-    whnf defs ctx (DCloE el th) = whnf defs ctx $ pushSubstsWith' th id el
+    whnf ns defs ctx (CloE  el th) = whnf ns defs ctx $ pushSubstsWith' id th el
+    whnf ns defs ctx (DCloE el th) = whnf ns defs ctx $ pushSubstsWith' th id el
 
   export covering
   Whnf Term Reduce.isRedexT where
-    whnf _ _ t@(TYPE {}) = pure $ nred t
-    whnf _ _ t@(Pi   {}) = pure $ nred t
-    whnf _ _ t@(Lam  {}) = pure $ nred t
-    whnf _ _ t@(Sig  {}) = pure $ nred t
-    whnf _ _ t@(Pair {}) = pure $ nred t
-    whnf _ _ t@(Enum {}) = pure $ nred t
-    whnf _ _ t@(Tag  {}) = pure $ nred t
-    whnf _ _ t@(Eq   {}) = pure $ nred t
-    whnf _ _ t@(DLam {}) = pure $ nred t
-    whnf _ _    Nat      = pure $ nred Nat
-    whnf _ _    Zero     = pure $ nred Zero
-    whnf _ _ t@(Succ {}) = pure $ nred t
-    whnf _ _ t@(BOX  {}) = pure $ nred t
-    whnf _ _ t@(Box  {}) = pure $ nred t
+    whnf _ _ _ t@(TYPE {}) = pure $ nred t
+    whnf _ _ _ t@(Pi   {}) = pure $ nred t
+    whnf _ _ _ t@(Lam  {}) = pure $ nred t
+    whnf _ _ _ t@(Sig  {}) = pure $ nred t
+    whnf _ _ _ t@(Pair {}) = pure $ nred t
+    whnf _ _ _ t@(Enum {}) = pure $ nred t
+    whnf _ _ _ t@(Tag  {}) = pure $ nred t
+    whnf _ _ _ t@(Eq   {}) = pure $ nred t
+    whnf _ _ _ t@(DLam {}) = pure $ nred t
+    whnf _ _ _    Nat      = pure $ nred Nat
+    whnf _ _ _    Zero     = pure $ nred Zero
+    whnf _ _ _ t@(Succ {}) = pure $ nred t
+    whnf _ _ _ t@(BOX  {}) = pure $ nred t
+    whnf _ _ _ t@(Box  {}) = pure $ nred t
 
     -- s ∷ A ⇝ s   (in term context)
-    whnf defs ctx (E e) = do
-      Element e enf <- whnf defs ctx e
+    whnf ns defs ctx (E e) = do
+      Element e enf <- whnf ns defs ctx e
       case nchoose $ isAnn e of
         Left  _  => let tm :# _ = e in pure $ Element tm $ noOr1 $ noOr2 enf
         Right na => pure $ Element (E e) $ na `orNo` enf
 
-    whnf defs ctx (CloT  tm th) = whnf defs ctx $ pushSubstsWith' id th tm
-    whnf defs ctx (DCloT tm th) = whnf defs ctx $ pushSubstsWith' th id tm
+    whnf ns defs ctx (CloT  tm th) = whnf ns defs ctx $ pushSubstsWith' id th tm
+    whnf ns defs ctx (DCloT tm th) = whnf ns defs ctx $ pushSubstsWith' th id tm
 
   ||| reduce a type-case applied to a type constructor
   private covering
-  reduceTypeCase : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
+  reduceTypeCase : {d, n : Nat} -> (ns : Mods) -> (defs : Definitions) ->
+                   WhnfContext d n ->
                    (ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
                    (arms : TypeCaseArms d n) -> (def : Term d n) ->
                    (0 _ : So (isTyCon ty)) =>
-                   Either Error (Subset (Elim d n) (No . isRedexE defs))
-  reduceTypeCase defs ctx ty u ret arms def = case ty of
+                   Either Error (Subset (Elim d n) (No . isRedexE ns defs))
+  reduceTypeCase ns defs ctx ty u ret arms def = case ty of
     -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
     TYPE _ =>
-      whnf defs ctx $ tycaseRhsDef0 def KTYPE arms :# ret
+      whnf ns defs ctx $ tycaseRhsDef0 def KTYPE arms :# ret
 
     -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
@@ -583,7 +592,7 @@ mutual
       let arg = arg :# TYPE u
           res = Lam res :# Arr Zero (TYPE u) (TYPE u)
       in
-      whnf defs ctx $ subN (tycaseRhsDef def KPi arms) [< arg, res] :# ret
+      whnf ns defs ctx $ subN (tycaseRhsDef def KPi arms) [< arg, res] :# ret
 
     -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
@@ -591,11 +600,11 @@ mutual
       let fst = fst :# TYPE u
           snd = Lam snd :# Arr Zero (TYPE u) (TYPE u)
       in
-      whnf defs ctx $ subN (tycaseRhsDef def KSig arms) [< fst, snd] :# ret
+      whnf ns defs ctx $ subN (tycaseRhsDef def KSig arms) [< fst, snd] :# ret
 
     -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
     Enum _ =>
-      whnf defs ctx $ tycaseRhsDef0 def KEnum arms :# ret
+      whnf ns defs ctx $ tycaseRhsDef0 def KEnum arms :# ret
 
     -- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q
     --  of { Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
@@ -604,7 +613,7 @@ mutual
     --   (L ∷ A‹0/i›)/l, (R ∷ A‹1/i›)/r] ∷ Q
     Eq a l r =>
       let a0 = a.zero; a1 = a.one in
-      whnf defs ctx $
+      whnf ns defs ctx $
         subN (tycaseRhsDef def KEq arms)
           [< a0 :# TYPE u, a1 :# TYPE u,
              DLam a :# Eq0 (TYPE u) a0 a1, l :# a0, r :# a1]
@@ -612,22 +621,23 @@ mutual
 
     -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
     Nat =>
-      whnf defs ctx $ tycaseRhsDef0 def KNat arms :# ret
+      whnf ns defs ctx $ tycaseRhsDef0 def KNat arms :# ret
 
     -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
     BOX _ s =>
-      whnf defs ctx $ sub1 (tycaseRhsDef def KBOX arms) (s :# TYPE u) :# ret
+      whnf ns defs ctx $ sub1 (tycaseRhsDef def KBOX arms) (s :# TYPE u) :# ret
 
   ||| pushes a coercion inside a whnf-ed term
   private covering
-  pushCoe : {n, d : Nat} -> (defs : Definitions) -> WhnfContext d n ->
+  pushCoe : {n, d : Nat} -> (ns : Mods) -> (defs : Definitions) ->
+            WhnfContext d n ->
             BaseName ->
-            (ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
+            (ty : Term (S d) n) -> (0 tynf : No (isRedexT ns defs ty)) =>
             Dim d -> Dim d ->
-            (s : Term d n) -> (0 snf : No (isRedexT defs s)) =>
-            Either Error (NonRedex Elim d n defs)
-  pushCoe defs ctx i ty p q s =
-    if p == q then whnf defs ctx $ s :# (ty // one q) else
+            (s : Term d n) -> (0 snf : No (isRedexT ns defs s)) =>
+            Either Error (NonRedex Elim d n ns defs)
+  pushCoe ns defs ctx i ty p q s =
+    if p == q then whnf ns defs ctx $ s :# (ty // one q) else
     case s of
       -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
       TYPE {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
@@ -644,7 +654,7 @@ mutual
         let body' = CoeT i ty p q $ Lam body
             term' = [< "y"] :\\ E (weakE 1 body' :@ BVT 0)
             type' = ty // one q
-        whnf defs ctx $ term' :# type'
+        whnf ns defs ctx $ term' :# type'
 
       {-
       -- maybe:
@@ -682,7 +692,7 @@ mutual
         let body' = CoeT i ty p q $ DLam body
             term' = [< "j"] :\\% E (dweakE 1 body' :% BV 0)
             type' = ty // one q
-        whnf defs ctx $ term' :# type'
+        whnf ns defs ctx $ term' :# type'
 
       -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
       Tag tag => do
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 1c2199b..4b12aa0 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -13,15 +13,16 @@ import Quox.EffExtra
 
 public export
 0 TCEff : List (Type -> Type)
-TCEff = [ErrorEff, DefsReader]
+TCEff = [ErrorEff, DefsReader, CurNSReader]
 
 public export
 0 TC : Type -> Type
 TC = Eff TCEff
 
 export
-runTC : Definitions -> TC a -> Either Error a
-runTC defs = extract . runExcept . runReader defs
+runTC : Mods -> Definitions -> TC a -> Either Error a
+runTC ns defs =
+  extract . runExcept . runReaderAt DEFS defs . runReaderAt NS ns
 
 
 export
@@ -148,7 +149,7 @@ mutual
                 (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
+    u <- expectTYPE !ns !defs ctx ty
     expectEqualQ Zero sg.fst
     checkTypeNoWrap ctx t (Just u)
     pure $ zeroFor ctx
@@ -163,7 +164,7 @@ mutual
   check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Lam body) ty = do
-    (qty, arg, res) <- expectPi !ask ctx ty
+    (qty, arg, res) <- expectPi !ns !defs ctx ty
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
     let qty' = sg.fst * qty
@@ -174,7 +175,7 @@ mutual
   check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Pair fst snd) ty = do
-    (tfst, tsnd) <- expectSig !ask ctx ty
+    (tfst, tsnd) <- expectSig !ns !defs ctx ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
     qfst <- checkC ctx sg fst tfst
     let tsnd = sub1 tsnd (fst :# tfst)
@@ -186,7 +187,7 @@ mutual
   check' ctx sg t@(Enum _) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Tag t) ty = do
-    tags <- expectEnum !ask ctx ty
+    tags <- expectEnum !ns !defs ctx ty
     -- if t ∈ ts
     unless (t `elem` tags) $ throw $ TagNotIn t tags
     -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
@@ -195,7 +196,7 @@ mutual
   check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (DLam body) ty = do
-    (ty, l, r) <- expectEq !ask ctx ty
+    (ty, l, r) <- expectEq !ns !defs ctx ty
     let ctx' = extendDim body.name ctx
         ty   = ty.term
         body = body.term
@@ -211,17 +212,17 @@ mutual
   check' ctx sg Nat ty = toCheckType ctx sg Nat ty
 
   check' ctx sg Zero ty = do
-    expectNat !ask ctx ty
+    expectNat !ns !defs ctx ty
     pure $ zeroFor ctx
 
   check' ctx sg (Succ n) ty = do
-    expectNat !ask ctx ty
+    expectNat !ns !defs ctx ty
     checkC ctx sg n Nat
 
   check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Box val) ty = do
-    (q, ty) <- expectBOX !ask ctx ty
+    (q, ty) <- expectBOX !ns !defs ctx ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     valout <- checkC ctx sg val ty
     -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
@@ -299,7 +300,8 @@ mutual
     -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
     case u of
       Just u  => subtype ctx infres.type (TYPE u)
-      Nothing => ignore $ expectTYPE !ask ctx infres.type
+      Nothing => ignore $
+        expectTYPE !ns !defs ctx infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
   private covering
@@ -336,7 +338,7 @@ mutual
 
   infer' ctx sg (F x) = do
     -- if π·x : A {≔ s} in global context
-    g <- lookupFree x !ask
+    g <- lookupFree !ns x !defs
     -- if σ ≤ π
     expectCompatQ sg.fst g.qty.fst
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
@@ -358,7 +360,7 @@ mutual
   infer' ctx sg (fun :@ arg) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
     funres <- inferC ctx sg fun
-    (qty, argty, res) <- expectPi !ask ctx funres.type
+    (qty, argty, res) <- expectPi !ns !defs ctx funres.type
     -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
     argout <- checkC ctx (subjMult sg qty) arg argty
     -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
@@ -375,7 +377,7 @@ mutual
     pairres <- inferC ctx sg pair
     -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
     checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
-    (tfst, tsnd) <- expectSig !ask ctx pairres.type
+    (tfst, tsnd) <- expectSig !ns !defs ctx pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ πσ
@@ -393,7 +395,7 @@ mutual
   infer' ctx sg (CaseEnum pi t ret arms) {d, n} = do
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t
-    ttags <- expectEnum !ask ctx tres.type
+    ttags <- expectEnum !ns !defs ctx tres.type
     -- if 1 ≤ π, OR there is only zero or one option
     unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ One pi
     -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
@@ -419,7 +421,7 @@ mutual
     expectCompatQ One pi
     -- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
     nres <- inferC ctx sg n
-    expectNat !ask ctx nres.type
+    expectNat !ns !defs ctx nres.type
     -- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
     checkTypeC (extendTy Zero ret.name Nat ctx) ret.term Nothing
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
@@ -443,7 +445,7 @@ mutual
   infer' ctx sg (CaseBox pi box ret body) = do
     -- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
     boxres <- inferC ctx sg box
-    (q, ty) <- expectBOX !ask ctx boxres.type
+    (q, ty) <- expectBOX !ns !defs ctx boxres.type
     -- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
     checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
     -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
@@ -461,7 +463,7 @@ mutual
   infer' ctx sg (fun :% dim) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun
-    ty <- fst <$> expectEq !ask ctx type
+    ty <- fst <$> expectEq !ns !defs ctx type
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
@@ -494,7 +496,7 @@ mutual
     -- if σ = 0
     expectEqualQ Zero sg.fst
     -- if Ψ, Γ ⊢₀ e ⇒ Type u
-    u <- expectTYPE !ask ctx . type =<< inferC ctx szero ty
+    u <- expectTYPE !ns !defs ctx . type =<< inferC ctx szero ty
     -- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
     checkTypeC ctx ret Nothing
     -- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 6e27e9b..622909c 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -39,8 +39,8 @@ InferResult eqs d n = IfConsistent eqs $ InferResult' d n
 
 
 export
-lookupFree : Has ErrorEff fs => Name -> Definitions -> Eff fs Definition
-lookupFree x defs = maybe (throw $ NotInScope x) pure $ lookup x defs
+lookupFree : Has ErrorEff fs => Mods -> Name -> Definitions -> Eff fs Definition
+lookupFree ns x defs = maybe (throw $ NotInScope x) pure $ lookupNS ns x defs
 
 
 public export
@@ -59,14 +59,14 @@ substCaseBoxRet dty retty =
   retty.term // (Box (BVT 0) :# weakT 1 dty ::: shift 1)
 
 
-parameters (defs : Definitions) {auto _ : Has ErrorEff fs}
+parameters (ns : Mods) (defs : Definitions) {auto _ : Has ErrorEff fs}
   namespace TyContext
    parameters (ctx : TyContext d n)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
-           tm d n -> Eff fs (NonRedex tm d n defs)
+           tm d n -> Eff fs (NonRedex tm d n ns defs)
     whnf = let Val n = ctx.termLen; Val d = ctx.dimLen in
-           rethrow . whnf defs (toWhnfContext ctx)
+           rethrow . whnf ns defs (toWhnfContext ctx)
 
     private covering %macro
     expect : (forall d, n. NameContexts d n -> Term d n -> Error) ->
@@ -108,8 +108,8 @@ parameters (defs : Definitions) {auto _ : Has ErrorEff fs}
    parameters (ctx : EqContext n)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
-           tm 0 n -> Eff fs (NonRedex tm 0 n defs)
-    whnf = let Val n = ctx.termLen in rethrow . whnf defs (toWhnfContext ctx)
+           tm 0 n -> Eff fs (NonRedex tm 0 n ns defs)
+    whnf = let Val n = ctx.termLen in rethrow . whnf ns defs (toWhnfContext ctx)
 
     private covering %macro
     expect : (forall d, n. NameContexts d n -> Term d n -> Error) ->
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index edb2eae..52ff442 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -21,10 +21,10 @@ defGlobals = fromList
 parameters (label : String) (act : Lazy (TC ()))
            {default defGlobals globals : Definitions}
   testEq : Test
-  testEq = test label $ runTC globals act
+  testEq = test label $ runTC [<] globals act
 
   testNeq : Test
-  testNeq = testThrows label (const True) $ runTC globals act $> "()"
+  testNeq = testThrows label (const True) $ runTC [<] globals act $> "()"
 
 
 parameters (0 d : Nat) (ctx : TyContext d n)
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index 09a15fd..1597dd6 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -13,7 +13,7 @@ parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex} {d, n : Nat}
   private
   testWhnf : String -> WhnfContext d n -> tm d n -> tm d n -> Test
   testWhnf label ctx from to = test "\{label}  (whnf)" $ do
-    result <- bimap toInfo fst $ whnf defs ctx from
+    result <- bimap toInfo fst $ whnf [<] defs ctx from
     unless (result == to) $ Left [("exp", show to), ("got", show result)]
 
   private
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 7daa180..ab5aca7 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -28,7 +28,7 @@ ToInfo Error' where
 M = Eff [Except Error', DefsReader]
 
 inj : TC a -> M a
-inj = rethrow . mapFst TCError <=< lift . runExcept
+inj = rethrow . mapFst TCError <=< lift . runExcept . runReaderAt NS [<]
 
 
 reflTy : Term d n
@@ -90,11 +90,11 @@ parameters (label : String) (act : Lazy (M ()))
            {default defGlobals globals : Definitions}
   testTC : Test
   testTC = test label {e = Error', a = ()} $
-    extract $ runExcept $ runReader globals act
+    extract $ runExcept $ runReaderAt DEFS globals act
 
   testTCFail : Test
   testTCFail = testThrows label (const True) $
-    (extract $ runExcept $ runReader globals act) $> "()"
+    (extract $ runExcept $ runReaderAt DEFS globals act) $> "()"
 
 
 anys : {n : Nat} -> QContext n