From a5ccf0215ab0ac9f212227d2f86606a28442d376 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 15 Apr 2023 15:13:01 +0200
Subject: [PATCH] coercions and compositions

---
 examples/misc.quox                 |  14 +-
 lib/Quox/Context.idr               |  14 +
 lib/Quox/Equal.idr                 | 249 +++++-----
 lib/Quox/Parser/FromParser.idr     |  26 +-
 lib/Quox/Parser/Lexer.idr          |   1 +
 lib/Quox/Parser/Parser.idr         |  38 +-
 lib/Quox/Parser/Syntax.idr         |   3 +
 lib/Quox/Pretty.idr                |   2 +-
 lib/Quox/Reduce.idr                | 711 ++++++++++++++++++++++-------
 lib/Quox/Syntax/Dim.idr            |   6 +-
 lib/Quox/Syntax/DimEq.idr          |   7 +-
 lib/Quox/Syntax/Term/Base.idr      |  73 ++-
 lib/Quox/Syntax/Term/Pretty.idr    | 137 ++++--
 lib/Quox/Syntax/Term/Subst.idr     |  56 ++-
 lib/Quox/Syntax/Term/TyConKind.idr |  34 ++
 lib/Quox/Typechecker.idr           |  74 ++-
 lib/Quox/Typing.idr                | 162 +++----
 lib/Quox/Typing/Context.idr        |  37 ++
 lib/Quox/Typing/Error.idr          | 183 +++++---
 lib/quox-lib.ipkg                  |   3 +-
 tests/TermImpls.idr                |  47 +-
 tests/Tests/PrettyTerm.idr         |  27 +-
 tests/Tests/Reduce.idr             |  79 ++--
 tests/Tests/Typechecker.idr        |   3 +-
 tests/TypingImpls.idr              |   9 +-
 25 files changed, 1344 insertions(+), 651 deletions(-)
 create mode 100644 lib/Quox/Syntax/Term/TyConKind.idr

diff --git a/examples/misc.quox b/examples/misc.quox
index 4d540f1..c36305b 100644
--- a/examples/misc.quox
+++ b/examples/misc.quox
@@ -1,4 +1,3 @@
-
 def0 Pred : 0.★₀ → ★₁ = λ A ⇒ 0.A → ★₀;
 
 def0 All : 0.(A : ★₀) → 0.(Pred A) → ★₁ =
@@ -23,3 +22,16 @@ defω funext :
     1.(All A (eq-f A P p q)) →
     p ≡ q : All A P =
   λ A P p q eq ⇒ δ i ⇒ λ x ⇒ eq x @i;
+
+def0 T : ω.{true, false} → ★₀ =
+  λ b ⇒ caseω b return ★₀ of { 'true ⇒ {tt}; 'false ⇒ {} };
+
+defω absurd :
+    0.('true ≡ 'false : {true, false}) → 0.(A : ★₀) → A =
+  λ eq A ⇒
+    case0 coe [i ⇒ T (eq @i)] @0 @1 'tt return A of { };
+
+defω sym : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) →
+           1.(x ≡ y : A) → y ≡ x : A =
+  λ A x y eq ⇒ δ i ⇒
+    comp [A] @0 @1 (eq @0) @i { 0 j ⇒ eq @j; 1 _ ⇒ eq @0 };
diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 450406a..683cf67 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -66,6 +66,11 @@ parameters {0 tm : Nat -> Type} (f : forall n. tm n -> a)
     toListAcc [<]        acc = acc
     toListAcc (tel :< t) acc = toListAcc tel (f t :: acc)
 
+  export
+  toSnocVectWith : Context tm n -> SnocVect n a
+  toSnocVectWith [<]        = [<]
+  toSnocVectWith (tel :< t) = toSnocVectWith tel :< f t
+
 export %inline
 toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
 toSnocList = toSnocListWith (Evidence _)
@@ -82,6 +87,15 @@ export %inline
 toList' : Telescope' a _ _ -> List a
 toList' = toListWith id
 
+export %inline
+toSnocVect : Context tm n -> SnocVect n (Exists tm)
+toSnocVect = toSnocVectWith (Evidence _)
+
+export %inline
+toSnocVect' : Context' a n -> SnocVect n a
+toSnocVect' = toSnocVectWith id
+
+
 
 export
 fromSnocVect : SnocVect n a -> Context' a n
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 8070a13..0092376 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -70,38 +70,38 @@ sameTyCon (E    {}) (E    {}) = True
 sameTyCon (E    {}) _         = False
 
 
