diff --git a/lib/Quox/No.idr b/lib/Quox/No.idr
index 948eaf6..59cbca1 100644
--- a/lib/Quox/No.idr
+++ b/lib/Quox/No.idr
@@ -52,3 +52,8 @@ export %inline
 nchoose : (b : Bool) -> Either (So b) (No b)
 nchoose True  = Left  Oh
 nchoose False = Right Ah
+
+export
+0 notYesNo : {f : Dec p} -> Not p -> No (isYes f)
+notYesNo {f = Yes y} g = absurd $ g y
+notYesNo {f = No  n} g = Ah
diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index b70c8f1..f3faadd 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -107,92 +107,84 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
-
   ||| pushes a coercion inside a whnf-ed term
   export covering
   pushCoe : BindName ->
-            (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)) => Loc ->
+            (ty : Term (S d) n) ->
+            (p, q : Dim d) -> (0 npq : Not (p `Eqv` q)) =>
+            (s : Term d n) -> (0 pc : So (canPushCoe ty s)) => Loc ->
             Eff Whnf (NonRedex Elim d n defs)
-  pushCoe i ty p q s loc {snf} =
-    if p == q then whnf defs ctx $ Ann s (ty // one q) loc else
-    case s of
-      -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
-      TYPE {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
-      Pi   {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
-      Sig  {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
-      Enum {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
-      Eq   {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
-      Nat  {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
-      BOX  {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
+  pushCoe i ty p q s loc =
+    case ty of
+      -- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
+      TYPE l tyLoc =>
+        whnf defs ctx $ Ann s (TYPE l tyLoc) loc
 
-      -- just η expand it. then whnf for App will handle it later
-      -- this is how @xtt does it
+      -- η expand it so that whnf for App can deal with it
       --
-      -- (coe [i ⇒ A] @p @q (λ x ⇒ s)) ⇝
-      -- (λ y ⇒ (coe [i ⇒ A] @p @q (λ x ⇒ s)) y) ∷ A‹q/i› ⇝ ⋯
-      lam@(Lam {body, _}) => do
-        let lam'  = CoeT i ty p q lam loc
-            term' = LamY !(fresh body.name)
-                      (E $ App (weakE 1 lam') (BVT 0 noLoc) loc) loc
-            type' = ty // one q
-        whnf defs ctx $ Ann term' type' loc
+      -- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
+      --   ⇝
+      -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
+      Pi {} =>
+        let inner = Coe (SY [< i] ty) p q s loc in
+        whnf defs ctx $
+          Ann (LamY !(mnb "y" loc)
+                  (E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
+              (ty // one q) loc
 
-      -- (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›
+      -- no η!!!
+      -- push into a pair constructor, otherwise still stuck
       --
-      -- can't use η here because... it doesn't exist
-      Pair {fst, snd, loc = pairLoc} => do
-        let Sig {fst = tfst, snd = tsnd, loc = sigLoc} = ty
-          | _ => throw $ ExpectedSig ty.loc (extendDim i ctx.names) ty
-        let fst'  = E $ CoeT i tfst p q fst fst.loc
-            tfst' = tfst // (B VZ noLoc ::: shift 2)
-            tsnd' = sub1 tsnd $
-                    CoeT !(fresh i) tfst' (weakD 1 p) (B VZ noLoc)
-                      (dweakT 1 fst) fst.loc
-            snd'  = E $ CoeT i tsnd' p q snd snd.loc
-        pure $
-          Element (Ann (Pair fst' snd' pairLoc)
-                       (Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah
+      --   s̃‹𝑘› ≔ coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑘 s
+      -- -----------------------------------------------
+      --   (coe (𝑖 ⇒ (x : A) × B) @p @q (s, t))
+      --     ⇝
+      --   (s̃‹q›, coe (𝑖 ⇒ B[s̃‹𝑖›/x]) @p @q t)
+      --     ∷ ((x : A) × B)‹q/𝑖›
+      Sig tfst tsnd tyLoc => do
+        let Pair fst snd sLoc = s
+            fst' = CoeT i tfst p q fst fst.loc
+            fstInSnd =
+              CoeT !(fresh i)
+                   (tfst // (BV 0 loc ::: shift 2))
+                   (weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
+            snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
+        whnf defs ctx $
+          Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
 
-      -- η expand, like for Lam
+      -- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
+      Enum cases tyLoc =>
+        whnf defs ctx $ Ann s (Enum cases tyLoc) loc
+
+      -- η expand, same as for Π
       --
-      -- (coe [i ⇒ A] @p @q (δ j ⇒ s)) ⇝
-      -- (δ k ⇒ (coe [i ⇒ A] @p @q (δ j ⇒ s)) @k) ∷ A‹q/i› ⇝ ⋯
-      dlam@(DLam {body, _}) => do
-        let dlam' = CoeT i ty p q dlam loc
-            term' = DLamY !(mnb "j")
-                      (E $ DApp (dweakE 1 dlam') (B VZ noLoc) loc) loc
-            type' = ty // one q
-        whnf defs ctx $ Ann term' type' loc
+      -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s)
+      --   ⇝
+      -- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
+      Eq {} =>
+        let inner = Coe (SY [< i] ty) p q s loc in
+        whnf defs ctx $
+          Ann (DLamY !(mnb "k" loc)
+                  (E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
+              (ty // one q) loc
 
-      -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
-      Tag {tag, loc = tagLoc} => do
-        let Enum {cases, loc = enumLoc} = ty
-          | _ => throw $ ExpectedEnum ty.loc (extendDim i ctx.names) ty
-        pure $ Element (Ann (Tag tag tagLoc) (Enum cases enumLoc) loc) Ah
+      -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
+      Nat tyLoc =>
+        whnf defs ctx $ Ann s (Nat tyLoc) loc
 
-      -- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ)
-      Zero {loc = zeroLoc} => do
-        pure $ Element (Ann (Zero zeroLoc) (Nat ty.loc) loc) Ah
-      Succ {p = pred, loc = succLoc} => do
-        pure $ Element (Ann (Succ pred succLoc) (Nat ty.loc) loc) Ah
-
-      -- (coe [i ⇒ [π.A]] @p @q [s]) ⇝
-      -- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›]
-      Box {val, loc = boxLoc} => do
-        let BOX {qty, ty = a, loc = tyLoc} = ty
-          | _ => throw $ ExpectedBOX ty.loc (extendDim i ctx.names) ty
-        pure $ Element
-          (Ann (Box (E $ CoeT i a p q val val.loc) boxLoc)
-               (BOX qty (a // one q) tyLoc) loc)
-          Ah
-
-      E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah)
-  where
-    unwrapTYPE : Term (S d) n -> Eff Whnf Universe
-    unwrapTYPE (TYPE {l, _}) = pure l
-    unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty
+      -- η expand
+      --
+      -- (coe (𝑖 ⇒ [π. A]) @p @q s)
+      --   ⇝
+      -- [case1 coe (𝑖 ⇒ [π. A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
+      --   ∷ [π. A]‹q/𝑖›
+      BOX qty inner tyLoc =>
+        let inner = CaseBox {
+              qty  = One,
+              box  = Coe (SY [< i] ty) p q s loc,
+              ret  = SN $ ty // one q,
+              body = SY [< !(mnb "x" loc)] $ BVT 0 loc,
+              loc
+            }
+        in
+        whnf defs ctx $ Ann (Box (E inner) loc) (ty // one q) loc
diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index 6c50074..4406d7d 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -147,25 +147,50 @@ isK (K {}) = True
 isK _      = False
 
 
+||| if `ty` is a type constructor, and `val` is a value of that type where a
+||| coercion can be reduced. which is the case if any of:
+||| - `ty` is an atomic type
+||| - `ty` has η
+||| - `val` is a constructor form
+public export %inline
+canPushCoe : (ty, val : Term {}) -> Bool
+canPushCoe (TYPE  {}) _         = True
+canPushCoe (Pi    {}) _         = True
+canPushCoe (Lam   {}) _         = False
+canPushCoe (Sig   {}) (Pair {}) = True
+canPushCoe (Sig   {}) _         = False
+canPushCoe (Pair  {}) _         = False
+canPushCoe (Enum  {}) _         = True
+canPushCoe (Tag   {}) _         = False
+canPushCoe (Eq    {}) _         = True
+canPushCoe (DLam  {}) _         = False
+canPushCoe (Nat   {}) _         = True
+canPushCoe (Zero  {}) _         = False
+canPushCoe (Succ  {}) _         = False
+canPushCoe (BOX   {}) _         = True
+canPushCoe (Box   {}) _         = False
+canPushCoe (E     {}) _         = False
+canPushCoe (CloT  {}) _         = False
+canPushCoe (DCloT {}) _         = False
+
+
 mutual
   ||| a reducible elimination
   |||
-  ||| - a free variable, if its definition is known
-  ||| - an application whose head is an annotated lambda,
-  |||   a case expression whose head is an annotated constructor form, etc
-  ||| - a redundant annotation, or one whose term or type is reducible
-  ||| - coercions `coe (𝑖 ⇒ A) @p @q s` where:
-  |||     - `A` is in whnf, or
-  |||     - `𝑖` is not mentioned in `A`, or
-  |||     - `p = q`
-  |||     - [fixme] this is not true right now but that's because i wrote it
-  |||       wrong
-  ||| - compositions `comp A @p @q s @r {⋯}` where:
-  |||     - `A` is in whnf, or
-  |||     - `p = q`, or
-  |||     - `r = 0` or `r = 1`
-  |||     - [fixme] the p=q condition is also missing here
-  ||| - closures
+  ||| 1. a free variable, if its definition is known
+  ||| 2. an elimination whose head is reducible
+  ||| 3. an "active" elimination:
+  |||    an application whose head is an annotated lambda,
+  |||    a case expression whose head is an annotated constructor form, etc
+  ||| 4. a redundant annotation, or one whose term or type is reducible
+  ||| 5. a coercion `coe (𝑖 ⇒ A) @p @q s` where:
+  |||      a. `A` is reducible or a type constructor, or
+  |||      b. `𝑖` is not mentioned in `A`
+  |||         ([fixme] should be A‹0/𝑖› = A‹1/𝑖›), or
+  |||      c. `p = q`
+  ||| 6. a composition `comp A @p @q s @r {⋯}`
+  |||    where `p = q`, `r = 0`, or `r = 1`
+  ||| 7. a closure
   public export
   isRedexE : RedexTest Elim
   isRedexE defs (F {x, _}) {d, n} =
@@ -185,10 +210,11 @@ mutual
     isRedexE defs fun || isDLamHead fun || isK arg
   isRedexE defs (Ann {tm, ty, _}) =
     isE tm || isRedexT defs tm || isRedexT defs ty
-  isRedexE defs (Coe {val, _}) =
-    isRedexT defs val || not (isE val)
-  isRedexE defs (Comp {ty, r, _}) =
-    isRedexT defs ty || isK r
+  isRedexE defs (Coe {ty = S _ (N _), _}) = True
+  isRedexE defs (Coe {ty = S _ (Y ty), p, q, val, _}) =
+    isRedexT defs ty || canPushCoe ty val || isYes (p `decEqv` q)
+  isRedexE defs (Comp {ty, r, p, q, _}) =
+    isYes (p `decEqv` q) || isK r
   isRedexE defs (TypeCase {ty, ret, _}) =
     isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
   isRedexE _ (CloE  {}) = True
@@ -196,10 +222,10 @@ mutual
 
   ||| a reducible term
   |||
-  ||| - a reducible elimination, as `isRedexE`
-  ||| - an annotated elimination
-  |||   (the annotation is redundant in a checkable context)
-  ||| - a closure
+  ||| 1. a reducible elimination, as `isRedexE`
+  ||| 2. an annotated elimination
+  |||    (the annotation is redundant in a checkable context)
+  ||| 3. a closure
   public export
   isRedexT : RedexTest Term
   isRedexT _    (CloT  {}) = True
diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index 0274c65..008ed9c 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -140,23 +140,31 @@ CanWhnf Elim Interface.isRedexE where
 
   whnf defs ctx (Coe (S _ (N ty)) _ _ val coeLoc) =
     whnf defs ctx $ Ann val ty coeLoc
-  whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) = do
-    Element ty  tynf  <- whnf defs (extendDim i ctx) ty
-    Element val valnf <- whnf defs ctx val
-    pushCoe defs ctx i ty p q val coeLoc
+  whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) =
+    case p `decEqv` q of
+      Yes y   => whnf defs ctx $ Ann val (ty // one q) coeLoc
+      No  npq => do
+        Element ty tynf <- whnf defs (extendDim i ctx) ty
+        case nchoose $ canPushCoe ty val of
+          Left y =>
+            pushCoe defs ctx i ty p q val coeLoc
+          Right npc =>
+            -- [fixme] what about ty.zero = ty.one????
+            pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
+                           (tynf `orNo` npc `orNo` notYesNo npq)
 
   whnf defs ctx (Comp ty p q val r zero one compLoc) =
-    -- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
-    if p == q then whnf defs ctx $ Ann val ty compLoc 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
+    case p `decEqv` q of
+      -- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
+      Yes y   => whnf defs ctx $ Ann val ty compLoc
+      No  npq => case r of
+        -- comp [A] @p @q s @0 { 0 𝑗 ⇒ t₀; ⋯ } ⇝ t₀‹q/𝑗› ∷ A
         K Zero _ => whnf defs ctx $ Ann (dsub1 zero q) ty compLoc
+        -- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
         K One  _ => whnf defs ctx $ Ann (dsub1 one  q) ty compLoc
-      Right nk => do
-        Element ty tynf <- whnf defs ctx ty
-        pure $ Element (Comp ty p q val r zero one compLoc) $ tynf `orNo` nk
+        B {}     =>
+          pure $ Element (Comp ty p q val r zero one compLoc)
+                         (notYesNo npq `orNo` Ah)
 
   whnf defs ctx (TypeCase ty ret arms def tcLoc) = do
     Element ty  tynf  <- whnf defs ctx ty