diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 87750df..557e115 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -120,11 +120,11 @@ NonRedexTerm q d n defs = Subset (Term q d n) (NotRedex defs)
 
 parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
   namespace Term
-    export %inline
+    export covering %inline
     whnfD : Term q d n -> NonRedexTerm q d n defs
     whnfD = whnf $ \x => lookupElim x defs
 
   namespace Elim
-    export %inline
+    export covering %inline
     whnfD : Elim q d n -> NonRedexElim q d n defs
     whnfD = whnf $ \x => lookupElim x defs
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index a758de4..ea88c5c 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -55,36 +55,52 @@ isTyCon (E     {}) = True
 isTyCon (CloT  {}) = False
 isTyCon (DCloT {}) = False
 
-private
-isSubSing : Term {} -> Bool
-isSubSing ty =
-  let Element ty _ = pushSubsts ty in
-  case ty of
-    TYPE _            => False
-    Pi {res, _}       => isSubSing res.term
-    Lam {}            => False
-    Sig {fst, snd, _} => isSubSing fst && isSubSing snd.term
-    Pair {}           => False
-    Eq {}             => True
-    DLam {}           => False
-    E e               => False
+public export %inline
+sameTyCon : (s, t : Term q d n) ->
+            (0 ts : So (isTyCon s)) => (0 tt : So (isTyCon t)) =>
+            Bool
+sameTyCon (TYPE {}) (TYPE {}) = True
+sameTyCon (TYPE {}) _         = False
+sameTyCon (Pi   {}) (Pi   {}) = True
+sameTyCon (Pi   {}) _         = False
+sameTyCon (Sig  {}) (Sig  {}) = True
+sameTyCon (Sig  {}) _         = False
+sameTyCon (Eq   {}) (Eq   {}) = True
+sameTyCon (Eq   {}) _         = False
+sameTyCon (E    {}) (E    {}) = True
+sameTyCon (E    {}) _         = False
+
+
+parameters (defs : Definitions' q g)
+  private
+  isSubSing : Term q 0 n -> Bool
+  isSubSing ty =
+    let Element ty nc = whnfD defs ty in
+    case ty of
+      TYPE _             => False
+      Pi   {res, _}      => isSubSing res.term
+      Lam  {}            => False
+      Sig  {fst, snd, _} => isSubSing fst && isSubSing snd.term
+      Pair {}            => False
+      Eq   {}            => True
+      DLam {}            => False
+      E    (s :# _)      => isSubSing s
+      E    _             => False
 
 
 parameters {auto _ : HasErr q m}
   export %inline
   ensure : (a -> Error q) -> (p : a -> Bool) -> (t : a) -> m (So (p t))
   ensure e p t = case nchoose $ p t of
-    Left y  => pure y
-    Right n => throwError $ e t
+    Left  y => pure y
+    Right _ => throwError $ e t
 
   export %inline
-  ensureType : (t : Term q d n) -> m (So (isTyCon t))
-  ensureType = ensure NotType isTyCon
+  ensureTyCon : HasErr q m => (t : Term q d n) -> m (So (isTyCon t))
+  ensureTyCon = ensure NotType isTyCon
 
 parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
   mutual
-    -- [todo] remove cumulativity & subtyping, it's too much of a pain
-    -- mugen might be good
     namespace Term
       export covering %inline
       compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
@@ -92,7 +108,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
         let Element ty nty = whnfD defs ty
             Element s  ns  = whnfD defs s
             Element t  nt  = whnfD defs t
-        tty <- ensureType ty
+        tty <- ensureTyCon ty
         compare0' ctx ty s t
 
       private %inline
@@ -107,9 +123,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
                   m ()
       compare0' ctx (TYPE _) s t = compareType ctx s t
 
-      compare0' ctx ty@(Pi {arg, res, _}) s t = local {mode := Equal} $
+      compare0' ctx ty@(Pi {arg, res, _}) s t {n} = local {mode := Equal} $
         let ctx' = ctx :< arg
-            eta : Elim q 0 ? -> ScopeTerm q 0 ? -> m ()
+            eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
             eta e (TUsed   b) = compare0 ctx' res.term (toLamBody e) b
             eta e (TUnused _) = clashT ty s t
         in
@@ -117,7 +133,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
           (Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term
           (E e,      Lam _ b)  => eta e b
           (Lam _ b,  E e)      => eta e b
-          (E e,      E f)      => compare0 ctx e f
+          (E e,      E f)      => Elim.compare0 ctx e f
           _ => throwError $ WrongType ty s t
 
       compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
@@ -137,75 +153,72 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
         -- e.g. an abstract value in an abstract type, bound variables, …
         E e <- pure s | _ => throwError $ WrongType ty s t
         E f <- pure t | _ => throwError $ WrongType ty s t
-        compare0 ctx e f
+        Elim.compare0 ctx e f
 
     export covering
     compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
     compareType ctx s t = do
       let Element s ns = whnfD defs s
           Element t nt = whnfD defs t
-      sok <- ensureType s
-      tok <- ensureType t
+      ts <- ensureTyCon s
+      tt <- ensureTyCon t
+      st <- either pure (const $ clashT (TYPE UAny) s t) $
+            nchoose $ sameTyCon s t
       compareType' ctx s t
 
     private covering
     compareType' : TContext q 0 n -> (s, t : Term q 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)) =>
                    m ()
-    compareType' ctx s t = do
-      let err : m () = clashT (TYPE UAny) s t
-      case s of
-        TYPE k => do
-          TYPE l <- pure t | _ => err
-          expectModeU !mode k l
+    compareType' ctx (TYPE k) (TYPE l) =
+      expectModeU !mode k l
 
-        Pi {qty = sQty, arg = sArg, res = sRes, _} => do
-          Pi {qty = tQty, arg = tArg, res = tRes, _} <- pure t | _ => err
-          expectEqualQ sQty tQty
-          compareType ctx tArg sArg -- contra
-          -- [todo] is using sArg also ok for subtyping?
-          compareType (ctx :< sArg) sRes.term tRes.term
+    compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, _})
+                     (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
+      expectEqualQ sQty tQty
+      local {mode $= flip} $ compareType ctx sArg tArg -- contra
+      compareType (ctx :< sArg) sRes.term tRes.term
 
-        Sig {fst = sFst, snd = sSnd, _} => do
-          Sig {fst = tFst, snd = tSnd, _} <- pure t | _ => err
-          compareType ctx sFst tFst
-          compareType (ctx :< sFst) sSnd.term tSnd.term
+    compareType' ctx (Sig {fst = sFst, snd = sSnd, _})
+                     (Sig {fst = tFst, snd = tSnd, _}) = do
+      compareType ctx sFst tFst
+      compareType (ctx :< sFst) sSnd.term tSnd.term
 
-        Eq {ty = sTy, l = sl, r = sr, _} => do
-          Eq {ty = tTy, l = tl, r = tr, _} <- pure t | _ => err
-          compareType ctx sTy.zero tTy.zero
-          compareType ctx sTy.one  tTy.one
-          local {mode := Equal} $ do
-            compare0 ctx sTy.zero sl tl
-            compare0 ctx sTy.one  sr tr
+    compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
+                     (Eq {ty = tTy, l = tl, r = tr, _}) = do
+      compareType ctx sTy.zero tTy.zero
+      compareType ctx sTy.one  tTy.one
+      local {mode := Equal} $ do
+        Term.compare0 ctx sTy.zero sl tl
+        Term.compare0 ctx sTy.one  sr tr
 
-        E e => do
-          E f <- pure t | _ => err
-          -- no fanciness needed here cos anything other than a neutral
-          -- has been inlined by whnfD
-          compare0 ctx e f
+    compareType' ctx (E e) (E f) = do
+      -- no fanciness needed here cos anything other than a neutral
+      -- has been inlined by whnfD
+      Elim.compare0 ctx e f
 
     ||| assumes the elim is already typechecked! only does the work necessary
     ||| to calculate the overall type
     private covering
     computeElimType : TContext q 0 n -> (e : Elim q 0 n) ->
-                      (0 ne : NotRedex defs e) =>
+                      (0 ne : NotRedex defs e) ->
                       m (Term q 0 n)
-    computeElimType ctx (F x) = do
+    computeElimType ctx (F x) _ = do
       defs <- lookupFree' defs x
       pure $ defs.type.get
-    computeElimType ctx (B i) = do
+    computeElimType ctx (B i) _ = do
       pure $ ctx !! i
-    computeElimType ctx (f :@ s) {ne} = do
-      (_, arg, res) <- computeElimType ctx f {ne = noOr1 ne} >>= expectPi defs
+    computeElimType ctx (f :@ s) ne = do
+      (_, arg, res) <- expectPi defs !(computeElimType ctx f (noOr1 ne))
       pure $ sub1 res (s :# arg)
-    computeElimType ctx (CasePair {pair, ret, _}) = do
+    computeElimType ctx (CasePair {pair, ret, _}) _ = do
       pure $ sub1 ret pair
-    computeElimType ctx (f :% p) {ne} = do
-      (ty, _, _) <- computeElimType ctx f {ne = noOr1 ne} >>= expectEq defs
+    computeElimType ctx (f :% p) ne = do
+      (ty, _, _) <- expectEq defs !(computeElimType ctx f (noOr1 ne))
       pure $ dsub1 ty p
-    computeElimType ctx (_ :# ty) = do
+    computeElimType ctx (_ :# ty) _ = do
       pure ty
 
     private covering
@@ -213,13 +226,12 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
                  (e : Elim q 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
                  m (Elim q 0 n)
     replaceEnd ctx e p ne = do
-      (ty, l, r) <- computeElimType ctx e >>= expectEq defs
+      (ty, l, r) <- expectEq defs !(computeElimType ctx e ne)
       pure $ ends l r p :# dsub1 ty (K p)
 
     namespace Elim
       -- [fixme] the following code ends up repeating a lot of work in the
       -- computeElimType calls. the results should be shared better
-
       export covering %inline
       compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
       compare0 ctx e f =
@@ -227,48 +239,50 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
             Element f nf = whnfD defs f
         in
         -- [fixme] there is a better way to do this "isSubSing" stuff for sure
-        unless (isSubSing !(computeElimType ctx e)) $ compare0' ctx e f
+        unless (isSubSing defs !(computeElimType ctx e ne)) $
+          compare0' ctx e f ne nf
 
       private covering
       compare0' : TContext q 0 n ->
                   (e, f : Elim q 0 n) ->
-                  (0 ne : NotRedex defs e) => (0 nf : NotRedex defs f) =>
+                  (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
                   m ()
       -- replace applied equalities with the appropriate end first
-      -- e.g. e : Eq [i ⇒ A] s t ⊢ e 0 = s : A‹0/i›
-      compare0' ctx (e :% K p) f {ne} =
+      -- e.g. e : Eq [i ⇒ A] s t ⊢ e 𝟎 = s : A‹𝟎/i›
+      compare0' ctx (e :% K p) f ne nf =
         compare0 ctx !(replaceEnd ctx e p $ noOr1 ne) f
-      compare0' ctx e (f :% K q) {nf} =
+      compare0' ctx e (f :% K q) ne nf =
         compare0 ctx e !(replaceEnd ctx f q $ noOr1 nf)
 
-      compare0' _ e@(F x) f@(F y) = unless (x == y) $ clashE e f
-      compare0' _ e@(F _) f = clashE e f
+      compare0' _ e@(F x) f@(F y) _ _ = unless (x == y) $ clashE e f
+      compare0' _ e@(F _) f _ _ = clashE e f
 
-      compare0' ctx e@(B i) f@(B j) = unless (i == j) $ clashE e f
-      compare0' _ e@(B _) f = clashE e f
+      compare0' ctx e@(B i) f@(B j) _ _ = unless (i == j) $ clashE e f
+      compare0' _ e@(B _) f _ _ = clashE e f
 
-      compare0' ctx (e :@ s) (f :@ t) {ne} = local {mode := Equal} $ do
-        compare0 ctx e f
-        (_, arg, _) <- computeElimType ctx e {ne = noOr1 ne} >>= expectPi defs
-        compare0 ctx arg s t
-      compare0' _ e@(_ :@ _) f = clashE e f
-
-      compare0' ctx (CasePair epi e _ eret _ _ ebody)
-                    (CasePair fpi f _ fret _ _ fbody) {ne} =
+      compare0' ctx (e :@ s) (f :@ t) ne nf =
         local {mode := Equal} $ do
           compare0 ctx e f
-          ety <- computeElimType ctx e {ne = noOr1 ne}
+          (_, arg, _) <- expectPi defs !(computeElimType ctx e (noOr1 ne))
+          Term.compare0 ctx arg s t
+      compare0' _ e@(_ :@ _) f _ _ = clashE e f
+
+      compare0' ctx (CasePair epi e _ eret _ _ ebody)
+                    (CasePair fpi f _ fret _ _ fbody) ne nf =
+        local {mode := Equal} $ do
+          compare0 ctx e f
+          ety <- computeElimType ctx e (noOr1 ne)
           compareType (ctx :< ety) eret.term fret.term
           (fst, snd) <- expectSig defs ety
-          compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret)
+          Term.compare0 (ctx :< fst :< snd.term) (substCasePairRet ety eret)
             ebody.term fbody.term
           unless (epi == fpi) $ throwError $ ClashQ epi fpi
-      compare0' _ e@(CasePair {}) f = clashE e f
+      compare0' _ e@(CasePair {}) f _ _ = clashE e f
 
-      compare0' ctx (s :# a) (t :# b) = do
-        compareType ctx a b
-        compare0 ctx a s t
-      compare0' _ e@(_ :# _) f = clashE e f
+      compare0' ctx   (s :# a) (t :# _) _ _ = Term.compare0 ctx a s t
+      compare0' ctx   (s :# a) f        _ _ = Term.compare0 ctx a s (E f)
+      compare0' ctx e          (t :# b) _ _ = Term.compare0 ctx b (E e) t
+      compare0' _   e@(_ :# _) f        _ _ = clashE e f
 
 
 parameters {auto _ : (HasDefs' q _ m, HasErr q m, Eq q)}
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 0d934d8..1550c3a 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -90,7 +90,7 @@ mutual
     ||| `CasePair 𝜋 𝑒 𝑟 𝐴 𝑥 𝑦 𝑡` is
     ||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
     CasePair : (qty : q) -> (pair : Elim q d n) ->
-               (r : Name) -> (ret  : ScopeTerm q d n) ->
+               (r : Name) -> (ret : ScopeTerm q d n) ->
                (x, y : Name) -> (body : ScopeTermN 2 q d n) ->
                Elim q d n
 
@@ -146,6 +146,11 @@ public export %inline
 Eq0 : (ty, l, r : Term q d n) -> Term q d n
 Eq0 {ty, l, r} = Eq {i = "_", ty = DUnused ty, l, r}
 
+||| non dependent pair type
+public export %inline
+And : (fst, snd : Term q d n) -> Term q d n
+And {fst, snd} = Sig {x = "_", fst, snd = TUnused snd}
+
 ||| same as `F` but as a term
 public export %inline
 FT : Name -> Term q d n
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index 2779c24..b955654 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -109,7 +109,7 @@ record InferResult q d n where
 
 
 public export
-data EqMode = Equal | Sub
+data EqMode = Equal | Sub | Super
 %runElab derive "EqMode" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
@@ -138,8 +138,15 @@ HasErr q = MonadError (Error q)
 
 export %inline
 ucmp : EqMode -> Universe -> Universe -> Bool
-ucmp Sub   = (<=)
 ucmp Equal = (==)
+ucmp Sub   = (<=)
+ucmp Super = (>=)
+
+export %inline
+flip : EqMode -> EqMode
+flip Equal = Equal
+flip Sub   = Super
+flip Super = Sub
 
 
 parameters {auto _ : HasErr q m}
@@ -172,7 +179,7 @@ lookupFree' defs x =
     Nothing => throwError $ NotInScope x
 
 
-export
+public export
 substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n)
 substCasePairRet dty retty =
   let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in
diff --git a/tests/Tests.idr b/tests/Tests.idr
index 27342ab..f3b70f8 100644
--- a/tests/Tests.idr
+++ b/tests/Tests.idr
@@ -14,4 +14,4 @@ allTests = [
   Typechecker.tests
 ]
 
-main = TAP.main !getTestOpts allTests
+main = TAP.main !getTestOpts ["all" :- allTests]
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index e3e7ee9..5d6789d 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -15,7 +15,9 @@ defGlobals = fromList
    ("a", mkAbstract Any  $ FT "A"),
    ("a'", mkAbstract Any  $ FT "A"),
    ("b", mkAbstract Any  $ FT "B"),
-   ("f", mkAbstract Any  $ Arr One (FT "A") (FT "A"))]
+   ("f", mkAbstract Any  $ Arr One (FT "A") (FT "A")),
+   ("id", mkDef Any (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0)),
+   ("eq-ab", mkAbstract Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))]
 
 parameters (label : String) (act : Lazy (M ()))
            {default defGlobals globals : Definitions Three}
@@ -45,15 +47,15 @@ parameters {default 0   d, n : Nat}
 export
 tests : Test
 tests = "equality & subtyping" :- [
+  note #""s{t,…}" for term substs; "s‹p,…›" for dim substs"#,
   note #""0=1 ⊢ 𝒥" means that 𝒥 holds in an inconsistent dim context"#,
-  note #""s{…}" for term substs; "s‹…›" for dim substs"#,
 
   "universes" :- [
-    testEq "★₀ ≡ ★₀" $
+    testEq "★₀ = ★₀" $
       equalT [<] (TYPE 1) (TYPE 0) (TYPE 0),
-    testNeq "★₀ ≢ ★₁" $
+    testNeq "★₀ ≠ ★₁" $
       equalT [<] (TYPE 2) (TYPE 0) (TYPE 1),
-    testNeq "★₁ ≢ ★₀" $
+    testNeq "★₁ ≠ ★₀" $
       equalT [<] (TYPE 2) (TYPE 1) (TYPE 0),
     testEq "★₀ <: ★₀" $
       subT [<] (TYPE 1) (TYPE 0) (TYPE 0),
@@ -64,33 +66,15 @@ tests = "equality & subtyping" :- [
   ],
 
   "pi" :- [
-    note #""A ⊸ B" for (1·A) → B"#,
-    note #""A ⇾ B" for (0·A) → B"#,
-    testEq "A ⊸ B ≡ A ⊸ B" $
-      let tm = Arr One (FT "A") (FT "B") in
-      equalT [<] (TYPE 0) tm tm,
-    testNeq "A ⇾ B ≢ A ⊸ B" $
-      let tm1 = Arr Zero (FT "A") (FT "B")
-          tm2 = Arr One  (FT "A") (FT "B") in
-      equalT [<] (TYPE 0) tm1 tm2,
-    testEq "0=1 ⊢ A ⇾ B ≢ A ⊸ B" $
-      let tm1 = Arr Zero (FT "A") (FT "B")
-          tm2 = Arr One  (FT "A") (FT "B") in
-      equalT [<] (TYPE 0) tm1 tm2 {eqs = ZeroIsOne},
-    testEq "A ⊸ B <: A ⊸ B" $
-      let tm = Arr One (FT "A") (FT "B") in
-      subT [<] (TYPE 0) tm tm,
-    testNeq "A ⇾ B ≮: A ⊸ B" $
-      let tm1 = Arr Zero (FT "A") (FT "B")
-          tm2 = Arr One  (FT "A") (FT "B") in
-      subT [<] (TYPE 0) tm1 tm2,
-    testEq "★₀ ⇾ ★₀ ≡ ★₀ ⇾ ★₀" $
+    note #""𝐴 ⊸ 𝐵" for (1·𝐴) → 𝐵"#,
+    note #""𝐴 ⇾ 𝐵" for (0·𝐴) → 𝐵"#,
+    testEq "★₀ ⇾ ★₀ = ★₀ ⇾ ★₀" $
       let tm = Arr Zero (TYPE 0) (TYPE 0) in
       equalT [<] (TYPE 1) tm tm,
     testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $
       let tm = Arr Zero (TYPE 0) (TYPE 0) in
       subT [<] (TYPE 1) tm tm,
-    testNeq "★₁ ⊸ ★₀ ≢ ★₀ ⇾ ★₀" $
+    testNeq "★₁ ⊸ ★₀ ≠ ★₀ ⇾ ★₀" $
       let tm1 = Arr Zero (TYPE 1) (TYPE 0)
           tm2 = Arr Zero (TYPE 0) (TYPE 0) in
       equalT [<] (TYPE 2) tm1 tm2,
@@ -98,10 +82,6 @@ tests = "equality & subtyping" :- [
       let tm1 = Arr One (TYPE 1) (TYPE 0)
           tm2 = Arr One (TYPE 0) (TYPE 0) in
       subT [<] (TYPE 2) tm1 tm2,
-    testNeq "★₀ ⊸ ★₀ ≢ ★₀ ⇾ ★₁" $
-      let tm1 = Arr Zero (TYPE 0) (TYPE 0)
-          tm2 = Arr Zero (TYPE 0) (TYPE 1) in
-      equalT [<] (TYPE 2) tm1 tm2,
     testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
       let tm1 = Arr One (TYPE 0) (TYPE 0)
           tm2 = Arr One (TYPE 0) (TYPE 1) in
@@ -109,11 +89,35 @@ tests = "equality & subtyping" :- [
     testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
       let tm1 = Arr One (TYPE 0) (TYPE 0)
           tm2 = Arr One (TYPE 0) (TYPE 1) in
-      subT [<] (TYPE 2) tm1 tm2
+      subT [<] (TYPE 2) tm1 tm2,
+    testEq "A ⊸ B = A ⊸ B" $
+      let tm = Arr One (FT "A") (FT "B") in
+      equalT [<] (TYPE 0) tm tm,
+    testEq "A ⊸ B <: A ⊸ B" $
+      let tm = Arr One (FT "A") (FT "B") in
+      subT [<] (TYPE 0) tm tm,
+    note "incompatible quantities",
+    testNeq "★₀ ⊸ ★₀ ≠ ★₀ ⇾ ★₁" $
+      let tm1 = Arr Zero (TYPE 0) (TYPE 0)
+          tm2 = Arr Zero (TYPE 0) (TYPE 1) in
+      equalT [<] (TYPE 2) tm1 tm2,
+    testNeq "A ⇾ B ≠ A ⊸ B" $
+      let tm1 = Arr Zero (FT "A") (FT "B")
+          tm2 = Arr One  (FT "A") (FT "B") in
+      equalT [<] (TYPE 0) tm1 tm2,
+    testNeq "A ⇾ B ≮: A ⊸ B" $
+      let tm1 = Arr Zero (FT "A") (FT "B")
+          tm2 = Arr One  (FT "A") (FT "B") in
+      subT [<] (TYPE 0) tm1 tm2,
+    testEq "0=1 ⊢ A ⇾ B = A ⊸ B" $
+      let tm1 = Arr Zero (FT "A") (FT "B")
+          tm2 = Arr One  (FT "A") (FT "B") in
+      equalT [<] (TYPE 0) tm1 tm2 {eqs = ZeroIsOne},
+    note "[todo] should π ≤ ρ ⊢ (ρ·A) → B <: (π·A) → B?"
   ],
 
   "lambda" :- [
-    testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $
+    testEq "λ x ⇒ [x] = λ x ⇒ [x]" $
       equalT [<] (Arr One (FT "A") (FT "A"))
         (["x"] :\\ BVT 0)
         (["x"] :\\ BVT 0),
@@ -121,7 +125,7 @@ tests = "equality & subtyping" :- [
       subT [<] (Arr One (FT "A") (FT "A"))
         (["x"] :\\ BVT 0)
         (["x"] :\\ BVT 0),
-    testEq "λ x ⇒ [x] ≡ λ y ⇒ [y]" $
+    testEq "λ x ⇒ [x] = λ y ⇒ [y]" $
       equalT [<] (Arr One (FT "A") (FT "A"))
         (["x"] :\\ BVT 0)
         (["y"] :\\ BVT 0),
@@ -129,74 +133,124 @@ tests = "equality & subtyping" :- [
       equalT [<] (Arr One (FT "A") (FT "A"))
         (["x"] :\\ BVT 0)
         (["y"] :\\ BVT 0),
-    testNeq "λ x y ⇒ [x] ≢ λ x y ⇒ [y]" $
+    testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $
       equalT [<] (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
         (["x", "y"] :\\ BVT 1)
         (["x", "y"] :\\ BVT 0),
-    testEq "λ x ⇒ [a] ≡ λ x ⇒ [a]  (TUsed vs TUnused)" $
+    testEq "λ x ⇒ [a] = λ x ⇒ [a]  (TUsed vs TUnused)" $
       equalT [<] (Arr Zero (FT "B") (FT "A"))
         (Lam "x" $ TUsed   $ FT "a")
         (Lam "x" $ TUnused $ FT "a"),
-    testEq "λ x ⇒ [f [x]] ≡ [f]  (η)" $
+    testEq "λ x ⇒ [f [x]] = [f]  (η)" $
       equalT [<] (Arr One (FT "A") (FT "A"))
         (["x"] :\\ E (F "f" :@ BVT 0))
         (FT "f")
   ],
 
   "eq type" :- [
-    testEq "(★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : ★₁)" $
+    testEq "(★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : ★₁)" $
       let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in
       equalT [<] (TYPE 2) tm tm,
-    testEq "A ≔ ★₁ ⊢ (★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : A)"
+    testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)"
         {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $
       equalT [<] (TYPE 2)
         (Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
         (Eq0 (FT "A") (TYPE 0) (TYPE 0))
   ],
 
-  "equalities" :-
+  "equalities and uip" :-
   let refl : Term q d n -> Term q d n -> Elim q d n
       refl a x = (DLam "_" $ DUnused x) :# (Eq0 a x x)
   in
   [
     note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
-    testEq "refl [A] a ≡ refl [A] a" $
+    note "binds before ∥ are globals, after it are BVs",
+    testEq "refl [A] a = refl [A] a" $
       equalE [<] (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
-    testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ⊢ p ≡ q  (free)"
+
+    testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q  (free)"
            {globals =
               let def = mkAbstract Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in
               defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
       equalE [<] (F "p") (F "q"),
-    testEq "x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x ≡ y  (bound)" $
+
+    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
-      equalE [< ty, ty] (BV 0) (BV 1) {n = 2}
+      equalE [< ty, ty] (BV 0) (BV 1) {n = 2},
+
+    testEq "∥ x : [(a ≡ a' : A) ∷ Type 0], y : [ditto] ⊢ x = y" $
+      let ty :  forall n. Term Three 0 n
+             := E (Eq0 (FT "A") (FT "a") (FT "a'") :# TYPE 0) in
+      equalE [< ty, ty] (BV 0) (BV 1) {n = 2},
+
+    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"))]} $
+      equalE [< FT "EE", FT "EE"] (BV 0) (BV 1) {n = 2},
+
+    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"))]} $
+      equalE [< FT "EE", FT "E"] (BV 0) (BV 1) {n = 2},
+
+    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'")))]} $
+      equalE [< FT "E", FT "E"] (BV 0) (BV 1) {n = 2},
+
+    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
+             := Sig "_" (FT "E") $ TUnused $ FT "E" in
+      equalE [< ty, ty] (BV 0) (BV 1) {n = 2},
+
+    testEq "E ≔ a ≡ a' : A, F ≔ E × E ∥ x : F, y : F ⊢ 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"))]} $
+      equalE [< FT "W", FT "W"] (BV 0) (BV 1) {n = 2}
   ],
 
   "term closure" :- [
-    note "𝑖, 𝑗 for bound variables pointing outside of the current expr",
-    testEq "[𝑖]{} ≡ [𝑖]" $
+    testEq "[#0]{} = [#0] : A" $
       equalT [< FT "A"] (FT "A") {n = 1}
         (CloT (BVT 0) id)
         (BVT 0),
-    testEq "[𝑖]{a/𝑖} ≡ [a]" $
+    testEq "[#0]{a} = [a] : A" $
       equalT [<] (FT "A")
         (CloT (BVT 0) (F "a" ::: id))
         (FT "a"),
-    testEq "[𝑖]{a/𝑖,b/𝑗} ≡ [a]" $
+    testEq "[#0]{a,b} = [a] : A" $
       equalT [<] (FT "A")
         (CloT (BVT 0) (F "a" ::: F "b" ::: id))
         (FT "a"),
-    testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a]  (TUnused)" $
+    testEq "[#1]{a,b} = [b] : A" $
+      equalT [<] (FT "A")
+        (CloT (BVT 1) (F "a" ::: F "b" ::: id))
+        (FT "b"),
+    testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A  (TUnused)" $
       equalT [<] (Arr Zero (FT "B") (FT "A"))
         (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
         (Lam "y" $ TUnused $ FT "a"),
-    testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a]  (TUsed)" $
+    testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A  (TUsed)" $
       equalT [<] (Arr Zero (FT "B") (FT "A"))
         (CloT (["y"] :\\ BVT 1) (F "a" ::: id))
         (["y"] :\\ FT "a")
   ],
 
-  todo "term d-closure",
+  "term d-closure" :- [
+    testEq "★₀‹𝟎› = ★₀ : ★₁" $
+      equalT {d = 1} [<] (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0),
+    testEq "(λᴰ i ⇒ a)‹𝟎› = (λᴰ i ⇒ a) : (a ≡ a : A)" $
+      equalT {d = 1} [<]
+        (Eq0 (FT "A") (FT "a") (FT "a"))
+        (DCloT (["i"] :\\% FT "a") (K Zero ::: id))
+        (["i"] :\\% FT "a"),
+    note "it is hard to think of well-typed terms with big dctxs"
+  ],
 
   "free var" :-
   let au_bu = fromList
@@ -206,17 +260,19 @@ tests = "equality & subtyping" :- [
         [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
          ("B", mkDef Any (TYPE (U 1)) (FT "A"))]
   in [
-    testEq "A ≡ A" $
+    testEq "A = A" $
       equalE [<] (F "A") (F "A"),
-    testNeq "A ≢ B" $
+    testNeq "A ≠ B" $
       equalE [<] (F "A") (F "B"),
-    testEq "0=1 ⊢ A ≡ B" $
+    testEq "0=1 ⊢ A = B" $
       equalE {eqs = ZeroIsOne} [<] (F "A") (F "B"),
-    testEq "A : ★₁ ≔ ★₀ ⊢ A ≡ (★₀ ∷ ★₁)" {globals = au_bu} $
+    testEq "A : ★₁ ≔ ★₀ ⊢ A = (★₀ ∷ ★₁)" {globals = au_bu} $
       equalE [<] (F "A") (TYPE 0 :# TYPE 1),
-    testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A ≡ B" {globals = au_bu} $
+    testEq "A : ★₁ ≔ ★₀ ⊢ [A] = ★₀" {globals = au_bu} $
+      equalT [<] (TYPE 1) (FT "A") (TYPE 0),
+    testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A = B" {globals = au_bu} $
       equalE [<] (F "A") (F "B"),
-    testEq "A ≔ ★₀, B ≔ A ⊢ A ≡ B" {globals = au_ba} $
+    testEq "A ≔ ★₀, B ≔ A ⊢ A = B" {globals = au_ba} $
       equalE [<] (F "A") (F "B"),
     testEq "A <: A" $
       subE [<] (F "A") (F "A"),
@@ -226,7 +282,8 @@ tests = "equality & subtyping" :- [
         {globals = fromList [("A", mkDef Any (TYPE 3) (TYPE 0)),
                              ("B", mkDef Any (TYPE 3) (TYPE 2))]} $
       subE [<] (F "A") (F "B"),
-    testEq "A : ★₁👈 ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: 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))]} $
       subE [<] (F "A") (F "B"),
@@ -235,30 +292,33 @@ tests = "equality & subtyping" :- [
   ],
 
   "bound var" :- [
-    note "𝑖, 𝑗 for distinct bound variables",
-    testEq "𝑖 ≡ 𝑖" $
+    testEq "#0 = #0" $
       equalE [< TYPE 0] (BV 0) (BV 0) {n = 1},
-    testNeq "𝑖 ≢ 𝑗" $
+    testEq "#0 <: #0" $
+      subE [< TYPE 0] (BV 0) (BV 0) {n = 1},
+    testNeq "#0 ≠ #1" $
       equalE [< TYPE 0, TYPE 0] (BV 0) (BV 1) {n = 2},
-    testEq "0=1 ⊢ 𝑖 ≡ 𝑗" $
+    testNeq "#0 ≮: #1" $
+      subE [< TYPE 0, TYPE 0] (BV 0) (BV 1) {n = 2},
+    testEq "0=1 ⊢ #0 = #1" $
       equalE [< TYPE 0, TYPE 0] (BV 0) (BV 1)
         {n = 2, eqs = ZeroIsOne}
   ],
 
   "application" :- [
-    testEq "f [a] ≡ f [a]" $
+    testEq "f [a] = f [a]" $
       equalE [<] (F "f" :@ FT "a") (F "f" :@ FT "a"),
     testEq "f [a] <: f [a]" $
       subE [<] (F "f" :@ FT "a") (F "f" :@ FT "a"),
-    testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A)  (β)" $
+    testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A)  (β)" $
       equalE [<]
         (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
         (E (FT "a" :# FT "A") :# FT "A"),
-    testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a  (βυ)" $
+    testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a  (βυ)" $
       equalE [<]
         (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
         (F "a"),
-    testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [a]  (β↘↙)" $
+    testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a]  (β↘↙)" $
       let a = FT "A"; a2a = (Arr One a a) in
       equalE [<]
         (((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f")
@@ -267,25 +327,68 @@ tests = "equality & subtyping" :- [
       subE [<]
         (((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a")
         (F "a"),
-    testEq "id : A ⊸ A ≔ λ x ⇒ [x] ⊢ id [a] ≡ a"
-           {globals = defGlobals `mergeLeft` fromList
-              [("id", mkDef Any (Arr One (FT "A") (FT "A"))
-                                (["x"] :\\ BVT 0))]} $
-      equalE [<] (F "id" :@ FT "a") (F "a")
+    note "id : A ⊸ A ≔ λ x ⇒ [x]",
+    testEq "id [a] = a" $ equalE [<] (F "id" :@ FT "a") (F "a"),
+    testEq "id [a] <: a" $ subE [<] (F "id" :@ FT "a") (F "a")
   ],
 
   todo "dim application",
 
-  todo "annotation",
+  "annotation" :- [
+    testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $
+      equalE [<]
+        ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
+        (FT "f" :# Arr One (FT "A") (FT "A")),
+    testEq "[f] ∷ A ⊸ A = f" $
+      equalE [<] (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"),
+    testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $
+      equalE [<]
+        ((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
+        (F "f")
+  ],
 
-  todo "elim closure",
+  "elim closure" :- [
+    testEq "#0{a} = a" $
+      equalE [<] (CloE (BV 0) (F "a" ::: id)) (F "a"),
+    testEq "#1{a} = #0" $
+      equalE [< FT "A"] (CloE (BV 1) (F "a" ::: id)) (BV 0) {n = 1}
+  ],
 
-  todo "elim d-closure",
+  "elim d-closure" :- [
+    note "0·eq-ab : (A ≡ B : ★₀)",
+    testEq "(eq-ab #0)‹𝟎› = eq-ab 𝟎" $
+      equalE {d = 1} [<]
+        (DCloE (F "eq-ab" :% BV 0) (K Zero ::: id))
+        (F "eq-ab" :% K Zero),
+    testEq "(eq-ab #0)‹𝟎› = A" $
+      equalE {d = 1} [<] (DCloE (F "eq-ab" :% BV 0) (K Zero ::: id)) (F "A"),
+    testEq "(eq-ab #0)‹𝟏› = B" $
+      equalE {d = 1} [<] (DCloE (F "eq-ab" :% BV 0) (K One  ::: id)) (F "B"),
+    testNeq "(eq-ab #0)‹𝟏› ≠ A" $
+      equalE {d = 1} [<] (DCloE (F "eq-ab" :% BV 0) (K One  ::: id)) (F "A"),
+    testEq "(eq-ab #0)‹#0,𝟎› = (eq-ab #0)" $
+      equalE {d = 2} [<]
+        (DCloE (F "eq-ab" :% BV 0) (BV 0 ::: K Zero ::: id))
+        (F "eq-ab" :% BV 0),
+    testNeq "(eq-ab #0)‹𝟎› ≠ (eq-ab 𝟎)" $
+      equalE {d = 2} [<]
+        (DCloE (F "eq-ab" :% BV 0) (BV 0 ::: K Zero ::: id))
+        (F "eq-ab" :% K Zero),
+    testEq "#0‹𝟎› = #0  # term and dim vars distinct" $
+      equalE {d = 1, n = 1} [< FT "A"] (DCloE (BV 0) (K Zero ::: id)) (BV 0),
+    testEq "a‹𝟎› = a" $
+      equalE {d = 1} [<] (DCloE (F "a") (K Zero ::: id)) (F "a"),
+    testEq "(f [a])‹𝟎› = f‹𝟎› [a]‹𝟎›" $
+      let th = (K Zero ::: id) in
+      equalE {d = 1} [<]
+        (DCloE (F "f" :@ FT "a") th)
+        (DCloE (F "f") th :@ DCloT (FT "a") th)
+  ],
 
   "clashes" :- [
-    testNeq "★₀ ≢ ★₀ ⇾ ★₀" $
+    testNeq "★₀ ≠ ★₀ ⇾ ★₀" $
       equalT [<] (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
-    testEq "0=1 ⊢ ★₀ ≡ ★₀ ⇾ ★₀" $
+    testEq "0=1 ⊢ ★₀ = ★₀ ⇾ ★₀" $
       equalT [<] (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0))
         {eqs = ZeroIsOne},
     todo "others"
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 1e516b3..b82b43a 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -15,7 +15,7 @@ M = ReaderT (Definitions Three) $ Either (Error Three)
 reflTy : IsQty q => Term q d n
 reflTy =
   Pi zero "A" (TYPE 0) $ TUsed $
-  Pi zero "x" (BVT 0)  $ TUsed $
+  Pi one  "x" (BVT 0)  $ TUsed $
   Eq0 (BVT 1) (BVT 0) (BVT 0)
 
 reflDef : IsQty q => Term q d n
@@ -27,9 +27,13 @@ defGlobals = fromList
    ("B", mkAbstract Zero $ TYPE 0),
    ("C", mkAbstract Zero $ TYPE 1),
    ("D", mkAbstract Zero $ TYPE 1),
+   ("P", mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
    ("a", mkAbstract Any  $ FT "A"),
    ("b", mkAbstract Any  $ FT "B"),
    ("f", mkAbstract Any  $ Arr One (FT "A") (FT "A")),
+   ("g", mkAbstract Any  $ Arr One (FT "A") (FT "B")),
+   ("p", mkAbstract Any  $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
+   ("q", mkAbstract Any  $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
    ("refl", mkDef Any reflTy reflDef)]
 
 parameters (label : String) (act : Lazy (M ()))
@@ -79,60 +83,81 @@ tests = "typechecker" :- [
 
   "function types" :- [
     note "A, B : ★₀;  C, D : ★₁",
-    testTC "0 · (1·A) → B ⇐ ★₀" $
+    testTC "0 · A ⊸ B ⇐ ★₀" $
       check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0),
-    testTC "0 · (1·A) → B ⇐ ★₁👈" $
+    note "subtyping",
+    testTC "0 · A ⊸ B ⇐ ★₁" $
       check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 1),
-    testTC "0 · (1·C) → D ⇐ ★₁" $
+    testTC "0 · C ⊸ D ⇐ ★₁" $
       check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1),
-    testTCFail "0 · (1·C) → D ⇍ ★₀" $
+    testTCFail "0 · C ⊸ D ⇍ ★₀" $
       check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0)
   ],
 
   "free vars" :- [
+    note "A : ★₀",
     testTC "0 · A ⇒ ★₀" $
       inferAs (ctx [<]) szero (F "A") (TYPE 0),
-    testTC "0 · A ⇐👈 ★₀" $
+    note "check",
+    testTC "0 · A ⇐ ★₀" $
       check_ (ctx [<]) szero (FT "A") (TYPE 0),
-    testTC "0 · A ⇐ ★₁👈" $
+    note "subtyping",
+    testTC "0 · A ⇐ ★₁" $
       check_ (ctx [<]) szero (FT "A") (TYPE 1),
-    testTCFail "1👈 · A ⇏ ★₀" $
+    note "(fail) runtime-relevant type",
+    testTCFail "1 · A ⇏ ★₀" $
       infer_ (ctx [<]) sone (F "A"),
-    note "refl : (0·A : ★₀) → (0·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)",
-    testTC "1 · refl ⇒ {type of refl}" $
-      inferAs (ctx [<]) sone (F "refl") reflTy,
-    testTC "1 · refl ⇐ {type of refl}" $
-      check_ (ctx [<]) sone (FT "refl") reflTy
+    note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)",
+    testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F  "refl") reflTy,
+    testTC "1 · refl ⇐ ⋯" $ check_  (ctx [<]) sone (FT "refl") reflTy
   ],
 
   "lambda" :- [
-    testTC #"1 · (λ A x ⇒ refl A x) ⇐ {type of refl, see "free vars"}"# $
+    note "linear & unrestricted identity",
+    testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $
+      check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
+    testTC "1 · (λ x ⇒ x) ⇐ A → A" $
+      check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
+    note "(fail) zero binding used relevantly",
+    testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $
+      check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
+    note "(but ok in overall erased context)",
+    testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
+      check_ (ctx [<]) szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
+    testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯  # (type of refl)" $
       check_ (ctx [<]) sone
         (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
-        reflTy
+        reflTy,
+    testTC "1 · (λ A x ⇒ λᴰ i ⇒ x) ⇐ ⋯  # (def. and type of refl)" $
+      check_ (ctx [<]) sone reflDef reflTy
   ],
 
   "misc" :- [
-    testTC "funext"
-           {globals = fromList
-              [("A", mkAbstract Zero $ TYPE 0),
-               ("B", mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
-               ("f", mkAbstract Any  $
-                  Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0),
-               ("g", mkAbstract Any  $
-                  Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0)]} $
-      -- 0·A : Type, 0·B : ω·A → Type,
-      -- ω·f, g : (ω·x : A) → B x
-      -- ⊢
-      -- 0·funext : (ω·eq : (0·x : A) → f x ≡ g x) → f ≡ g
-      --          = λ eq ⇒ λᴰ i ⇒ λ x ⇒ eq x i
-      check_ (ctx [<]) szero
+    note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
+    note "⊢",
+    note "1 · λ x y xy ⇒ λᴰ i ⇒ p (xy i)",
+    note "  ⇐ (0·x, y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
+    testTC "cong" $
+      check_ (ctx [<]) sone
+        (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
+        (Pi Zero "x"  (FT "A") $ TUsed $
+         Pi Zero "y"  (FT "A") $ TUsed $
+         Pi One  "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $ TUsed $
+         Eq "i" (DUsed $ E $ F "P" :@ E (BV 0 :% BV 0))
+                (E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
+    note "0·A : Type, 0·P : ω·A → Type,",
+    note "ω·p, q : (1·x : A) → P x",
+    note "⊢",
+    note "1 · λ eq ⇒ λᴰ i ⇒ λ x ⇒ eq x i",
+    note "    ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
+    testTC "funext" $
+      check_ (ctx [<]) sone
         (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
-        (Pi Any "eq"
-            (Pi Zero "x" (FT "A") $ TUsed $
-              Eq0 (E $ F "B" :@ BVT 0)
-                  (E $ F "f" :@ BVT 0) (E $ F "g" :@ BVT 0)) $ TUsed $
-         Eq0 (Pi Any "x" (FT "A") $ TUsed $ E $ F "B" :@ BVT 0)
-             (FT "f") (FT "g"))
+        (Pi One "eq"
+            (Pi One "x" (FT "A") $ TUsed $
+              Eq0 (E $ F "P" :@ BVT 0)
+                  (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)) $ TUsed $
+         Eq0 (Pi Any "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0)
+             (FT "p") (FT "q"))
   ]
 ]