-parameters (defs : Definitions)
-  ||| true if a type is known to be a subsingleton purely by its form.
-  ||| a subsingleton is a type with only zero or one possible values.
-  ||| equality/subtyping accepts immediately on values of subsingleton types.
-  |||
-  ||| * a function type is a subsingleton if its codomain is.
-  ||| * a pair type is a subsingleton if both its elements are.
-  ||| * all equality types are subsingletons because uip is admissible by
-  |||   boundary separation.
-  ||| * an enum type is a subsingleton if it has zero or one tags.
-  public export covering
-  isSubSing : Has ErrorEff fs =>
-              {n : Nat} -> Term 0 n -> Eff fs Bool
-  isSubSing ty0 = do
-    Element ty0 nc <- whnfT defs ty0
-    case ty0 of
-      TYPE _          => pure False
-      Pi   {res, _}   => isSubSing res.term
-      Lam  {}         => pure False
-      Sig  {fst, snd} => isSubSing fst `andM` isSubSing snd.term
-      Pair {}         => pure False
-      Enum tags       => pure $ length (SortedSet.toList tags) <= 1
-      Tag  {}         => pure False
-      Eq   {}         => pure True
-      DLam {}         => pure False
-      Nat             => pure False
-      Zero            => pure False
-      Succ {}         => pure False
-      BOX  {ty, _}    => isSubSing ty
-      Box  {}         => pure False
-      E    (s :# _)   => isSubSing s
-      E    _          => pure False
+||| true if a type is known to be a subsingleton purely by its form.
+||| a subsingleton is a type with only zero or one possible values.
+||| equality/subtyping accepts immediately on values of subsingleton types.
+|||
+||| * a function type is a subsingleton if its codomain is.
+||| * a pair type is a subsingleton if both its elements are.
+||| * equality types are subsingletons because of uip.
+||| * an enum type is a subsingleton if it has zero or one tags.
+||| * 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
+  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
+    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
+    E    _   => pure False
+    Lam  _   => pure False
+    Pair _ _ => pure False
+    Tag  _   => pure False
+    DLam _   => pure False
+    Zero     => pure False
+    Succ _   => pure False
+    Box  _   => pure False
 
 
 export
@@ -112,6 +112,17 @@ ensureTyCon ctx t = case nchoose $ isTyConE t of
   Left  y => pure y
   Right n => throw $ NotType (toTyContext ctx) (t // shift0 ctx.dimLen)
 
+||| performs the minimum work required to recompute the type of an elim.
+|||
+||| ⚠ **assumes the elim is already typechecked.** ⚠
+private covering
+computeElimTypeE : (defs : Definitions) -> EqContext n ->
+                   (e : Elim 0 n) -> (0 ne : NotRedex defs e) =>
+                   Equal (Term 0 n)
+computeElimTypeE defs ectx e =
+  let Val n = ectx.termLen in
+  rethrow $ computeElimType defs (toWhnfContext ectx) e
+
 parameters (defs : Definitions)
   mutual
     namespace Term
@@ -124,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 <- whnfT defs ty
-          Element s  ns  <- whnfT defs s
-          Element t  nt  <- whnfT defs t
+          Element ty nty <- whnf defs ctx ty
+          Element s  ns  <- whnf defs ctx s
+          Element t  nt  <- whnf defs ctx t
           tty <- ensureTyCon ctx ty
           compare0' ctx ty s t
 
@@ -134,7 +145,7 @@ parameters (defs : Definitions)
       ||| a lambda "Γ ⊢ λx ⇒ t" that has been converted to "Γ, x ⊢ t".
       private %inline
       toLamBody : Elim d n -> Term d (S n)
-      toLamBody e = E $ weakE e :@ BVT 0
+      toLamBody e = E $ weakE 1 e :@ BVT 0
 
       private covering
       compare0' : EqContext n ->
@@ -209,7 +220,8 @@ parameters (defs : Definitions)
       compare0' _ (Eq {}) _ _ =
         -- ✨ uip ✨
         --
-        -- Γ ⊢ e = f : Eq [i ⇒ A] s t
+        -- ----------------------------
+        --  Γ ⊢ e = f : Eq [i ⇒ A] s t
         pure ()
 
       compare0' ctx Nat s t = local_ Equal $
@@ -263,8 +275,8 @@ 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 <- whnfT defs s
-      Element t nt <- whnfT defs t
+      Element s ns <- whnf defs ctx s
+      Element t nt <- whnf defs ctx t
       ts <- ensureTyCon ctx s
       tt <- ensureTyCon ctx t
       st <- either pure (const $ clashTy ctx s t) $
@@ -336,37 +348,12 @@ parameters (defs : Definitions)
       -- has been inlined by whnf
       Elim.compare0 ctx e f
 
-    ||| performs the minimum work required to recompute the type of an elim.
-    |||
-    ||| ⚠ **assumes the elim is already typechecked.** ⚠
-    private covering
-    computeElimType : EqContext n -> (e : Elim 0 n) ->
-                      (0 ne : NotRedex defs e) ->
-                      Equal (Term 0 n)
-    computeElimType ctx (F x) _ = do
-      def <- lookupFree x defs
-      let Val n = ctx.termLen
-      pure $ def.type
-    computeElimType ctx (B i) _ = pure $ ctx.tctx !! i
-    computeElimType ctx (f :@ s) ne = do
-      (_, arg, res) <- expectPiE defs ctx !(computeElimType ctx f (noOr1 ne))
-      pure $ sub1 res (s :# arg)
-    computeElimType ctx (CasePair {pair, ret, _}) _ = pure $ sub1 ret pair
-    computeElimType ctx (CaseEnum {tag, ret, _}) _ = pure $ sub1 ret tag
-    computeElimType ctx (CaseNat {nat, ret, _}) _ = pure $ sub1 ret nat
-    computeElimType ctx (CaseBox {box, ret, _}) _ = pure $ sub1 ret box
-    computeElimType ctx (f :% p) ne = do
-      (ty, _, _) <- expectEqE defs ctx !(computeElimType ctx f (noOr1 ne))
-      pure $ dsub1 ty p
-    computeElimType ctx (TypeCase {ret, _}) _ = pure ret
-    computeElimType ctx (_ :# ty) _ = pure ty
-
     private covering
     replaceEnd : EqContext n ->
                  (e : Elim 0 n) -> DimConst -> (0 ne : NotRedex defs e) ->
                  Equal (Elim 0 n)
     replaceEnd ctx e p ne = do
-      (ty, l, r) <- expectEqE defs ctx !(computeElimType ctx e ne)
+      (ty, l, r) <- expectEq defs ctx !(computeElimTypeE defs ctx e)
       pure $ ends l r p :# dsub1 ty (K p)
 
     namespace Elim
@@ -382,10 +369,10 @@ parameters (defs : Definitions)
       compare0 ctx e f =
         wrapErr (WhileComparingE ctx !mode e f) $ do
           let Val n = ctx.termLen
-          Element e ne <- whnfT defs e
-          Element f nf <- whnfT defs f
+          Element e ne <- whnf defs ctx e
+          Element f nf <- whnf defs ctx f
           -- [fixme] there is a better way to do this "isSubSing" stuff for sure
-          unless !(isSubSing defs !(computeElimType ctx e ne)) $
+          unless !(isSubSing defs ctx !(computeElimTypeE defs ctx e)) $
             compare0' ctx e f ne nf
 
       private covering
@@ -411,7 +398,8 @@ parameters (defs : Definitions)
       compare0' ctx (e :@ s) (f :@ t) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          (_, arg, _) <- expectPiE defs ctx !(computeElimType ctx e (noOr1 ne))
+          (_, arg, _) <- expectPi defs ctx =<<
+                         computeElimTypeE defs ctx e @{noOr1 ne}
           Term.compare0 ctx arg s t
       compare0' ctx e@(_ :@ _) f _ _ = clashE ctx e f
 
@@ -419,9 +407,9 @@ parameters (defs : Definitions)
                     (CasePair fpi f fret fbody) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimType ctx e (noOr1 ne)
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          (fst, snd) <- expectSigE defs ctx ety
+          (fst, snd) <- expectSig defs ctx ety
           let [< x, y] = ebody.names
           Term.compare0 (extendTyN [< (epi, x, fst), (epi, y, snd.term)] ctx)
                         (substCasePairRet ety eret)
@@ -433,9 +421,9 @@ parameters (defs : Definitions)
                     (CaseEnum fpi f fret farms) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimType ctx e (noOr1 ne)
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          for_ !(expectEnumE defs ctx ety) $ \t =>
+          for_ !(expectEnum defs ctx ety) $ \t =>
             compare0 ctx (sub1 eret $ Tag t :# ety)
               !(lookupArm t earms) !(lookupArm t farms)
           expectEqualQ epi fpi
@@ -450,7 +438,7 @@ parameters (defs : Definitions)
                     (CaseNat fpi fpi' f fret fzer fsuc) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimType ctx e (noOr1 ne)
+          ety <- computeElimTypeE 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
@@ -465,9 +453,9 @@ parameters (defs : Definitions)
                     (CaseBox fpi f fret fbody) ne nf =
         local_ Equal $ do
           compare0 ctx e f
-          ety <- computeElimType ctx e (noOr1 ne)
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          (q, ty) <- expectBOXE defs ctx ety
+          (q, ty) <- expectBOX defs ctx ety
           compare0 (extendTy (epi * q) ebody.name ty ctx)
             (substCaseBoxRet ety eret)
             ebody.term fbody.term
@@ -475,50 +463,93 @@ parameters (defs : Definitions)
       compare0' ctx e@(CaseBox {}) f _ _ = clashE ctx e f
 
       compare0' ctx (s :# a) (t :# b) _ _ =
-          Term.compare0 ctx !(bigger a b) s t
-        where
-          bigger : forall a. a -> a -> Equal a
-          bigger l r = mode <&> \case Super => l; _ => r
+        let ty = case !mode of Super => a; _ => b in
+        Term.compare0 ctx ty s t
 
-      compare0' ctx (TypeCase ty1 ret1 univ1 pi1 sig1 enum1 eq1 nat1 box1)
-                    (TypeCase ty2 ret2 univ2 pi2 sig2 enum2 eq2 nat2 box2)
+      compare0' ctx (Coe ty1 p1 q1 (E val1)) (Coe ty2 p2 q2 (E val2)) ne nf = do
+        compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2)
+        compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2)
+        compare0 ctx val1 val2
+      compare0' ctx e@(Coe {}) f _ _ = clashE ctx e f
+
+      compare0' ctx (Comp _ _ _ _ (K _) _ _) _ ne _ = void $ absurd $ noOr2 ne
+      compare0' ctx (Comp _ _ _ _ (B i) _ _) _ _ _ = absurd i
+      compare0' ctx _ (Comp _ _ _ _ (K _) _ _) _ nf = void $ absurd $ noOr2 nf
+
+      compare0' ctx (TypeCase ty1 ret1 arms1 def1)
+                    (TypeCase ty2 ret2 arms2 def2)
                     ne _ =
         local_ Equal $ do
           compare0 ctx ty1 ty2
-          u <- expectTYPEE defs ctx =<< computeElimType ctx ty1 (noOr1 ne)
+          u <- expectTYPE defs ctx =<<
+               computeElimTypeE defs ctx ty1 @{noOr1 ne}
           compareType ctx ret1 ret2
-          compare0 ctx univ1 univ2 ret1
-          let [< piA, piB] = pi1.names
-              piCtx = extendTyN
-                [< (Zero, piA, TYPE u),
-                   (Zero, piB, Arr Zero (BVT 0) (TYPE u))] ctx
-              ret1_2 = weakT ret1 {by = 2}
-          compare0 piCtx pi1.term  pi2.term  ret1_2
-          let [< sigA, sigB] = sig1.names
-              sigCtx = extendTyN
-                [< (Zero, sigA, TYPE u),
-                   (Zero, sigB, Arr Zero (BVT 0) (TYPE u))] ctx
-          compare0 sigCtx sig1.term sig2.term ret1_2
-          compare0 ctx enum1 enum2 ret1
-          let [< eqA0, eqA1, eqA, eqL, eqR] = eq1.names
-              eqCtx = extendTyN
-                [< (Zero, eqA0, TYPE u),
-                   (Zero, eqA1, TYPE u),
-                   (Zero, eqA,  Eq0 (TYPE u) (BVT 1) (BVT 0)),
-                   (Zero, eqL,  BVT 2),
-                   (Zero, eqR,  BVT 2)] ctx
-              ret1_5 = weakT ret1 {by = 5}
-          compare0 eqCtx eq1.term eq2.term ret1_5
-          compare0 ctx nat1 nat2 ret1
-          let boxCtx = extendTy Zero box1.name (TYPE u) ctx
-              ret1_1 = weakT ret1
-          compare0 boxCtx box1.term box2.term ret1_1
+          compareType ctx def1 def2
+          for_ allKinds $ \k =>
+            compareArm ctx k ret1 u
+              (lookupPrecise k arms1) (lookupPrecise k arms2) def1
       compare0' ctx e@(TypeCase {}) f _ _ = clashE ctx e f
 
       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' ctx e@(_ :# _) f        _ _ = clashE ctx e f
 
+      ||| compare two type-case branches, which came from the arms of the given
+      ||| kind. `ret` is the return type of the case expression, and `u` is the
+      ||| universe the head is in.
+      private covering
+      compareArm : EqContext n -> (k : TyConKind) ->
+                   (ret : Term 0 n) -> (u : Universe) ->
+                   (b1, b2 : Maybe (TypeCaseArmBody k 0 n)) ->
+                   (def : Term 0 n) ->
+                   Equal ()
+      compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
+      compareArm ctx k ret u b1 b2 def =
+        let def = SN def in
+        compareArm_ ctx k ret u (fromMaybe def b1) (fromMaybe def b2)
+
+      private covering
+      compareArm_ : EqContext n -> (k : TyConKind) ->
+                    (ret : Term 0 n) -> (u : Universe) ->
+                    (b1, b2 : TypeCaseArmBody k 0 n) ->
+                    Equal ()
+      compareArm_ ctx KTYPE ret u b1 b2 =
+        compare0 ctx ret b1.term b2.term
+
+      compareArm_ ctx KPi ret u b1 b2 = do
+        let [< a, b] = b1.names
+            ctx = extendTyN
+              [< (Zero, a, TYPE u),
+                 (Zero, b, Arr Zero (BVT 0) (TYPE u))] ctx
+        compare0 ctx (weakT 2 ret) b1.term b2.term
+
+      compareArm_ ctx KSig ret u b1 b2 = do
+        let [< a, b] = b1.names
+            ctx = extendTyN
+              [< (Zero, a, TYPE u),
+                 (Zero, b, Arr Zero (BVT 0) (TYPE u))] ctx
+        compare0 ctx (weakT 2 ret) b1.term b2.term
+
+      compareArm_ ctx KEnum ret u b1 b2 =
+        compare0 ctx ret b1.term b2.term
+
+      compareArm_ ctx KEq ret u b1 b2 = do
+        let [< a0, a1, a, l, r] = b1.names
+            ctx = extendTyN
+              [< (Zero, a0, TYPE u),
+                 (Zero, a1, TYPE u),
+                 (Zero, a,  Eq0 (TYPE u) (BVT 1) (BVT 0)),
+                 (Zero, l,  BVT 2),
+                 (Zero, r,  BVT 2)] ctx
+        compare0 ctx (weakT 5 ret) b1.term b2.term
+
+      compareArm_ ctx KNat ret u b1 b2 =
+        compare0 ctx ret b1.term b2.term
+
+      compareArm_ ctx KBOX ret u b1 b2 = do
+        let ctx = extendTy Zero b1.name (TYPE u) ctx
+        compare0 ctx (weakT 1 ret) b1.term b1.term
+
 
 parameters {auto _ : (Has DefsReader fs, Has ErrorEff fs)} (ctx : TyContext d n)
   -- [todo] only split on the dvars that are actually used anywhere in
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index c7b7701..34ba61b 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -99,13 +99,13 @@ mutual
       Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t
 
     Case pi pair (r, ret) (CasePair (x, y) body) =>
-      map E $ Base.CasePair pi
+      map E $ CasePair pi
         <$> fromPTermElim ds ns pair
         <*> fromPTermTScope ds ns [< r] ret
         <*> fromPTermTScope ds ns [< x, y] body
 
     Case pi tag (r, ret) (CaseEnum arms) =>
-      map E $ Base.CaseEnum pi
+      map E $ CaseEnum pi
         <$> fromPTermElim ds ns tag
         <*> fromPTermTScope ds ns [< r] ret
         <*> assert_total fromPTermEnumArms ds ns arms
@@ -115,7 +115,7 @@ mutual
     Succ n => [|Succ $ fromPTermWith ds ns n|]
 
     Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc)) =>
-      Prelude.map E $ Base.CaseNat pi pi'
+      map E $ CaseNat pi pi'
         <$> fromPTermElim ds ns nat
         <*> fromPTermTScope ds ns [< r] ret
         <*> fromPTermWith ds ns zer
@@ -143,7 +143,7 @@ mutual
     Box val => Box <$> fromPTermWith ds ns val
 
     Case pi box (r, ret) (CaseBox b body) =>
-      Prelude.map E $ CaseBox pi
+      map E $ CaseBox pi
         <$> fromPTermElim ds ns box
         <*> fromPTermTScope ds ns [< r] ret
         <*> fromPTermTScope ds ns [< b] body
@@ -157,6 +157,24 @@ mutual
     s :# a =>
       map E $ (:#) <$> fromPTermWith ds ns s <*> fromPTermWith ds ns a
 
+    Coe (i, ty) p q val =>
+      map E $ Coe
+        <$> fromPTermDScope ds ns [< i] ty
+        <*> fromPDimWith ds p
+        <*> fromPDimWith ds q
+        <*> fromPTermWith ds ns val
+
+    -- [todo] direct translation for homo comp?
+    Comp (i, ty) p q val r (j0, val0) (j1, val1) =>
+      map E $ CompH
+        <$> fromPTermDScope ds ns [< i] ty
+        <*> fromPDimWith ds p
+        <*> fromPDimWith ds q
+        <*> fromPTermWith ds ns val
+        <*> fromPDimWith ds r
+        <*> fromPTermDScope ds ns [< j0] val0
+        <*> fromPTermDScope ds ns [< j1] val1
+
   private
   fromPTermEnumArms : Has (Except Error) fs =>
                       Context' BName d -> Context' BName n ->
diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr
index 22f5f6b..2760f53 100644
--- a/lib/Quox/Parser/Lexer.idr
+++ b/lib/Quox/Parser/Lexer.idr
@@ -197,6 +197,7 @@ reserved =
    Sym "★" `Or` Word "Type",
    Word "ℕ" `Or` Word "Nat",
    Word1 "zero", Word1 "succ",
+   Word1 "coe", Word1 "comp",
    Word1 "def",
    Word1 "def0",
    Word "defω" `Or` Word "def#",
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index aaafdc7..b066f7e 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -177,7 +177,7 @@ optNameBinder = [|join $ optional $ bname <* darr|]
 mutual
   export covering
   term : Grammar True PTerm
-  term = lamTerm <|> caseTerm <|> bindTerm <|> annTerm
+  term = lamTerm <|> caseTerm <|> coeTerm <|> compTerm <|> bindTerm <|> annTerm
 
   private covering
   lamTerm : Grammar True PTerm
@@ -190,6 +190,30 @@ mutual
            (resC "return" *> optBinderTerm)
            (resC "of"     *> caseBody)|]
 
+  private covering
+  coeTerm : Grammar True PTerm
+  coeTerm = resC "coe" *> [|Coe typeLine dimArg dimArg aTerm|]
+
+  private covering
+  compTerm : Grammar True PTerm
+  compTerm = resC "comp" *> do
+    head <- [|Comp typeLine dimArg dimArg aTerm dimArg|]
+    uncurry head <$> compBody
+  where
+    compBranch : Grammar True (DimConst, BName, PTerm)
+    compBranch = [|(,,) dimConst bname (resC "⇒" *> term)|]
+
+    zeroOne : (DimConst, a) -> (DimConst, a) -> Grammar False (a, a)
+    zeroOne (Zero, x) (One,  y) = pure (x, y)
+    zeroOne (One,  x) (Zero, y) = pure (y, x)
+    zeroOne _ _ = fatalError "body of comp needs one 0 branch and one 1 branch"
+
+    compBody : Grammar True ((BName, PTerm), (BName, PTerm))
+    compBody = braces $ do
+      et0 <- compBranch <* resC ";"
+      et1 <- compBranch <* optional (resC ";")
+      zeroOne et0 et1
+
   private covering
   caseBody : Grammar True PCaseBody
   caseBody = braces $
@@ -251,14 +275,14 @@ mutual
   private covering
   appTerm : Grammar True PTerm
   appTerm = resC "★"    *> [|TYPE nat|]
-        <|> resC "Eq"   *> [|Eq (bracks optBinderTerm) aTerm aTerm|]
+        <|> resC "Eq"   *> [|Eq typeLine aTerm aTerm|]
         <|> resC "succ" *> [|Succ aTerm|]
         <|> [|apply aTerm (many appArg)|]
   where
     data PArg = TermArg PTerm | DimArg PDim
 
     appArg : Grammar True PArg
-    appArg = [|DimArg $ resC "@" *> dim|] <|> [|TermArg aTerm|]
+    appArg = [|DimArg dimArg|] <|> [|TermArg aTerm|]
 
     apply : PTerm -> List PArg -> PTerm
     apply = foldl apply1 where
@@ -266,6 +290,14 @@ mutual
       apply1 f (TermArg x) = f :@ x
       apply1 f (DimArg  p) = f :% p
 
+  private covering
+  typeLine : Grammar True (BName, PTerm)
+  typeLine = bracks optBinderTerm
+
+  private covering
+  dimArg : Grammar True PDim
+  dimArg = resC "@" *> dim
+
   private covering
   aTerm : Grammar True PTerm
   aTerm = [|Enum $ braces $ commaSep bareTag|]
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index 1b2d78f..cdb3ed4 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -54,6 +54,9 @@ namespace PTerm
 
       | V PName
       | (:#) PTerm PTerm
+
+      | Coe (BName, PTerm) PDim PDim PTerm
+      | Comp (BName, PTerm) PDim PDim PTerm PDim (BName, PTerm) (BName, PTerm)
     %name PTerm s, t
 
     public export
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index fd6c1ee..e4f100e 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -87,7 +87,7 @@ bracks = delims "[" "]"
 ||| includes spaces inside the braces
 export %inline
 braces : Doc HL -> Doc HL
-braces doc = hl Delim "{" <++> doc <++> hl Delim "}"
+braces doc = hl Delim "{" <++> nest 2 doc <++> hl Delim "}"
 
 export %inline
 parensIf : Bool -> Doc HL -> Doc HL
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 8268032..1b39cc6 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -3,6 +3,8 @@ module Quox.Reduce
 import Quox.No
 import Quox.Syntax
 import Quox.Definition
+import Quox.Typing.Context
+import Quox.Typing.Error
 import Data.SnocVect
 import Data.Maybe
 import Data.List
@@ -10,36 +12,35 @@ import Data.List
 %default total
 
 
-||| errors that might happen if you pass an ill typed expression into
-||| whnf. don't do that please
-public export
-data WhnfError = MissingEnumArm TagVal (List TagVal)
-
-
 public export
 0 RedexTest : TermLike -> Type
 RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
 
 public export
-interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) (0 err : Type) | tm
+interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
-  whnf : {d, n : Nat} -> (defs : Definitions) ->
-         tm d n -> Either err (Subset (tm d n) (No . isRedex defs))
+  whnf : {d, n : Nat} -> (defs : Definitions) -> (ctx : WhnfContext d n) ->
+         tm d n -> Either Error (Subset (tm d n) (No . isRedex 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
 
 public export
-0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex err =>
+0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex =>
                       Definitions -> Pred (tm d n)
 IsRedex  defs = So . isRedex defs
 NotRedex defs = No . isRedex defs
 
 public export
 0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
-             Whnf tm isRedex err =>
-             (d, n : Nat) -> (defs : Definitions) -> Type
+             Whnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
 NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
 
 public export %inline
-nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex err) =>
+nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) =>
        (t : tm d n) -> (0 nr : NotRedex defs t) =>
        NonRedex tm d n defs
 nred t = Element t nr
@@ -48,32 +49,38 @@ nred t = Element t nr
 public export %inline
 isLamHead : Elim {} -> Bool
 isLamHead (Lam {} :# Pi {}) = True
+isLamHead (Coe {})          = True
 isLamHead _                 = False
 
 public export %inline
 isDLamHead : Elim {} -> Bool
 isDLamHead (DLam {} :# Eq {}) = True
+isDLamHead (Coe {})           = True
 isDLamHead _                  = False
 
 public export %inline
 isPairHead : Elim {} -> Bool
 isPairHead (Pair {} :# Sig {}) = True
+isPairHead (Coe {})            = True
 isPairHead _                   = False
 
 public export %inline
 isTagHead : Elim {} -> Bool
 isTagHead (Tag t :# Enum _) = True
+isTagHead (Coe {})          = True
 isTagHead _ = False
 
 public export %inline
 isNatHead : Elim {} -> Bool
 isNatHead (Zero   :# Nat) = True
 isNatHead (Succ n :# Nat) = True
+isNatHead (Coe {})        = True
 isNatHead _ = False
 
 public export %inline
 isBoxHead : Elim {} -> Bool
 isBoxHead (Box {} :# BOX {}) = True
+isBoxHead (Coe {})           = True
 isBoxHead _ = False
 
 public export %inline
@@ -88,36 +95,41 @@ isAnn _        = False
 
 ||| true if a term is syntactically a type.
 public export %inline
-isTyCon : (t : Term {}) -> Bool
-isTyCon (TYPE  {}) = True
-isTyCon (Pi    {}) = True
-isTyCon (Lam   {}) = False
-isTyCon (Sig   {}) = True
-isTyCon (Pair  {}) = False
-isTyCon (Enum  {}) = True
-isTyCon (Tag   {}) = False
-isTyCon (Eq    {}) = True
-isTyCon (DLam  {}) = False
-isTyCon Nat        = True
-isTyCon Zero       = False
-isTyCon (Succ  {}) = False
-isTyCon (BOX   {}) = True
-isTyCon (Box   {}) = False
-isTyCon (E     {}) = False
-isTyCon (CloT  {}) = False
-isTyCon (DCloT {}) = False
+isTyCon : Term {} -> Bool
+isTyCon (TYPE     {}) = True
+isTyCon (Pi       {}) = True
+isTyCon (Lam      {}) = False
+isTyCon (Sig      {}) = True
+isTyCon (Pair     {}) = False
+isTyCon (Enum     {}) = True
+isTyCon (Tag      {}) = False
+isTyCon (Eq       {}) = True
+isTyCon (DLam     {}) = False
+isTyCon Nat           = True
+isTyCon Zero          = False
+isTyCon (Succ     {}) = False
+isTyCon (BOX      {}) = True
+isTyCon (Box      {}) = False
+isTyCon (E        {}) = False
+isTyCon (CloT     {}) = False
+isTyCon (DCloT    {}) = False
 
 ||| true if a term is syntactically a type, or a neutral.
 public export %inline
-isTyConE : (t : Term {}) -> Bool
+isTyConE : Term {} -> Bool
 isTyConE s = isTyCon s || isE s
 
 ||| true if a term is syntactically a type.
 public export %inline
-isAnnTyCon : (t : Elim {}) -> Bool
+isAnnTyCon : Elim {} -> Bool
 isAnnTyCon (ty :# TYPE _) = isTyCon ty
 isAnnTyCon _              = False
 
+public export %inline
+isK : Dim d -> Bool
+isK (K _) = True
+isK _     = False
+
 
 mutual
   public export
@@ -135,102 +147,332 @@ mutual
     isRedexE defs nat || isNatHead nat
   isRedexE defs (CaseBox {box, _}) =
     isRedexE defs box || isBoxHead box
-  isRedexE defs (f :% _) =
-    isRedexE defs f || isDLamHead f
+  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 (TypeCase {ty, _}) =
-    isRedexE defs ty || isAnnTyCon ty
+  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
 
   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 defs (E e)              = isAnn e || isRedexE defs e
+  isRedexT _    _                  = False
+
+
+public export
+tycaseRhs : (k : TyConKind) -> TypeCaseArms d n ->
+            Maybe (ScopeTermN (arity k) d n)
+tycaseRhs k arms = lookupPrecise k arms
+
+public export
+tycaseRhsDef : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
+               ScopeTermN (arity k) d n
+tycaseRhsDef def k arms = fromMaybe (SN def) $ tycaseRhs k arms
+
+public export
+tycaseRhs0 : (k : TyConKind) -> TypeCaseArms d n ->
+             (0 eq : arity k = 0) => Maybe (Term d n)
+tycaseRhs0 k arms {eq} with (tycaseRhs k arms) | (arity k)
+  tycaseRhs0 k arms {eq = Refl} | res | 0 = map (.term) res
+
+public export
+tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
+                (0 eq : arity k = 0) => Term d n
+tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms
+
+
+
+private
+weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n)
+weakDS by (S names (Y body)) = S names $ Y $ weakT by body
+weakDS by (S names (N body)) = S names $ N $ weakT by body
+
+private
+dweakS : (by : Nat) -> ScopeTerm d n -> ScopeTerm (by + d) n
+dweakS by (S names (Y body)) = S names $ Y $ dweakT by body
+dweakS by (S names (N body)) = S names $ N $ dweakT by body
+
+private
+coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d ->
+            ScopeTermN s d n -> ScopeTermN s d n
+coeScoped ty p q (S names (Y body)) =
+  S names $ Y $ E $ Coe (weakDS s ty) p q body
+coeScoped ty p q (S names (N body)) =
+  S names $ N $ E $ Coe ty p q body
+
 
 mutual
+  parameters {d, n : Nat} (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)) =>
+                      Either Error (Term d n)
+    computeElimType (F x) = do
+      let Just def = lookup 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}
+        | t => Left $ ExpectedPi ctx.names t
+      pure $ sub1 res (s :# arg)
+    computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair
+    computeElimType (CaseEnum {tag, ret, _}) = pure $ sub1 ret tag
+    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}
+        | t => Left $ ExpectedEq ctx.names t
+      pure $ dsub1 ty p
+    computeElimType (Coe {ty, q, _}) = pure $ dsub1 ty q
+    computeElimType (Comp {ty, _}) = pure ty
+    computeElimType (TypeCase {ret, _}) = pure ret
+    computeElimType (_ :# ty) = pure ty
+
+  parameters {d, n : Nat} (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)) =>
+               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}
+      let arg  = E $ typeCase1 e ty KPi [< "Arg", "Ret"] (BVT 1)
+          res' = typeCase1 e (Arr Zero arg ty) KPi [< "Arg", "Ret"] (BVT 0)
+          res  = SY [< "Arg"] $ E $ weakE 1 res' :@ BVT 0
+      pure (arg, res)
+    tycasePi t = Left $ ExpectedPi ctx.names t
+
+    ||| 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
+    tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT 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}
+      let fst  = E $ typeCase1 e ty KSig [< "Fst", "Snd"] (BVT 1)
+          snd' = typeCase1 e (Arr Zero fst ty) KSig [< "Fst", "Snd"] (BVT 0)
+          snd  = SY [< "Fst"] $ E $ weakE 1 snd' :@ BVT 0
+      pure (fst, snd)
+    tycaseSig t = Left $ ExpectedSig ctx.names t
+
+    ||| for [π. A], returns A;
+    ||| 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)) =>
+                Either Error (Term (S d) n)
+    tycaseBOX (BOX _ a) = pure a
+    tycaseBOX (E e) {tnf} = do
+      ty <- computeElimType defs ctx e @{noOr2 tnf}
+      pure $ E $ typeCase1 e ty KBOX [< "Ty"] (BVT 0)
+    tycaseBOX t = Left $ ExpectedBOX ctx.names t
+
+    ||| for Eq [i ⇒ A] l r, returns (A‹0/i›, A‹1/i›, A, l, r);
+    ||| 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)) =>
+               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}
+      let names = [< "A0", "A1", "A", "L", "R"]
+          a0 = E $ typeCase1 e ty KEq names (BVT 4)
+          a1 = E $ typeCase1 e ty KEq names (BVT 3)
+          a' = typeCase1 e (Eq0 ty a0 a1) KEq names (BVT 2)
+          a  = SY [< "i"] $ E $ dweakE 1 a' :% BV 0
+          l  = E $ typeCase1 e a0 KEq names (BVT 1)
+          r  = E $ typeCase1 e a1 KEq names (BVT 0)
+      pure (a0, a1, a, l, r)
+    tycaseEq t = Left $ ExpectedEq ctx.names t
+
+
+  parameters {d, n : Nat} (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))
+    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›)
+      --   where 𝒔‹j› ≔ coe [i ⇒ A] @q @j s
+      --
+      -- type-case is used to expose A,B if the type is neutral
+      let ctx1 = extendDimN i ctx
+      Element ty tynf <- whnf defs ctx1 ty.term
+      (arg, res) <- tycasePi defs ctx1 ty
+      let s0   = Coe (SY i arg) q p s
+          body = E $ (val :# (ty // one p)) :@ E s0
+          s1   = Coe (SY i (arg // (BV 0 ::: shift 2))) (weakD 1 q) (BV 0)
+                     (s // shift 1)
+      whnf defs ctx $ Coe (SY 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))
+    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 }
+      -- ⇝
+      -- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
+      -- of { (a, b) ⇒
+      --   e[(coe [i ⇒ A] @p @q a)/a,
+      --     (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @q b)/b] }
+      --
+      -- type-case is used to expose A,B if the type is neutral
+      let ctx1 = extendDimN i ctx
+      Element ty tynf <- whnf defs ctx1 ty.term
+      (tfst, tsnd) <- tycaseSig defs ctx1 ty
+      let a' = Coe (SY i $ weakT 2 tfst) p q (BVT 1)
+          tsnd' = tsnd.term //
+            (Coe (SY i $ weakT 2 $ tfst // (BV 0 ::: shift 2))
+              (weakD 1 p) (BV 0) (BVT 1) ::: shift 2)
+          b' = Coe (SY i tsnd') p q (BVT 0)
+      whnf defs ctx $ CasePair qty (val :# (ty // one p)) ret $
+        SY 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))
+    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 = extendDimN j ctx
+      Element ty tynf <- whnf defs ctx1 ty.term
+      (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
+      let a'   = SY j $ dsub1 a (weakD 1 r)
+          val' = E $ (val :# (ty // one p)) :% r
+      whnf defs ctx $ CompH a' p q val' r (SY j s) (SY 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))
+    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 = extendDimN i ctx
+      Element ty tynf <- whnf defs ctx1 ty.term
+      ta <- tycaseBOX defs ctx1 ty
+      let a' = Coe (SY i $ weakT 1 ta) p q $ BVT 0
+      whnf defs ctx $ CaseBox qty (val :# (ty // one p)) ret $
+        SY body.names $ body.term // (a' ::: shift 1)
+
+
   export covering
-  Whnf Elim Reduce.isRedexE WhnfError where
-    whnf defs (F x) with (lookupElim x defs) proof eq
-      _ | Just y  = whnf defs y
+  Whnf Elim Reduce.isRedexE where
+    whnf defs ctx (F x) with (lookupElim x defs) proof eq
+      _ | Just y  = whnf 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 (f :@ s) = do
-      Element f fnf <- whnf defs f
+    whnf defs ctx (f :@ s) = do
+      Element f fnf <- whnf defs ctx f
       case nchoose $ isLamHead f of
-        Left _ =>
-          let Lam body :# Pi {arg, res, _} = f
-              s = s :# arg
-          in
-          whnf defs $ sub1 body s :# sub1 res s
+        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
         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 (CasePair pi pair ret body) = do
-      Element pair pairnf <- whnf defs pair
+    whnf defs ctx (CasePair pi pair ret body) = do
+      Element pair pairnf <- whnf defs ctx pair
       case nchoose $ isPairHead pair of
-        Left _ =>
-          let Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} = pair
-              fst = fst :# tfst
-              snd = snd :# sub1 tsnd fst
-          in
-          whnf defs $ subN body [< fst, snd] :# sub1 ret pair
+        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
+          Coe ty p q val => do
+            sigCoe defs ctx pi ty p q val ret body
         Right np =>
-          pure $ Element (CasePair pi pair ret body)
-                         (pairnf `orNo` 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 (CaseEnum pi tag ret arms) = do
-      Element tag tagnf <- whnf defs tag
+    whnf defs ctx (CaseEnum pi tag ret arms) = do
+      Element tag tagnf <- whnf defs ctx tag
       case nchoose $ isTagHead tag of
-        Left t =>
-          let Tag t :# Enum ts = tag
-              ty = sub1 ret tag
-          in
-          case lookup t arms of
-            Just arm => whnf defs $ arm :# ty
-            Nothing  => Left $ MissingEnumArm t (keys arms)
+        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
+              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
         Right nt =>
           pure $ Element (CaseEnum pi tag ret arms) $ tagnf `orNo` nt
 
     -- case zero ∷ ℕ return p ⇒ C of { zero ⇒ u; … } ⇝
     --   u ∷ C[zero∷ℕ/p]
     --
-    -- case succ n ∷ ℕ return p ⇒ C of { succ n' [π.ih] ⇒ u; … } ⇝
+    -- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
     --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
-    whnf defs (CaseNat pi piIH nat ret zer suc) = do
-      Element nat natnf <- whnf defs nat
+    whnf defs ctx (CaseNat pi piIH nat ret zer suc) = do
+      Element nat natnf <- whnf defs ctx nat
       case nchoose $ isNatHead nat of
         Left _ =>
           let ty = sub1 ret nat in
           case nat of
-            Zero :# Nat => whnf defs (zer :# ty)
+            Zero :# Nat => whnf 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 $ tm :# ty
+              whnf 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
         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 (CaseBox pi box ret body) = do
-      Element box boxnf <- whnf defs box
+    whnf defs ctx (CaseBox pi box ret body) = do
+      Element box boxnf <- whnf defs ctx box
       case nchoose $ isBoxHead box of
-        Left _ =>
-          let Box val :# BOX q bty = box
-              ty = sub1 ret box
-          in
-          whnf defs $ sub1 body (val :# bty) :# ty
+        Left _ => case box of
+          Box val :# BOX q bty =>
+            let ty = sub1 ret box in
+            whnf defs ctx $ sub1 body (val :# bty) :# ty
+          Coe ty p q val =>
+            boxCoe defs ctx pi ty p q val ret body
         Right nb =>
           pure $ Element (CaseBox pi box ret body) $ boxnf `orNo` nb
 
@@ -238,114 +480,231 @@ mutual
     -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @1 ⇝ u ∷ A‹1/𝑗›
     -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
     --   (if 𝑘 is a variable)
-    whnf defs (f :% p) = do
-      Element f fnf <- whnf defs f
+    whnf defs ctx (f :% p) = do
+      Element f fnf <- whnf defs ctx f
       case nchoose $ isDLamHead f of
-        Left _ =>
-          let DLam body :# Eq {ty = ty, l, r, _} = f
-              body = endsOr l r (dsub1 body p) p
-          in
-          whnf defs $ body :# dsub1 ty p
-        Right ndlh =>
-          pure $ Element (f :% p) $ fnf `orNo` ndlh
+        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
+          Coe ty p' q' val =>
+            eqCoe 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
+              | ty => Left $ ExpectedEq ctx.names ty
+            whnf 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 (s :# a) = do
-      Element s snf <- whnf defs s
+    whnf defs ctx (s :# a) = do
+      Element s snf <- whnf 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 a
+          Element a anf <- whnf defs ctx a
           pure $ Element (s :# a) $ ne `orNo` snf `orNo` anf
 
-    -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
-    --
-    -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
-    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
-    --
-    -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
-    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
-    --
-    -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
-    --
-    -- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q of {
-    --     Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
-    -- s[(A‹0/i› ∷ ★ᵢ)/a₀, (A‹1/i› ∷ ★ᵢ)/a₁,
-    --   ((δ i ⇒ A) ∷ Eq [★ᵢ] A‹0/i› A‹1/i›)/a,
-    --   (L ∷ A‹0/i›)/l, (R ∷ A‹1/i›)/r] ∷ Q
-    --
-    -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
-    --
-    -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
-    whnf defs (TypeCase {ty, ret, univ, pi, sig, enum, eq, nat, box}) = do
-      Element ty tynf <- whnf defs ty
+    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 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
+      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
+        Right nk => do
+          Element ty tynf <- whnf 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
       case nchoose $ isAnnTyCon ty of
-        Left y =>
-          let ty :# TYPE u = ty in
-          case ty of
-            TYPE _ =>
-              whnf defs $ univ :# ret
-            Pi _ arg res =>
-              let arg = arg :# TYPE u
-                  res = toLam res :# Arr Zero (TYPE u) (TYPE u)
-              in
-              whnf defs $ subN pi [< arg, res] :# ret
-            Sig fst snd =>
-              let fst = fst :# TYPE u
-                  snd = toLam snd :# Arr Zero (TYPE u) (TYPE u)
-              in
-              whnf defs $ subN sig [< fst, snd] :# ret
-            Enum _ =>
-              whnf defs $ enum :# ret
-            Eq a l r =>
-              let a0' = a.zero; a1' = a.one
-                  a0 = a0' :# TYPE u
-                  a1 = a1' :# TYPE u
-                  a  = toDLam a :# Eq0 (TYPE u) a0' a1'
-                  l  = l :# a0'
-                  r  = r :# a1'
-              in
-              whnf defs $ subN eq [< a0, a1, a, l, r] :# ret
-            Nat =>
-              whnf defs $ nat :# ret
-            BOX _ s =>
-              whnf defs $ sub1 box (s :# TYPE u) :# ret
-        Right nt => pure $
-          Element (TypeCase {ty, ret, univ, pi, sig, enum, eq, nat, box}) $
-            tynf `orNo` nt
-    where
-      toLam : {s : Nat} -> ScopeTermN s d n -> Term d n
-      toLam (S names body) = names :\\ body.term
+        Left  y  => let ty :# TYPE u = ty in
+                    reduceTypeCase defs ctx ty u ret arms def
+        Right nt => pure $ Element (TypeCase ty ret arms def) $
+                             tynf `orNo` retnf `orNo` nt
 
-      toDLam : {s : Nat} -> DScopeTermN s d n -> Term d n
-      toDLam (S names body) = names :\\% body.term
-
-    whnf defs (CloE  el th) = whnf defs $ pushSubstsWith' id th el
-    whnf defs (DCloE el th) = whnf defs $ pushSubstsWith' th id el
+    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
 
   export covering
-  Whnf Term Reduce.isRedexT WhnfError 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 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
 
     -- s ∷ A ⇝ s   (in term context)
-    whnf defs (E e) = do
-      Element e enf <- whnf defs e
+    whnf defs ctx (E e) = do
+      Element e enf <- whnf 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 (CloT  tm th) = whnf defs $ pushSubstsWith' id th tm
-    whnf defs (DCloT tm th) = whnf defs $ pushSubstsWith' th id tm
+    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
+
+  ||| reduce a type-case applied to a type constructor
+  private covering
+  reduceTypeCase : {d, n : Nat} -> (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
+    -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
+    TYPE _ =>
+      whnf 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] ∷ ★ᵢ
+    Pi _ arg res =>
+      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
+
+    -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
+    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
+    Sig fst snd =>
+      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
+
+    -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
+    Enum _ =>
+      whnf defs ctx $ tycaseRhsDef0 def KEnum arms :# ret
+
+    -- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q
+    --  of { Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
+    -- s[(A‹0/i› ∷ ★ᵢ)/a₀, (A‹1/i› ∷ ★ᵢ)/a₁,
+    --   ((δ i ⇒ A) ∷ Eq [★ᵢ] A‹0/i› A‹1/i›)/a,
+    --   (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 $
+        subN (tycaseRhsDef def KEq arms)
+          [< a0 :# TYPE u, a1 :# TYPE u,
+             DLam a :# Eq0 (TYPE u) a0 a1, l :# a0, r :# a1]
+        :# ret
+
+    -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
+    Nat =>
+      whnf 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
+
+  ||| pushes a coercion inside a whnf-ed term
+  private covering
+  pushCoe : {n, d : Nat} -> (defs : Definitions) -> WhnfContext d n ->
+            BaseName ->
+            (ty : Term (S d) n) -> (0 tynf : No (isRedexT 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
+    case s of
+      -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
+      TYPE {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
+      Pi   {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
+      Sig  {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
+      Enum {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
+      Eq   {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
+      Nat     => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
+      BOX  {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
+
+      -- just η expand it. then whnf for (:@) will handle it later
+      -- this is how @xtt does it
+      Lam body => do
+        let body' = Coe (SY [< i] ty) p q (Lam body)
+            term' = Lam (SY [< "y"] $ E $ weakE 1 body' :@ BVT 0)
+            type' = ty // one q
+        whnf defs ctx $ term' :# type'
+
+      {-
+      -- maybe:
+      -- (coe [i ⇒ π.(x : A) → B] @p @q (λ x ⇒ s)) ⇝
+      -- (λ x ⇒ coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @q @i x)/x]] @p @q s)
+      --   ∷ (π.(x: A‹q/i›) → B‹q/i›)
+      Lam body => do
+        let Pi {qty, arg, res} = ty
+          | _ => Left $ ?err
+        let arg' = SY [< "j"] $ weakT 1 $ arg // (BV 0 ::: shift 2)
+            res' = SY [< i] $ res.term //
+                      (Coe arg' (weakD 1 q) (BV 0) (BVT 0) ::: shift 1)
+            body = SY body.names $ E $ Coe res' p q body.term
+        pure $ Element (Lam body :# Pi qty (arg // one q) (res // one q)) Ah
+      -}
+
+      -- (coe [i ⇒ (x : A) × B] @p @q (s, t)) ⇝
+      -- (coe [i ⇒ A] @p @q s,
+      --  coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i s)/x]] @p @q t)
+      --   ∷ (x : A‹q/i›) × B‹q/i›
+      --
+      -- can't use η here because... it doesn't exist
+      Pair fst snd => do
+        let Sig {fst = tfst, snd = tsnd} = ty
+          | _ => Left $ ExpectedSig (extendDim i ctx.names) ty
+        let fst'  = E $ Coe (SY [< i] tfst) p q fst
+            tfst' = SY [< "j"] $ tfst `CanDSubst.(//)` (BV 0 ::: shift 2)
+            tsnd' = SY [< i] $ sub1 tsnd $
+                      Coe tfst' (weakD 1 p) (BV 0) $ dweakT 1 fst
+            snd'  = E $ Coe tsnd' p q snd
+        pure $
+          Element (Pair fst' snd' :# Sig (tfst // one q) (tsnd // one q)) Ah
+
+      -- η expand like λ
+      DLam body => do
+        let body' = Coe (SY [< i] ty) p q (DLam body)
+            term' = DLam (SY [< "j"] $ E $ dweakE 1 body' :% BV 0)
+            type' = ty // one q
+        whnf defs ctx $ term' :# type'
+
+      -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
+      Tag tag => do
+        let Enum ts = ty
+          | _ => Left $ ExpectedEnum (extendDim i ctx.names) ty
+        pure $ Element (Tag tag :# Enum ts) Ah
+
+      -- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ)
+      Zero   => pure $ Element (Zero :# Nat) Ah
+      Succ t => pure $ Element (Succ t :# Nat) Ah
+
+      -- (coe [i ⇒ [π.A]] @p @q [s]) ⇝
+      -- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›]
+      Box val => do
+        let BOX {qty, ty = a} = ty
+          | _ => Left $ ExpectedBOX (extendDim i ctx.names) ty
+        let a = SY [< i] a
+        pure $ Element (Box (E $ Coe a p q s) :# BOX qty (dsub1 a q)) Ah
+
+      E e => pure $ Element (Coe (SY [< i] ty) p q (E e)) (snf `orNo` Ah)
+  where
+    unwrapTYPE : Term (S d) n -> Either Error Universe
+    unwrapTYPE (TYPE u) = pure u
+    unwrapTYPE ty       = Left $ ExpectedTYPE (extendDim i ctx.names) ty
diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index bf3d1ca..826b1df 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -22,7 +22,7 @@ data DimConst = Zero | One
 
 ||| `ends l r e` returns `l` if `e` is `Zero`, or `r` if it is `One`.
 public export
-ends : a -> a -> DimConst -> a
+ends : Lazy a -> Lazy a -> DimConst -> a
 ends l r Zero = l
 ends l r One  = r
 
@@ -130,5 +130,5 @@ BV i = B $ V i
 
 
 export
-weakD : {default 1 by : Nat} -> Dim d -> Dim (by + d)
-weakD p = p // shift by
+weakD : (by : Nat) -> Dim d -> Dim (by + d)
+weakD by p = p // shift by
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index adeecf4..2359181 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -63,6 +63,11 @@ ifConsistent : Applicative f => (eqs : DimEq d) -> f a -> f (IfConsistent eqs a)
 ifConsistent ZeroIsOne act = pure Nothing
 ifConsistent (C _)     act = Just <$> act
 
+public export
+toMaybe : IfConsistent eqs a -> Maybe a
+toMaybe Nothing  = Nothing
+toMaybe (Just x) = Just x
+
 
 export
 fromGround' : Context' DimConst d -> DimEq' d
@@ -245,7 +250,7 @@ PrettyHL (DimEq' d) where
     go [<]              = pure [<]
     go (eqs :< Nothing) = local {dnames $= tail} $ go eqs
     go (eqs :< Just p)  = do
-      eq  <- prettyCst (BV {d = 1} 0) (weakD p)
+      eq  <- prettyCst (BV {d = 1} 0) (weakD 1 p)
       eqs <- local {dnames $= tail} $ go eqs
       pure $ eqs :< eq
 
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 9e06b60..2a874ad 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -5,6 +5,7 @@ import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst
 import public Quox.Syntax.Qty
 import public Quox.Syntax.Dim
+import public Quox.Syntax.Term.TyConKind
 import public Quox.Name
 import public Quox.Context
 
@@ -17,33 +18,35 @@ import Data.Nat
 import public Data.So
 import Data.String
 import public Data.SortedMap
+import public Data.SortedMap.Dependent
 import public Data.SortedSet
 
 %default total
 
 
 public export
-0 TermLike : Type
+TermLike : Type
 TermLike = Nat -> Nat -> Type
 
 public export
-0 TSubstLike : Type
+TSubstLike : Type
 TSubstLike = Nat -> Nat -> Nat -> Type
 
 public export
-0 Universe : Type
+Universe : Type
 Universe = Nat
 
 public export
-0 TagVal : Type
+TagVal : Type
 TagVal = String
 
+
 infixl 8 :#
 infixl 9 :@, :%
 mutual
   public export
-  0 TSubst : TSubstLike
-  TSubst d = Subst $ Elim d
+  TSubst : TSubstLike
+  TSubst d = Subst $ \n => Elim d n
 
   ||| first argument `d` is dimension scope size;
   ||| second `n` is term scope size
@@ -138,16 +141,19 @@ mutual
     ||| type-annotated term
     (:#) : (tm, ty : Term d n) -> Elim d n
 
-    ||| match on types (needed for coercions :mario_flop:)
-    TypeCase : (ty   : Elim d n) ->
-               (ret  : Term d n) ->
-               (univ : Term d n) ->
-               (pi   : ScopeTermN 2 d n) ->
-               (sig  : ScopeTermN 2 d n) ->
-               (enum : Term d n) ->
-               (eq   : ScopeTermN 5 d n) ->
-               (nat  : Term d n) ->
-               (box  : ScopeTerm d n) ->
+    ||| coerce a value along a type equality, or show its coherence
+    ||| [@xtt; §2.1.1]
+    Coe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
+          (val : Term d n) -> Elim d n
+
+    ||| "generalised composition" [@xtt; §2.1.2]
+    Comp : (ty : Term d n) -> (p, q : Dim d) ->
+           (val : Term d n) -> (r : Dim d) ->
+           (zero, one : DScopeTerm d n) -> Elim d n
+
+    ||| match on types. needed for b.s. of coercions [@xtt; §2.2]
+    TypeCase : (ty : Elim d n) -> (ret : Term d n) ->
+               (arms : TypeCaseArms d n) -> (def : Term d n) ->
                Elim d n
 
     ||| term closure/suspended substitution
@@ -158,9 +164,22 @@ mutual
             Elim dto n
 
   public export
-  0 CaseEnumArms : TermLike
+  CaseEnumArms : TermLike
   CaseEnumArms d n = SortedMap TagVal (Term d n)
 
+  public export
+  TypeCaseArms : TermLike
+  TypeCaseArms d n = SortedDMap TyConKind (\k => TypeCaseArmBody k d n)
+
+  public export
+  TypeCaseArm : TermLike
+  TypeCaseArm d n = (k ** TypeCaseArmBody k d n)
+
+  public export
+  TypeCaseArmBody : TyConKind -> TermLike
+  TypeCaseArmBody k = ScopeTermN (arity k)
+
+
   ||| a scoped term with names
   public export
   record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
@@ -174,15 +193,16 @@ mutual
     N : (body : f n)       -> ScopedBody s f n
 
   public export
-  0 ScopeTermN, DScopeTermN : Nat -> TermLike
+  ScopeTermN, DScopeTermN : Nat -> TermLike
   ScopeTermN  s d n = Scoped s (Term d) n
   DScopeTermN s d n = Scoped s (\d => Term d n) d
 
   public export
-  0 ScopeTerm, DScopeTerm : TermLike
+  ScopeTerm, DScopeTerm : TermLike
   ScopeTerm  = ScopeTermN 1
   DScopeTerm = DScopeTermN 1
 
+
 %name Term s, t, r
 %name Elim e, f
 %name Scoped body
@@ -260,6 +280,19 @@ makeNat : Nat -> Term d n
 makeNat 0 = Zero
 makeNat (S k) = Succ $ makeNat k
 
-public export
+public export %inline
 enum : List TagVal -> Term d n
 enum = Enum . SortedSet.fromList
+
+public export %inline
+typeCase : Elim d n -> Term d n ->
+           List (TypeCaseArm d n) -> Term d n -> Elim d n
+typeCase ty ret arms def = TypeCase ty ret (fromList arms) def
+
+public export %inline
+typeCase1 : Elim d n -> Term d n ->
+            (k : TyConKind) -> NContext (arity k) -> Term d (arity k + n) ->
+            {default Nat def : Term d n} ->
+            Elim d n
+typeCase1 ty ret k ns body {def} =
+  typeCase ty ret [(k ** SY ns body)] def
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 4ffa82b..356c112 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -15,22 +15,22 @@ export %inline
 typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD :
   Pretty.HasEnv m => m (Doc HL)
 typeD   = hlF Syntax $ ifUnicode "★" "Type"
-arrowD  = hlF Syntax $ ifUnicode "→" "->"
-darrowD = hlF Syntax $ ifUnicode "⇒" "=>"
-timesD  = hlF Syntax $ ifUnicode "×" "**"
+arrowD  = hlF Delim  $ ifUnicode "→" "->"
+darrowD = hlF Delim  $ ifUnicode "⇒" "=>"
+timesD  = hlF Delim  $ ifUnicode "×" "**"
 lamD    = hlF Syntax $ ifUnicode "λ" "fun"
-eqndD   = hlF Syntax $ ifUnicode "≡" "=="
+eqndD   = hlF Delim  $ ifUnicode "≡" "=="
 dlamD   = hlF Syntax $ ifUnicode "δ" "dfun"
-annD    = hlF Syntax $ ifUnicode "∷" "::"
+annD    = hlF Delim  $ ifUnicode "∷" "::"
 natD    = hlF Syntax $ ifUnicode "ℕ" "Nat"
 
 export %inline
 eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
-ofD, dotD, zeroD, succD : Doc HL
+ofD, dotD, zeroD, succD, coeD, compD : Doc HL
 eqD       = hl Syntax "Eq"
-colonD    = hl Syntax ":"
-commaD    = hl Syntax ","
-semiD     = hl Syntax ";"
+colonD    = hl Delim  ":"
+commaD    = hl Delim  ","
+semiD     = hl Delim  ";"
 caseD     = hl Syntax "case"
 typecaseD = hl Syntax "type-case"
 ofD       = hl Syntax "of"
@@ -38,6 +38,8 @@ returnD   = hl Syntax "return"
 dotD      = hl Delim "."
 zeroD     = hl Syntax "zero"
 succD     = hl Syntax "succ"
+coeD      = hl Syntax "coe"
+compD     = hl Syntax "compD"
 
 
 export
@@ -138,10 +140,10 @@ prettyTuple = map (parens . align . separate commaD) . traverse prettyM
 
 export
 prettyArms : PrettyHL a => Pretty.HasEnv m =>
-             List (SnocList BaseName, Doc HL, a) -> m (Doc HL)
-prettyArms =
+             BinderSort -> List (SnocList BaseName, Doc HL, a) -> m (Doc HL)
+prettyArms s =
   map (braces . aseparate semiD) .
-  traverse (\(xs, l, r) => prettyArm T xs l r)
+  traverse (\(xs, l, r) => prettyArm s xs l r)
 
 export
 prettyCase' : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
@@ -153,7 +155,7 @@ prettyCase' intro elim r ret arms = do
   ret   <- case r of
     Unused => pretty0M ret
     _      => prettyLams Nothing T [< r] ret
-  arms  <- prettyArms arms
+  arms  <- prettyArms T arms
   pure $ asep [intro <++> elim, returnD <++> ret, ofD <++> arms]
 
 export
@@ -192,6 +194,12 @@ export
 prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
 prettyBoxVal val = bracks <$> pretty0M val
 
+export
+prettyCompPat : Pretty.HasEnv m => Dim d -> DimConst -> BaseName -> m (Doc HL)
+prettyCompPat s e j = pure $
+  hsep [parens (hsep [!(pretty0M s), hl Syntax "=", !(pretty0M e)]),
+        !(pretty0M $ DV j)]
+
 export
 toNatLit : Term d n -> Maybe Nat
 toNatLit Zero     = Just 0
@@ -210,58 +218,77 @@ parameters (showSubsts : Bool)
   where
     prettyM (TYPE l) =
       parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
+
     prettyM (Pi qty s (S _ (N t))) = do
       dom <- pretty0M $ MkWithQty qty s
       cod <- withPrec AnnR $ prettyM t
       parensIfM AnnR $ asep [dom <++> !arrowD, cod]
+
     prettyM (Pi qty s (S [< x] (Y t))) =
       prettyBindType (Just qty) x s !arrowD t
+
     prettyM (Lam (S x t)) =
       let GotLams {names, body, _} = getLams' x t.term Refl in
       prettyLams (Just !lamD) T (toSnocList' names) body
+
     prettyM (Sig s (S _ (N t))) = do
       s <- withPrec InTimes $ prettyM s
       t <- withPrec Times   $ prettyM t
       parensIfM Times $ asep [s <++> !timesD, t]
+
     prettyM (Sig s (S [< x] (Y t))) =
       prettyBindType Nothing x s !timesD t
+
     prettyM (Pair s t) =
       let GotPairs {init, last, _} = getPairs' [< s] t in
       prettyTuple $ toList $ init :< last
+
     prettyM (Enum tags) =
       pure $ delims "{" "}" . aseparate comma $ map prettyTagBare $
         Prelude.toList tags
+
     prettyM (Tag t) =
       pure $ prettyTag t
+
     prettyM (Eq (S _ (N ty)) l r) = do
       l  <- withPrec InEq $ prettyM l
       r  <- withPrec InEq $ prettyM r
       ty <- withPrec InEq $ prettyM ty
       parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty]
+
     prettyM (Eq (S [< i] (Y ty)) l r) = do
       prettyApps Nothing (L eqD)
         [epretty $ MkTypeLine i ty, epretty l, epretty r]
+
     prettyM (DLam (S i t)) =
       let GotDLams {names, body, _} = getDLams' i t.term Refl in
       prettyLams (Just !dlamD) D (toSnocList' names) body
+
     prettyM Nat = natD
+
     prettyM Zero = pure $ hl Syntax "0"
+
     prettyM (Succ n) =
       case toNatLit n of
         Just n  => pure $ hl Syntax $ pretty $ S n
         Nothing => prettyApps Nothing (L succD) [n]
+
     prettyM (BOX pi ty) = do
       pi <- pretty0M pi
       ty <- pretty0M ty
       pure $ bracks $ hcat [pi, dotD, align ty]
+
     prettyM (Box val) = prettyBoxVal val
+
     prettyM (E e) = prettyM e
+
     prettyM (CloT s th) =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
           [|withPrec SApp (prettyM s) <%> prettyTSubst th|]
       else
         prettyM $ pushSubstsWith' id th s
+
     prettyM (DCloT s th) =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
@@ -274,61 +301,97 @@ parameters (showSubsts : Bool)
   where
     prettyM (F x) =
       hl' Free <$> prettyM x
+
     prettyM (B i) =
       prettyVar TVar TVarErr (!ask).tnames i
+
     prettyM (e :@ s) =
       let GotArgs {fun, args, _} = getArgs' e [s] in
       prettyApps Nothing fun args
+
     prettyM (CasePair pi p (S [< r] ret) (S [< x, y] body)) = do
       pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y]
       prettyCase pi p r ret.term [([< x, y], pat, body.term)]
+
     prettyM (CaseEnum pi t (S [< r] ret) arms) =
       prettyCase pi t r ret.term
         [([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
+
     prettyM (CaseNat pi pi' nat (S [< r] ret) zer (S [< s, ih] suc)) =
       prettyCase pi nat r ret.term
         [([<],       zeroD,    eterm zer),
          ([< s, ih], !succPat, eterm suc.term)]
-      where
-        succPat : m (Doc HL)
-        succPat = case (ih, pi') of
-          (Unused, Zero) => pure $ succD <++> !(pretty0M s)
-          _ => pure $ asep [succD <++> !(pretty0M s) <+> comma,
-                            !(pretty0M $ MkWithQty pi' ih)]
+    where
+      succPat : m (Doc HL)
+      succPat = case (ih, pi') of
+        (Unused, Zero) => pure $ succD <++> !(pretty0M s)
+        _ => pure $ asep [succD <++> !(pretty0M s) <+> comma,
+                          !(pretty0M $ MkWithQty pi' ih)]
+
     prettyM (CaseBox pi box (S [< r] ret) (S [< u] body)) =
       prettyCase pi box r ret.term
         [([< u], !(prettyBoxVal $ TV u), body.term)]
+
     prettyM (e :% d) =
       let GotDArgs {fun, args, _} = getDArgs' e [d] in
       prettyApps (Just "@") fun args
+
     prettyM (s :# a) = do
       s <- withPrec AnnL $ prettyM s
       a <- withPrec AnnR $ prettyM a
       parensIfM AnnR $ hang 2 $ s <++> !annD <%%> a
-    prettyM (TypeCase ty ret univ
-                (S [< piA, piB] pi) (S [< sigA, sigB] sig) enum
-                (S [< eqA0, eqA1, eqA, eqL, eqR] eq)
-                nat (S [< boxA] box)) = do
-      let v : BaseName -> Doc HL := pretty0 True . TV
-      pipat  <- pure $ parens $ hsep [v piA,  !arrowD, v piB]
-      sigpat <- pure $ parens $ hsep [v sigA, !timesD, v sigB]
-      eqpat  <- prettyApps Nothing (L eqD)
-                  [TV eqA0, TV eqA1, TV eqA, TV eqL, TV eqR]
-      boxpat <- pure $ bracks $ v boxA
-      prettyCase' typecaseD ty Unused ret
-        [([<], !typeD, eterm univ),
-         ([< piA, piB], pipat, eterm pi.term),
-         ([< sigA, sigB], sigpat, eterm sig.term),
-         ([<], hl Syntax "{}", eterm enum),
-         ([< eqA0, eqA1, eqA, eqL, eqR], eqpat, eterm eq.term),
-         ([<], !natD, eterm nat),
-         ([< boxA], boxpat, eterm box.term)]
+
+    prettyM (Coe (S [< i] ty) p q val) =
+      let ty = case ty of
+            Y ty => epretty $ MkTypeLine i ty
+            N ty => epretty ty
+      in
+      prettyApps' (L coeD)
+        [(Nothing,  ty),
+         (Just "@", epretty p),
+         (Just "@", epretty q),
+         (Nothing,  epretty val)]
+
+    prettyM (Comp ty p q val r (S [< z] zero) (S [< o] one)) = do
+      apps <- prettyApps' (L compD)
+        [(Nothing,  epretty ty),
+         (Just "@", epretty p),
+         (Just "@", epretty q),
+         (Nothing,  epretty val)]
+      arms <- prettyArms D
+        [([< z], !(prettyCompPat r Zero z), zero.term),
+         ([< o], !(prettyCompPat r One  o), one.term)]
+      pure $ apps <++> arms
+
+    prettyM (TypeCase ty ret arms def) = do
+      arms <- traverse fromArm (toList arms)
+      prettyCase' typecaseD ty Unused ret $
+        arms ++ [([<], hl Syntax "_", eterm def)]
+    where
+      v : BaseName -> Doc HL
+      v = pretty0 True . TV
+
+      tyCasePat : (k : TyConKind) -> NContext (arity k) -> m (Doc HL)
+      tyCasePat KTYPE [<] = typeD
+      tyCasePat KPi   [< a, b] = pure $ parens $ hsep [v a, !arrowD, v b]
+      tyCasePat KSig  [< a, b] = pure $ parens $ hsep [v a, !arrowD, v b]
+      tyCasePat KEnum [<]   = pure $ hl Syntax "{}"
+      tyCasePat KEq   vars  = prettyApps Nothing (L eqD) $ map TV $ toList' vars
+      tyCasePat KNat  [<]   = natD
+      tyCasePat KBOX  [< a] = pure $ bracks $ v a
+
+      fromArm : TypeCaseArm d n ->
+                m (SnocList BaseName, Doc HL, Exists (Term d))
+      fromArm (k ** S ns t) =
+        pure (toSnocList' ns, !(tyCasePat k ns), eterm t.term)
+
     prettyM (CloE e th)  =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
           [|withPrec SApp (prettyM e) <%> prettyTSubst th|]
       else
         prettyM $ pushSubstsWith' id th e
+
     prettyM (DCloE e th) =
       if showSubsts then
         parensIfM SApp . hang 2 =<<
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 7a7097a..3444feb 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -130,21 +130,21 @@ comp th ps ph = map (// th) ps . ph
 
 
 public export %inline
-dweakT : {by : Nat} -> Term d n -> Term (by + d) n
-dweakT t = t // shift by
+dweakT : (by : Nat) -> Term d n -> Term (by + d) n
+dweakT by t = t // shift by
 
 public export %inline
-dweakE : {by : Nat} -> Elim d n -> Elim (by + d) n
-dweakE t = t // shift by
+dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
+dweakE by t = t // shift by
 
 
 public export %inline
-weakT : {default 1 by : Nat} -> Term d n -> Term d (by + n)
-weakT t = t // shift by
+weakT : (by : Nat) -> Term d n -> Term d (by + n)
+weakT by t = t // shift by
 
 public export %inline
-weakE : {default 1 by : Nat} -> Elim d n -> Elim d (by + n)
-weakE t = t // shift by
+weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
+weakE by t = t // shift by
 
 
 parameters {s : Nat}
@@ -152,7 +152,7 @@ parameters {s : Nat}
     export %inline
     (.term) : ScopedBody s (Term d) n -> Term d (s + n)
     (Y b).term = b
-    (N b).term = weakT b {by = s}
+    (N b).term = weakT s b
 
   namespace ScopeTermN
     export %inline
@@ -163,7 +163,7 @@ parameters {s : Nat}
     export %inline
     (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
     (Y b).term = b
-    (N b).term = dweakT b {by = s}
+    (N b).term = dweakT s b
 
   namespace DScopeTermN
     export %inline
@@ -305,13 +305,37 @@ mutual
       nclo $ (f // th // ph) :% (d // th)
     pushSubstsWith th ph (s :# a) =
       nclo $ (s // th // ph) :# (a // th // ph)
-    pushSubstsWith th ph (TypeCase ty ret univ pi sig enum eq nat box) =
-      nclo $ TypeCase (ty   // th // ph) (ret  // th // ph)
-                      (univ // th // ph) (pi   // th // ph)
-                      (sig  // th // ph) (enum // th // ph)
-                      (eq   // th // ph) (nat  // th // ph)
-                      (box  // th // ph)
+    pushSubstsWith th ph (Coe ty p q val) =
+      nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph)
+    pushSubstsWith th ph (Comp ty p q val r zero one) =
+      nclo $ Comp (ty // th // ph) (p // th) (q // th)
+                  (val // th // ph) (r // th)
+                  (zero // th // ph) (one // th // ph)
+    pushSubstsWith th ph (TypeCase ty ret arms def) =
+      nclo $ TypeCase (ty // th // ph) (ret  // th // ph)
+        (map (\t => t // th // ph) arms) (def // th // ph)
     pushSubstsWith th ph (CloE e ps) =
       pushSubstsWith th (comp th ps ph) e
     pushSubstsWith th ph (DCloE e ps) =
       pushSubstsWith (ps . th) ph e
+
+
+||| heterogeneous composition, using Comp and Coe (and subst)
+|||
+||| comp [i ⇒ A] @p @q s { (r=0) j ⇒ t₀; (r=1) j ⇒ t₁ }
+||| ≔
+||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) {
+|||   (r=0) j ⇒ coe [i ⇒ A] @j @q t₀;
+|||   (r=1) j ⇒ coe [i ⇒ A] @j @q t₁
+||| }
+public export %inline
+CompH : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
+        (r : Dim d) -> (zero, one : DScopeTerm d n) -> Elim d n
+CompH {ty, p, q, val, r, zero, one} =
+  let ty' = SY ty.names $ ty.term // (B VZ ::: shift 2) in
+  Comp {
+    ty = dsub1 ty q, p, q,
+    val = E $ Coe ty p q val, r,
+    zero = SY zero.names $ E $ Coe ty' (B VZ) (weakD 1 q) zero.term,
+    one  = SY one.names  $ E $ Coe ty' (B VZ) (weakD 1 q) one.term
+  }
diff --git a/lib/Quox/Syntax/Term/TyConKind.idr b/lib/Quox/Syntax/Term/TyConKind.idr
new file mode 100644
index 0000000..6bacf77
--- /dev/null
+++ b/lib/Quox/Syntax/Term/TyConKind.idr
@@ -0,0 +1,34 @@
+module Quox.Syntax.Term.TyConKind
+
+import Decidable.Equality
+import Derive.Prelude
+import Generics.Derive
+
+%language ElabReflection
+%default total
+
+
+public export
+data TyConKind = KTYPE | KPi | KSig | KEnum | KEq | KNat | KBOX
+%name TyConKind k
+%runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq]
+
+||| a list of all `TyConKind`s
+public export %inline
+allKinds : List TyConKind
+allKinds = %runElab do
+  -- as a script so it stays up to date if there are more tycon kinds
+  cs <- getCons $ fst !(lookupName "TyConKind")
+  traverse (check . var) cs
+
+
+||| in `type-case`, how many variables are bound in this branch
+public export %inline
+arity : TyConKind -> Nat
+arity KTYPE = 0
+arity KPi   = 2
+arity KSig  = 2
+arity KEnum = 0
+arity KEq   = 5
+arity KNat  = 0
+arity KBOX  = 1
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index ce3b968..9d337d4 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -56,6 +56,20 @@ addNames0 : Context (Term d . (+ n)) s -> NContext s -> CtxExtension d n (s + n)
 addNames0 [<] [<] = [<]
 addNames0 (ts :< t) (xs :< x) = addNames0 ts xs :< (Zero, x, t)
 
+export
+typecaseTel : (k : TyConKind) -> Universe -> CtxExtension0' (arity k) d n
+typecaseTel k u = case k of
+  KTYPE => [<]
+  -- A : ★ᵤ, B : 0.A → ★ᵤ
+  KPi => [< TYPE u, Arr Zero (BVT 0) (TYPE u)]
+  KSig => [< TYPE u, Arr Zero (BVT 0) (TYPE u)]
+  KEnum => [<]
+  -- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
+  KEq => [< TYPE u, TYPE u, Eq0 (TYPE u) (BVT 1) (BVT 0), BVT 2, BVT 2]
+  KNat => [<]
+  -- A : ★ᵤ
+  KBOX => [< TYPE u]
+
 
 mutual
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
@@ -291,7 +305,7 @@ mutual
                  ScopeTermN s d n -> Term d n -> TC ()
   check0ScopeN ctx ext (S _     (N body)) ty = check0 ctx body ty
   check0ScopeN ctx ext (S names (Y body)) ty =
-    check0 (extendTyN (addNames0 ext names) ctx) body (weakT {by = s} ty)
+    check0 (extendTyN (addNames0 ext names) ctx) body (weakT s ty)
 
   private covering
   check0Scope : TyContext d n -> Term d n ->
@@ -332,11 +346,11 @@ mutual
     pure $ lookupBound sg.fst i ctx.tctx
    where
     lookupBound : forall n. Qty -> Var n -> TContext d n -> InferResult' d n
-    lookupBound pi VZ (ctx :< ty) =
-      InfRes {type = weakT ty, qout = zeroFor ctx :< pi}
+    lookupBound pi VZ (ctx :< type) =
+      InfRes {type = weakT 1 type, qout = zeroFor ctx :< pi}
     lookupBound pi (VS i) (ctx :< _) =
       let InfRes {type, qout} = lookupBound pi i ctx in
-      InfRes {type = weakT type, qout = qout :< Zero}
+      InfRes {type = weakT 1 type, qout = qout :< Zero}
 
   infer' ctx sg (fun :@ arg) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
@@ -367,7 +381,7 @@ mutual
         bodyctx = extendTyN [< (pisg, x, tfst), (pisg, y, tsnd.term)] ctx
         bodyty  = substCasePairRet pairres.type ret
     bodyout <- checkC bodyctx sg body.term bodyty >>= popQs [< pisg, pisg]
-    -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
+    -- then Ψ | Γ ⊢ σ · caseπ ⋯ ⇒ ret[pair/p] ⊳ πΣ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret pair,
       qout = pi * pairres.qout + bodyout
@@ -390,7 +404,7 @@ mutual
     armres <- for arms $ \(a, s) =>
       checkC ctx sg s (sub1 ret (Tag a :# tres.type))
     let Just armout = lubs ctx armres
-          | _ => throw $ BadCaseQtys ctx $
+          | _ => throw $ BadQtys "case arms" ctx $
               zipWith (\qs, (t, rhs) => (qs, Tag t)) armres arms
     pure $ InfRes {
       type = sub1 ret t,
@@ -417,7 +431,7 @@ mutual
     expectCompatQ qih (pi' * sg.fst)
     -- [fixme] better error here
     expectCompatQ (qp + qih) pisg
-    -- then Ψ | Γ ⊢ case ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
+    -- then Ψ | Γ ⊢ caseπ ⋯ ⇒ A[n] ⊳ πΣn + Σz + ωΣs
     pure $ InfRes {
       type = sub1 ret n,
       qout = pi * nres.qout + zerout + Any * sucout
@@ -435,7 +449,7 @@ mutual
         bodyCtx  = extendTy qpisg body.name ty ctx
         bodyType = substCaseBoxRet ty ret
     bodyout <- checkC bodyCtx sg body.term bodyType >>= popQ qpisg
-    -- then Ψ | Γ ⊢ case ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂
+    -- then Ψ | Γ ⊢ caseπ ⋯ ⇒ R[b/x] ⊳ Σ₁ + Σ₂
     pure $ InfRes {
       type = sub1 ret box,
       qout = boxres.qout + bodyout
@@ -448,23 +462,43 @@ mutual
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
-  infer' ctx sg (TypeCase ty ret univ pi sig enum eq nat box) = do
+  infer' ctx sg (Coe (S [< i] ty) p q val) = do
+    let ty = ty.term
+    checkType (extendDim i ctx) ty Nothing
+    qout <- checkC ctx sg val (ty // one p)
+    pure $ InfRes {type = ty // one q, qout}
+
+  infer' ctx sg (Comp ty p q val r (S [< j0] val0) (S [< j1] val1)) = do
+    checkType ctx ty Nothing
+    qout <- checkC ctx sg val ty
+    let ty'  = dweakT 1 ty; val' = dweakT 1 val; p' = weakD 1 p
+        ctx0 = extendDim j0 $ eqDim r (K Zero) ctx
+        val0 = val0.term
+    qout0 <- check ctx0 sg val0 ty'
+    equal (eqDim (BV 0) p' ctx0) ty' val0 val'
+    let ctx1 = extendDim j0 $ eqDim r (K One) ctx
+        val1  = val1.term
+    qout1 <- check ctx1 sg val1 ty'
+    equal (eqDim (BV 0) p' ctx1) ty' val1 val'
+    let qout0' = toMaybe $ map (, val0 // one p) qout0
+        qout1' = toMaybe $ map (, val1 // one p) qout1
+        qouts  = (qout, val) :: catMaybes [qout0', qout1']
+    let Just qout = lubs ctx $ map fst qouts
+      | Nothing => throw $ BadQtys "composition" ctx qouts
+    pure $ InfRes {type = ty, qout}
+
+  infer' ctx sg (TypeCase ty ret arms def) = do
     -- if σ = 0
     expectEqualQ Zero sg.fst
     -- if Ψ, Γ ⊢₀ e ⇒ Type u
     u <- expectTYPE !ask ctx . type =<< inferC ctx szero ty
-    -- if Ψ, Γ ⊢₀ C ⇐ Type
-    --   (non-dependent return type)
+    -- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
     checkTypeC ctx ret Nothing
-    -- if all the cases have type C
-    check0 ctx univ ret
-    check0ScopeN ctx [< TYPE u, Arr Zero (BVT 0) (TYPE u)] pi  ret
-    check0ScopeN ctx [< TYPE u, Arr Zero (BVT 0) (TYPE u)] sig ret
-    check0 ctx enum ret
-    check0ScopeN ctx [< TYPE u, TYPE u, Eq0 (TYPE u) (BVT 1) (BVT 0),
-                        BVT 2, BVT 2] eq ret
-    check0 ctx nat ret
-    check0Scope ctx (TYPE u) box ret
+    -- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A
+    for_ allKinds $ \k =>
+      for_ (lookupPrecise k arms) $ \(S names t) =>
+        check0 (extendTyN (addNames0 (typecaseTel k u) names) ctx)
+               t.term (weakT (arity k) ret)
     -- then Ψ, Γ ⊢₀ type-case ⋯ ⇒ C
     pure $ InfRes {type = ret, qout = zeroFor ctx}
 
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index d1ff753..6e27e9b 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -8,9 +8,15 @@ import public Quox.Syntax
 import public Quox.Definition
 import public Quox.Reduce
 
+import Language.Reflection
 import Control.Eff
 
 %default total
+%language ElabReflection
+
+private TTName : Type
+TTName = TT.Name
+%hide TT.Name
 
 
 public export
@@ -50,146 +56,94 @@ substCaseSuccRet retty = retty.term // (Succ (BVT 1) :# Nat ::: shift 2)
 public export
 substCaseBoxRet : Term d n -> ScopeTerm d n -> Term d (S n)
 substCaseBoxRet dty retty =
-  retty.term // (Box (BVT 0) :# weakT dty ::: shift 1)
+  retty.term // (Box (BVT 0) :# weakT 1 dty ::: shift 1)
 
 
 parameters (defs : Definitions) {auto _ : Has ErrorEff fs}
-  export covering %inline
-  whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError =>
-          {d, n : Nat} -> tm d n -> Eff fs (NonRedex tm d n defs)
-  whnfT = either (throw . WhnfError) pure . whnf defs
+  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)
+    whnf = let Val n = ctx.termLen; Val d = ctx.dimLen in
+           rethrow . whnf defs (toWhnfContext ctx)
 
-  parameters {d2, n : Nat} (ctx : Lazy (TyContext d1 n))
-             (th : Lazy (DSubst d2 d1))
-    export covering %inline
-    expectTYPE_ : Term d2 n -> Eff fs Universe
-    expectTYPE_ s = case fst !(whnfT s) of
-      TYPE l => pure l
-      _      => throw $ ExpectedTYPE ctx (s // th)
+    private covering %macro
+    expect : (forall d, n. NameContexts d n -> Term d n -> Error) ->
+             TTImp -> TTImp -> Elab (Term d n -> Eff fs a)
+    expect k l r = do
+      f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
+      pure $ \t => maybe (throw $ k ctx.names t) pure . f . fst =<< whnf t
 
-    export covering %inline
-    expectPi_ : Term d2 n -> Eff fs (Qty, Term d2 n, ScopeTerm d2 n)
-    expectPi_ s = case fst !(whnfT s) of
-      Pi {qty, arg, res, _} => pure (qty, arg, res)
-      _                     => throw $ ExpectedPi ctx (s // th)
-
-    export covering %inline
-    expectSig_ : Term d2 n -> Eff fs (Term d2 n, ScopeTerm d2 n)
-    expectSig_ s = case fst !(whnfT s) of
-      Sig {fst, snd, _} => pure (fst, snd)
-      _                 => throw $ ExpectedSig ctx (s // th)
-
-    export covering %inline
-    expectEnum_ : Term d2 n -> Eff fs (SortedSet TagVal)
-    expectEnum_ s = case fst !(whnfT s) of
-      Enum tags => pure tags
-      _         => throw $ ExpectedEnum ctx (s // th)
-
-    export covering %inline
-    expectEq_ : Term d2 n ->
-                Eff fs (DScopeTerm d2 n, Term d2 n, Term d2 n)
-    expectEq_ s = case fst !(whnfT s) of
-      Eq {ty, l, r, _} => pure (ty, l, r)
-      _                => throw $ ExpectedEq ctx (s // th)
-
-    export covering %inline
-    expectNat_ : Term d2 n -> Eff fs ()
-    expectNat_ s = case fst !(whnfT s) of
-      Nat => pure ()
-      _   => throw $ ExpectedNat ctx (s // th)
-
-    export covering %inline
-    expectBOX_ : Term d2 n -> Eff fs (Qty, Term d2 n)
-    expectBOX_ s = case fst !(whnfT s) of
-      BOX q a => pure (q, a)
-      _       => throw $ ExpectedBOX ctx (s // th)
-
-
-  -- [fixme] refactor this stuff
-
-  parameters (ctx : TyContext d n)
     export covering %inline
     expectTYPE : Term d n -> Eff fs Universe
-    expectTYPE =
-      let Val d = ctx.dimLen; Val n = ctx.termLen in
-      expectTYPE_ ctx id
+    expectTYPE = expect ExpectedTYPE `(TYPE l) `(l)
 
     export covering %inline
     expectPi : Term d n -> Eff fs (Qty, Term d n, ScopeTerm d n)
-    expectPi =
-      let Val d = ctx.dimLen; Val n = ctx.termLen in
-      expectPi_ ctx id
+    expectPi = expect ExpectedPi `(Pi {qty, arg, res}) `((qty, arg, res))
 
     export covering %inline
     expectSig : Term d n -> Eff fs (Term d n, ScopeTerm d n)
-    expectSig =
-      let Val d = ctx.dimLen; Val n = ctx.termLen in
-      expectSig_ ctx id
+    expectSig = expect ExpectedSig `(Sig {fst, snd}) `((fst, snd))
 
     export covering %inline
     expectEnum : Term d n -> Eff fs (SortedSet TagVal)
-    expectEnum =
-      let Val d = ctx.dimLen; Val n = ctx.termLen in
-      expectEnum_ ctx id
+    expectEnum = expect ExpectedEnum `(Enum ts) `(ts)
 
     export covering %inline
     expectEq : Term d n -> Eff fs (DScopeTerm d n, Term d n, Term d n)
-    expectEq =
-      let Val d = ctx.dimLen; Val n = ctx.termLen in
-      expectEq_ ctx id
+    expectEq = expect ExpectedEq `(Eq {ty, l, r}) `((ty, l, r))
 
     export covering %inline
     expectNat : Term d n -> Eff fs ()
-    expectNat =
-      let Val d = ctx.dimLen; Val n = ctx.termLen in
-      expectNat_ ctx id
+    expectNat = expect ExpectedNat `(Nat) `(())
 
     export covering %inline
     expectBOX : Term d n -> Eff fs (Qty, Term d n)
-    expectBOX =
-      let Val d = ctx.dimLen; Val n = ctx.termLen in
-      expectBOX_ ctx id
+    expectBOX = expect ExpectedBOX `(BOX {qty, ty}) `((qty, ty))
 
 
-  parameters (ctx : EqContext n)
-    export covering %inline
-    expectTYPEE : Term 0 n -> Eff fs Universe
-    expectTYPEE t =
-      let Val n = ctx.termLen in
-      expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t
+  namespace EqContext
+   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)
+
+    private covering %macro
+    expect : (forall d, n. NameContexts d n -> Term d n -> Error) ->
+             TTImp -> TTImp -> Elab (Term 0 n -> Eff fs a)
+    expect k l r = do
+      f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
+      pure $ \t =>
+        let err = throw $ k ctx.names (t // shift0 ctx.dimLen) in
+        maybe err pure . f . fst =<< whnf t
 
     export covering %inline
-    expectPiE : Term 0 n -> Eff fs (Qty, Term 0 n, ScopeTerm 0 n)
-    expectPiE t =
-      let Val n = ctx.termLen in
-      expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectTYPE : Term 0 n -> Eff fs Universe
+    expectTYPE = expect ExpectedTYPE `(TYPE l) `(l)
 
     export covering %inline
-    expectSigE : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
-    expectSigE t =
-      let Val n = ctx.termLen in
-      expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectPi : Term 0 n -> Eff fs (Qty, Term 0 n, ScopeTerm 0 n)
+    expectPi = expect ExpectedPi `(Pi {qty, arg, res}) `((qty, arg, res))
 
     export covering %inline
-    expectEnumE : Term 0 n -> Eff fs (SortedSet TagVal)
-    expectEnumE t =
-      let Val n = ctx.termLen in
-      expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectSig : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
+    expectSig = expect ExpectedSig `(Sig {fst, snd}) `((fst, snd))
 
     export covering %inline
-    expectEqE : Term 0 n -> Eff fs (DScopeTerm 0 n, Term 0 n, Term 0 n)
-    expectEqE t =
-      let Val n = ctx.termLen in
-      expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
+    expectEnum = expect ExpectedEnum `(Enum ts) `(ts)
 
     export covering %inline
-    expectNatE : Term 0 n -> Eff fs ()
-    expectNatE t =
-      let Val n = ctx.termLen in
-      expectNat_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectEq : Term 0 n -> Eff fs (DScopeTerm 0 n, Term 0 n, Term 0 n)
+    expectEq = expect ExpectedEq `(Eq {ty, l, r}) `((ty, l, r))
 
     export covering %inline
-    expectBOXE : Term 0 n -> Eff fs (Qty, Term 0 n)
-    expectBOXE t =
-      let Val n = ctx.termLen in
-      expectBOX_ (toTyContext ctx) (shift0 ctx.dimLen) t
+    expectNat : Term 0 n -> Eff fs ()
+    expectNat = expect ExpectedNat `(Nat) `(())
+
+    export covering %inline
+    expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n)
+    expectBOX = expect ExpectedBOX `(BOX {qty, ty}) `((qty, ty))
diff --git a/lib/Quox/Typing/Context.idr b/lib/Quox/Typing/Context.idr
index 555e4ab..2ad6f34 100644
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@@ -51,6 +51,14 @@ record EqContext n where
 %name EqContext ctx
 
 
+public export
+record WhnfContext d n where
+  constructor MkWhnfContext
+  dnames : NContext d
+  tnames : NContext n
+  tctx   : TContext d n
+%name WhnfContext ctx
+
 namespace TContext
   export %inline
   pushD : TContext d n -> TContext (S d) n
@@ -111,6 +119,11 @@ namespace TyContext
   eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
   eqDim p q = {dctx $= set p q, dimLen $= id, termLen $= id}
 
+  export
+  toWhnfContext : TyContext d n -> WhnfContext d n
+  toWhnfContext (MkTyContext {dnames, tnames, tctx, _}) =
+    MkWhnfContext {dnames, tnames, tctx}
+
 
 namespace QOutput
   export %inline
@@ -190,6 +203,30 @@ namespace EqContext
       dnames, tnames, qtys
     }
 
+  export
+  toWhnfContext : (ectx : EqContext n) -> WhnfContext 0 n
+  toWhnfContext (MkEqContext {tnames, tctx, _}) =
+    MkWhnfContext {dnames = [<], tnames, tctx}
+
+namespace WhnfContext
+  public export %inline
+  empty : WhnfContext 0 0
+  empty = MkWhnfContext [<] [<] [<]
+
+  export
+  extendDimN : {s : Nat} -> NContext s -> WhnfContext d n ->
+               WhnfContext (s + d) n
+  extendDimN ns (MkWhnfContext {dnames, tnames, tctx}) =
+    MkWhnfContext {
+      dnames = dnames ++ toSnocVect' ns,
+      tctx   = dweakT s <$> tctx,
+      tnames
+    }
+
+  export
+  extendDim : BaseName -> WhnfContext d n -> WhnfContext (S d) n
+  extendDim i = extendDimN [< i]
+
 
 private
 data CtxBinder a = MkCtxBinder BaseName a
diff --git a/lib/Quox/Typing/Error.idr b/lib/Quox/Typing/Error.idr
index 14eea35..b8d962b 100644
--- a/lib/Quox/Typing/Error.idr
+++ b/lib/Quox/Typing/Error.idr
@@ -1,7 +1,6 @@
 module Quox.Typing.Error
 
 import Quox.Syntax
-import Quox.Reduce
 import Quox.Typing.Context
 import Quox.Typing.EqMode
 import Quox.Pretty
@@ -10,19 +9,62 @@ import Data.List
 import Control.Eff
 
 
+public export
+record NameContexts d n where
+  constructor MkNameContexts
+  dnames : NContext d
+  tnames : NContext n
+
+namespace NameContexts
+  export
+  empty : NameContexts 0 0
+  empty = MkNameContexts [<] [<]
+
+  export
+  extendDimN : NContext s -> NameContexts d n -> NameContexts (s + d) n
+  extendDimN xs = {dnames $= (++ toSnocVect' xs)}
+
+  export
+  extendDim : BaseName -> NameContexts d n -> NameContexts (S d) n
+  extendDim i = extendDimN [< i]
+
+namespace TyContext
+  public export
+  (.names) : TyContext d n -> NameContexts d n
+  (MkTyContext {dnames, tnames, _}).names =
+    MkNameContexts {dnames, tnames}
+
+namespace EqContext
+  public export
+  (.names) : (e : EqContext n) -> NameContexts e.dimLen n
+  (MkEqContext {dnames, tnames, _}).names =
+    MkNameContexts {dnames, tnames}
+
+  public export
+  (.names0) : EqContext n -> NameContexts 0 n
+  (MkEqContext {tnames, _}).names0 =
+    MkNameContexts {dnames = [<], tnames}
+
+namespace WhnfContext
+  public export
+  (.names) : WhnfContext d n -> NameContexts d n
+  (MkWhnfContext {dnames, tnames, _}).names =
+    MkNameContexts {dnames, tnames}
+
+
 public export
 data Error
-= ExpectedTYPE (TyContext d n) (Term d n)
-| ExpectedPi   (TyContext d n) (Term d n)
-| ExpectedSig  (TyContext d n) (Term d n)
-| ExpectedEnum (TyContext d n) (Term d n)
-| ExpectedEq   (TyContext d n) (Term d n)
-| ExpectedNat  (TyContext d n) (Term d n)
-| ExpectedBOX  (TyContext d n) (Term d n)
+= ExpectedTYPE (NameContexts d n) (Term d n)
+| ExpectedPi   (NameContexts d n) (Term d n)
+| ExpectedSig  (NameContexts d n) (Term d n)
+| ExpectedEnum (NameContexts d n) (Term d n)
+| ExpectedEq   (NameContexts d n) (Term d n)
+| ExpectedNat  (NameContexts d n) (Term d n)
+| ExpectedBOX  (NameContexts d n) (Term d n)
 | BadUniverse  Universe Universe
 | TagNotIn     TagVal (SortedSet TagVal)
 | BadCaseEnum  (SortedSet TagVal) (SortedSet TagVal)
-| BadCaseQtys  (TyContext d n) (List (QOutput n, Term d n))
+| BadQtys      String (TyContext d n) (List (QOutput n, Term d n))
 
 -- first term arg of ClashT is the type
 | ClashT  (EqContext n) EqMode (Term 0 n) (Term 0 n) (Term 0 n)
@@ -35,6 +77,8 @@ data Error
 | NotType (TyContext d n) (Term d n)
 | WrongType (EqContext n) (Term 0 n) (Term 0 n)
 
+| MissingEnumArm TagVal (List TagVal)
+
 -- extra context
 | WhileChecking
     (TyContext d n) Qty
@@ -59,8 +103,6 @@ data Error
     (EqContext n) EqMode
     (Elim 0 n) (Elim 0 n)
     Error
-
-| WhnfError WhnfError
 %name Error err
 
 public export
@@ -157,62 +199,71 @@ isTypeInUniverse (Just k) = "is a type in universe" <++> prettyUniverse k
 
 parameters (unicode : Bool)
   private
-  termt : TyContext d n -> Term d n -> Doc HL
-  termt ctx = hang 4 . prettyTerm unicode ctx.dnames ctx.tnames
+  termn : NameContexts d n -> Term d n -> Doc HL
+  termn ctx = hang 4 . prettyTerm unicode ctx.dnames ctx.tnames
 
   private
-  terme : EqContext n -> Term 0 n -> Doc HL
-  terme ctx = hang 4 . prettyTerm unicode [<] ctx.tnames
+  dstermn : {s : Nat} -> NameContexts d n -> DScopeTermN s d n -> Doc HL
+  dstermn ctx (S i t) = termn (extendDimN i ctx) t.term
 
   private
-  dissectCaseQtys : TyContext d n ->
-                    NContext n' -> List (QOutput n', z) ->
-                    List (Doc HL)
-  dissectCaseQtys ctx [<]        arms = []
-  dissectCaseQtys ctx (tel :< x) arms =
-    let qs = map (head . fst) arms
-        tl = dissectCaseQtys ctx tel (map (mapFst tail) arms)
+  filterSameQtys : NContext n -> List (QOutput n, z) ->
+                   Exists $ \n' => (NContext n', List (QOutput n', z))
+  filterSameQtys [<]       qts = Evidence 0 ([<], qts)
+  filterSameQtys (ns :< n) qts =
+    let (qs, qts) = unzip $ map (\(qs :< q, t) => (q, qs, t)) qts
+        Evidence l (ns, qts) = filterSameQtys ns qts
     in
-    if allSame qs then tl else
-    ("-" <++> asep [hsep [pretty0 unicode $ TV x, "is used with quantities"],
-                    hseparate comma $ map (pretty0 unicode) qs]) :: tl
+    if allSame qs
+    then Evidence l (ns, qts)
+    else Evidence (S l) (ns :< n, zipWith (\(qs, t), q => (qs :< q, t)) qts qs)
   where
     allSame : List Qty -> Bool
     allSame []        = True
     allSame (q :: qs) = all (== q) qs
 
-  export
-  prettyWhnfError : WhnfError -> Doc HL
-  prettyWhnfError = \case
-    MissingEnumArm tag tags =>
-      sep [hsep ["the tag", hl Tag $ pretty tag, "is not contained in"],
-           termt empty $ Enum $ fromList tags]
+  private
+  printCaseQtys : TyContext d n ->
+                  NContext n' -> List (QOutput n', Term d n) ->
+                  List (Doc HL)
+  printCaseQtys ctx ns qts =
+    let Evidence l (ns, qts) = filterSameQtys ns qts in
+    map (line ns) qts
+  where
+    commaList : PrettyHL a => Context' a l -> Doc HL
+    commaList = hseparate comma . map (pretty0 unicode) . toList'
+
+    line : NContext l -> (QOutput l, Term d n) -> Doc HL
+    line ns (qs, t) =
+      "-" <++> asep ["the term", termn ctx.names t,
+                     "uses variables", commaList $ TV <$> ns,
+                     "with quantities", commaList qs]
 
   -- [todo] only show some contexts, probably
   export
   prettyError : (showContext : Bool) -> Error -> Doc HL
   prettyError showContext = \case
     ExpectedTYPE ctx s =>
-      sep ["expected a type universe, but got", termt ctx s]
+      sep ["expected a type universe, but got", termn ctx s]
 
     ExpectedPi ctx s =>
-      sep ["expected a function type, but got", termt ctx s]
+      sep ["expected a function type, but got", termn ctx s]
 
     ExpectedSig ctx s =>
-      sep ["expected a pair type, but got", termt ctx s]
+      sep ["expected a pair type, but got", termn ctx s]
 
     ExpectedEnum ctx s =>
-      sep ["expected an enumeration type, but got", termt ctx s]
+      sep ["expected an enumeration type, but got", termn ctx s]
 
     ExpectedEq ctx s =>
-      sep ["expected an equality type, but got", termt ctx s]
+      sep ["expected an equality type, but got", termn ctx s]
 
     ExpectedNat ctx s {d, n} =>
       sep ["expected the type", pretty0 unicode $ Nat {d, n},
-           "but got", termt ctx s]
+           "but got", termn ctx s]
 
     ExpectedBOX ctx s =>
-      sep ["expected a box type, but got", termt ctx s]
+      sep ["expected a box type, but got", termn ctx s]
 
     BadUniverse k l =>
       sep ["the universe level", prettyUniverse k,
@@ -220,32 +271,32 @@ parameters (unicode : Bool)
 
     TagNotIn tag set =>
       sep [sep ["tag", prettyTag tag, "is not contained in"],
-           termt empty (Enum set)]
+           termn empty (Enum set)]
 
     BadCaseEnum type arms =>
-      sep ["case expression has head of type", termt empty (Enum type),
-           "but cases for", termt empty (Enum arms)]
+      sep ["case expression has head of type", termn empty (Enum type),
+           "but cases for", termn empty (Enum arms)]
 
-    BadCaseQtys ctx arms =>
+    BadQtys what ctx arms =>
       hang 4 $ sep $
-        "inconsistent variable usage in case arms" ::
-        dissectCaseQtys ctx ctx.tnames arms
+        ("inconsistent variable usage in" <++> fromString what) ::
+        printCaseQtys ctx ctx.tnames arms
 
     ClashT ctx mode ty s t =>
       inEContext ctx $
-      sep ["the term", terme ctx s,
-           hsep ["is not", prettyMode mode], terme ctx t,
-           "at type", terme ctx ty]
+      sep ["the term", termn ctx.names0 s,
+           hsep ["is not", prettyMode mode], termn ctx.names0 t,
+           "at type", termn ctx.names0 ty]
 
     ClashTy ctx mode a b =>
       inEContext ctx $
-      sep ["the type", terme ctx a,
-           hsep ["is not", prettyMode mode], terme ctx b]
+      sep ["the type", termn ctx.names0 a,
+           hsep ["is not", prettyMode mode], termn ctx.names0 b]
 
     ClashE ctx mode e f =>
       inEContext ctx $
-      sep ["the term", terme ctx $ E e,
-           hsep ["is not", prettyMode mode], terme ctx $ E f]
+      sep ["the term", termn ctx.names0 $ E e,
+           hsep ["is not", prettyMode mode], termn ctx.names0 $ E f]
 
     ClashU mode k l =>
       sep ["the universe level", prettyUniverse k,
@@ -260,46 +311,48 @@ parameters (unicode : Bool)
 
     NotType ctx s =>
       inTContext ctx $
-      sep ["the term", termt ctx s, "is not a type"]
+      sep ["the term", termn ctx.names s, "is not a type"]
 
     WrongType ctx ty s =>
       inEContext ctx $
-      sep ["the term", terme ctx s,
-           "cannot have type", terme ctx ty]
+      sep ["the term", termn ctx.names0 s,
+           "cannot have type", termn ctx.names0 ty]
+
+    MissingEnumArm tag tags =>
+      sep [hsep ["the tag", hl Tag $ pretty tag, "is not contained in"],
+           termn empty $ Enum $ fromList tags]
 
     WhileChecking ctx pi s a err =>
       vsep [inTContext ctx $
-              sep ["while checking", termt ctx s,
-                   "has type", termt ctx a,
+              sep ["while checking", termn ctx.names s,
+                   "has type", termn ctx.names a,
                    hsep ["with quantity", pretty0 unicode pi]],
             prettyError showContext err]
 
     WhileCheckingTy ctx a k err =>
       vsep [inTContext ctx $
-              sep ["while checking", termt ctx a,
+              sep ["while checking", termn ctx.names a,
                    isTypeInUniverse k],
             prettyError showContext err]
 
     WhileInferring ctx pi e err =>
       vsep [inTContext ctx $
-              sep ["while inferring the type of", termt ctx $ E e,
+              sep ["while inferring the type of", termn ctx.names $ E e,
                    hsep ["with quantity", pretty0 unicode pi]],
             prettyError showContext err]
 
     WhileComparingT ctx mode a s t err =>
       vsep [inEContext ctx $
-              sep ["while checking that", terme ctx s,
-                   hsep ["is", prettyMode mode], terme ctx t,
-                   "at type", terme ctx a],
+              sep ["while checking that", termn ctx.names0 s,
+                   hsep ["is", prettyMode mode], termn ctx.names0 t,
+                   "at type", termn ctx.names0 a],
             prettyError showContext err]
 
     WhileComparingE ctx mode e f err =>
       vsep [inEContext ctx $
-              sep ["while checking that", terme ctx $ E e,
-                   hsep ["is", prettyMode mode], terme ctx $ E f],
+              sep ["while checking that", termn ctx.names0 $ E e,
+                   hsep ["is", prettyMode mode], termn ctx.names0 $ E f],
             prettyError showContext err]
-
-    WhnfError err => prettyWhnfError err
   where
     inTContext : TyContext d n -> Doc HL -> Doc HL
     inTContext ctx doc =
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 0d73bbe..82c52db 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -5,7 +5,7 @@ authors   = "rhiannon morris"
 sourceloc = "https://git.rhiannon.website/rhi/quox"
 license   = "acsl"
 
-depends = base, contrib, elab-util, snocvect, eff
+depends = base, contrib, elab-util, sop, snocvect, eff
 
 modules =
   Quox.BoolExtra,
@@ -21,6 +21,7 @@ modules =
   Quox.Syntax.Shift,
   Quox.Syntax.Subst,
   Quox.Syntax.Term,
+  Quox.Syntax.Term.TyConKind,
   Quox.Syntax.Term.Base,
   Quox.Syntax.Term.Pretty,
   Quox.Syntax.Term.Split,
diff --git a/tests/TermImpls.idr b/tests/TermImpls.idr
index a12ac7a..07037ab 100644
--- a/tests/TermImpls.idr
+++ b/tests/TermImpls.idr
@@ -25,14 +25,14 @@ mutual
     TYPE _ == _ = False
 
     Pi qty1 arg1 res1 == Pi qty2 arg2 res2 =
-      qty1 == qty2 && arg1 == arg2 && res1.term == res2.term
+      qty1 == qty2 && arg1 == arg2 && res1 == res2
     Pi {} == _ = False
 
-    Lam body1 == Lam body2 = body1.term == body2.term
+    Lam body1 == Lam body2 = body1 == body2
     Lam {} == _ = False
 
     Sig fst1 snd1 == Sig fst2 snd2 =
-      fst1 == fst2 && snd1.term == snd2.term
+      fst1 == fst2 && snd1 == snd2
     Sig {} == _ = False
 
     Pair fst1 snd1 == Pair fst2 snd2 = fst1 == fst2 && snd1 == snd2
@@ -45,10 +45,10 @@ mutual
     Tag _ == _ = False
 
     Eq ty1 l1 r1 == Eq ty2 l2 r2 =
-      ty1.term == ty2.term && l1 == l2 && r1 == r2
+      ty1 == ty2 && l1 == l2 && r1 == r2
     Eq {} == _ = False
 
-    DLam body1 == DLam body2 = body1.term == body2.term
+    DLam body1 == DLam body2 = body1 == body2
     DLam {} == _ = False
 
     Nat == Nat = True
@@ -93,20 +93,20 @@ mutual
     (_ :@ _) == _ = False
 
     CasePair q1 p1 r1 b1 == CasePair q2 p2 r2 b2 =
-      q1 == q2 && p1 == p2 && r1.term == r2.term && b1.term == b2.term
+      q1 == q2 && p1 == p2 && r1 == r2 && b1 == b2
     CasePair {} == _ = False
 
     CaseEnum q1 t1 r1 a1 == CaseEnum q2 t2 r2 a2 =
-      q1 == q2 && t1 == t2 && r1.term == r2.term && a1 == a2
+      q1 == q2 && t1 == t2 && r1 == r2 && a1 == a2
     CaseEnum {} == _ = False
 
     CaseNat q1 q1' n1 r1 z1 s1 == CaseNat q2 q2' n2 r2 z2 s2 =
       q1 == q2 && q1' == q2' && n1 == n2 &&
-      r1.term == r2.term && z1 == z2 && s1.term == s2.term
+      r1 == r2 && z1 == z2 && s1 == s2
     CaseNat {} == _ = False
 
     CaseBox q1 x1 r1 b1 == CaseBox q2 x2 r2 b2 =
-      q1 == q2 && x1 == x2 && r1.term == r2.term && b1.term == b2.term
+      q1 == q2 && x1 == x2 && r1 == r2 && b1 == b2
     CaseBox {} == _ = False
 
     (fun1 :% dim1) == (fun2 :% dim2) = fun1 == fun2 && dim1 == dim2
@@ -115,17 +115,18 @@ mutual
     (tm1 :# ty1) == (tm2 :# ty2) = tm1 == tm2 && ty1 == ty2
     (_ :# _) == _ = False
 
-    TypeCase ty1 ret1 univ1 pi1 sig1 enum1 eq1 nat1 box1
-      ==
-    TypeCase ty2 ret2 univ2 pi2 sig2 enum2 eq2 nat2 box2 =
-      ty1 == ty2 && ret1 == ret2 &&
-      pi1.term == pi2.term &&
-      sig1.term == sig2.term &&
-      enum1 == enum2 &&
-      eq1.term == eq2.term &&
-      nat1 == nat2 &&
-      box1.term == box2.term
+    Coe ty1 p1 q1 val1 == Coe ty2 p2 q2 val2 =
+      ty1 == ty2 && p1 == p2 && q1 == q2 && val1 == val2
+    Coe {} == _ = False
 
+    Comp ty1 p1 q1 val1 r1 zero1 one1 == Comp ty2 p2 q2 val2 r2 zero2 one2 =
+      ty1 == ty2 && p1 == p2 && q1 == q2 &&
+      val1 == val2 && r1 == r2 && zero1 == zero2 && one1 == one2
+    Comp {} == _ = False
+
+    TypeCase ty1 ret1 arms1 def1 == TypeCase ty2 ret2 arms2 def2 =
+      ty1 == ty2 && ret1 == ret2 &&
+      arms1 == arms2 && def1 == def2
     TypeCase {} == _ = False
 
     CloE el1 th1 == CloE el2 th2 =
@@ -140,6 +141,14 @@ mutual
            Nothing   => False
     DCloE {} == _ = False
 
+  export covering
+  {s : Nat} -> Eq (ScopeTermN s d n) where
+    b1 == b2 = b1.term == b2.term
+
+  export covering
+  {s : Nat} -> Eq (DScopeTermN s d n) where
+    b1 == b2 = b1.term == b2.term
+
 export covering
 Show (Term d n) where
   showPrec d t = showParens (d /= Open) $ prettyStr True t
diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index d2e7408..dc01e78 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -155,30 +155,9 @@ tests = "pretty printing terms" :- [
   "type-case" :- [
     testPrettyE [<] [<]
       {label = "type-case ℕ ∷ ★₀ return ★₀ of { ⋯ }"}
-      (TypeCase (Nat :# TYPE 0) (TYPE 0) Nat (SN Nat) (SN Nat) Nat
-        (SN Nat) Nat (SN Nat))
-      """
-        type-case ℕ ∷ ★₀ return ★₀ of {
-          ★            ⇒ ℕ;
-          (_ → _)      ⇒ ℕ;
-          (_ × _)      ⇒ ℕ;
-          {}           ⇒ ℕ;
-          Eq _ _ _ _ _ ⇒ ℕ;
-          ℕ            ⇒ ℕ;
-          [_]          ⇒ ℕ
-        }
-      """
-      """
-        type-case Nat :: Type0 return Type0 of {
-          Type         => Nat;
-          (_ -> _)     => Nat;
-          (_ ** _)     => Nat;
-          {}           => Nat;
-          Eq _ _ _ _ _ => Nat;
-          Nat          => Nat;
-          [_]          => Nat
-        }
-      """
+      (TypeCase (Nat :# TYPE 0) (TYPE 0) empty Nat)
+      "type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ }"
+      "type-case Nat :: Type0 return Type0 of { _ => Nat }"
   ],
 
   "annotations" :- [
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index e1e5bf7..09a15fd 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -7,108 +7,113 @@ import TypingImpls
 import TAP
 
 
-parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex err}
-           {auto _ : ToInfo err}
-           {auto _ : forall d, n. Eq   (tm d n)}
-           {auto _ : forall d, n. Show (tm d n)}
+parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex} {d, n : Nat}
+           {auto _ : (Eq (tm d n), Show (tm d n))}
            {default empty defs : Definitions}
-           {default 0 d, n : Nat}
-  testWhnf : String -> tm d n -> tm d n -> Test
-  testWhnf label from to = test "\{label}  (whnf)" $ do
-    result <- bimap toInfo fst $ whnf defs from
+  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
     unless (result == to) $ Left [("exp", show to), ("got", show result)]
 
-  testNoStep : String -> tm d n -> Test
-  testNoStep label e = testWhnf label e e
+  private
+  testNoStep : String -> WhnfContext d n -> tm d n -> Test
+  testNoStep label ctx e = testWhnf label ctx e e
+
+private
+ctx : Context (\n => (BaseName, Term 0 n)) n -> WhnfContext 0 n
+ctx xs = let (ns, ts) = unzip xs in MkWhnfContext [<] ns ts
 
 
+export
+tests : Test
 tests = "whnf" :- [
   "head constructors" :- [
-    testNoStep "★₀" $ TYPE 0,
-    testNoStep "[A] ⊸ [B]" $
+    testNoStep "★₀" empty $ TYPE 0,
+    testNoStep "[A] ⊸ [B]" empty $
       Arr One (FT "A") (FT "B"),
-    testNoStep "(x: [A]) ⊸ [B [x]]" $
+    testNoStep "(x: [A]) ⊸ [B [x]]" empty $
       Pi One (FT "A") (S [< "x"] $ Y $ E $ F "B" :@ BVT 0),
-    testNoStep "λx. [x]" $
+    testNoStep "λx. [x]" empty $
       Lam $ S [< "x"] $ Y $ BVT 0,
-    testNoStep "[f [a]]" $
+    testNoStep "[f [a]]" empty $
       E $ F "f" :@ FT "a"
   ],
 
   "neutrals" :- [
-    testNoStep "x" {n = 1} $ BV 0,
-    testNoStep "a"         $ F "a",
-    testNoStep "f [a]"     $ F "f" :@ FT "a",
-    testNoStep "★₀ ∷ ★₁"   $ TYPE 0 :# TYPE 1
+    testNoStep "x" (ctx [< ("A", Nat)]) $ BV 0,
+    testNoStep "a"       empty $ F "a",
+    testNoStep "f [a]"   empty $ F "f" :@ FT "a",
+    testNoStep "★₀ ∷ ★₁" empty $ TYPE 0 :# TYPE 1
   ],
 
   "redexes" :- [
-    testWhnf "[a] ∷ [A]"
+    testWhnf "[a] ∷ [A]" empty
       (FT "a" :# FT "A")
       (F "a"),
-    testWhnf "[★₁ ∷ ★₃]"
+    testWhnf "[★₁ ∷ ★₃]" empty
       (E (TYPE 1 :# TYPE 3))
       (TYPE 1),
-    testWhnf "(λx. [x] ∷ [A] ⊸ [A]) [a]"
+    testWhnf "(λx. [x] ∷ [A] ⊸ [A]) [a]" empty
       ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
       (F "a")
   ],
 
   "definitions" :- [
-    testWhnf "a  (transparent)"
+    testWhnf "a  (transparent)" empty
       {defs = fromList [("a", mkDef gzero (TYPE 1) (TYPE 0))]}
       (F "a") (TYPE 0 :# TYPE 1)
   ],
 
   "elim closure" :- [
-    testWhnf "x{}" {n = 1}
+    testWhnf "x{}" (ctx [< ("A", Nat)])
       (CloE (BV 0) id)
       (BV 0),
-    testWhnf "x{a/x}"
+    testWhnf "x{a/x}" empty
       (CloE (BV 0) (F "a" ::: id))
       (F "a"),
-    testWhnf "x{x/x,a/y}" {n = 1}
+    testWhnf "x{x/x,a/y}" (ctx [< ("A", Nat)])
       (CloE (BV 0) (BV 0 ::: F "a" ::: id))
       (BV 0),
-    testWhnf "x{(y{a/y})/x}"
+    testWhnf "x{(y{a/y})/x}" empty
       (CloE (BV 0) ((CloE (BV 0) (F "a" ::: id)) ::: id))
       (F "a"),
-    testWhnf "(x y){f/x,a/y}"
+    testWhnf "(x y){f/x,a/y}" empty
       (CloE (BV 0 :@ BVT 1) (F "f" ::: F "a" ::: id))
       (F "f" :@ FT "a"),
-    testWhnf "([y] ∷ [x]){A/x}" {n = 1}
+    testWhnf "([y] ∷ [x]){A/x}" (ctx [< ("A", Nat)])
       (CloE (BVT 1 :# BVT 0) (F "A" ::: id))
       (BV 0),
-    testWhnf "([y] ∷ [x]){A/x,a/y}"
+    testWhnf "([y] ∷ [x]){A/x,a/y}" empty
       (CloE (BVT 1 :# BVT 0) (F "A" ::: F "a" ::: id))
       (F "a")
   ],
 
   "term closure" :- [
-    testWhnf "(λy. x){a/x}"
+    testWhnf "(λy. x){a/x}" empty
       (CloT (Lam $ S [< "y"] $ N $ BVT 0) (F "a" ::: id))
       (Lam $ S [< "y"] $ N $ FT "a"),
-    testWhnf "(λy. y){a/x}"
+    testWhnf "(λy. y){a/x}" empty
       (CloT ([< "y"] :\\ BVT 0) (F "a" ::: id))
       ([< "y"] :\\ BVT 0)
   ],
 
   "looking inside […]" :- [
-    testWhnf "[(λx. x ∷ A ⊸ A) [a]]"
+    testWhnf "[(λx. x ∷ A ⊸ A) [a]]" empty
       (E $ (([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
       (FT "a")
   ],
 
   "nested redex" :- [
     note "whnf only looks at top level redexes",
-    testNoStep "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
+    testNoStep "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" empty $
       [< "y"] :\\ E ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0),
-    testNoStep "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
+    testNoStep "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" empty $
       F "a" :@
       E ((([< "x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
-    testNoStep "λx. [y [x]]{x/x,a/y}" {n = 1} $
+    testNoStep "λx. [y [x]]{x/x,a/y}" (ctx [< ("A", Nat)]) $
       [< "x"] :\\ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
-    testNoStep "f ([y [x]]{x/x,a/y})" {n = 1} $
+    testNoStep "f ([y [x]]{x/x,a/y})" (ctx [< ("A", Nat)]) $
       F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id)
   ]
 ]
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index 3ee5ef3..b7c0425 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -451,8 +451,7 @@ tests = "typechecker" :- [
   "type-case" :- [
     testTC "0 · type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ } ⇒ ★₀" $
       inferAs empty szero
-        (TypeCase (Nat :# TYPE 0) (TYPE 0) Nat (SN Nat) (SN Nat) Nat
-          (SN Nat) Nat (SN Nat))
+        (TypeCase (Nat :# TYPE 0) (TYPE 0) empty Nat)
         (TYPE 0)
   ],
 
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index 04d68f7..7d41449 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -9,17 +9,10 @@ import Derive.Prelude
 %language ElabReflection
 
 
-%runElab derive "Reduce.WhnfError" [Show]
 %runElab deriveIndexed "TyContext" [Show]
 %runElab deriveIndexed "EqContext" [Show]
+%runElab deriveIndexed "NameContexts" [Show]
 %runElab derive "Error" [Show]
 
-export
-ToInfo WhnfError where
-  toInfo (MissingEnumArm t ts) =
-    [("type", "MissingEnumArm"),
-     ("tag", show t),
-     ("list", show ts)]
-
 export
 ToInfo Error where toInfo err = [("err", show $ prettyError True True err)]