diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 978a65f..7a3185f 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -74,6 +74,11 @@ compareU : CanEqual' q _ m => Universe -> Universe -> m ()
 compareU k l = unless !(compareU' k l) $
   throwError $ ClashU !mode k l
 
+export %inline
+compareD : HasErr q m => Dim d -> Dim d -> m ()
+compareD p q = unless (p == q) $
+  throwError $ ClashD p q
+
 mutual
   private covering
   compareTN' : CanEqual' q _ m => Eq q =>
@@ -96,14 +101,25 @@ mutual
   compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
     unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
     compareT0  arg2 arg1 -- reversed for contravariant domain
-    compareTS0 res1 res2
+    compareST0 res1 res2
   compareTN' s@(Pi {}) t _ _ = clashT s t
 
   -- [todo] eta
   compareTN' (Lam _ body1) (Lam _ body2) _ _ =
-    local {mode := Equal} $ compareTS0 body1 body2
+    local {mode := Equal} $ compareST0 body1 body2
   compareTN' s@(Lam {}) t _ _ = clashT s t
 
+  compareTN' (Eq _ ty1 l1 r1) (Eq _ ty2 l2 r2) _ _ = do
+    compareDST0 ty1 ty2
+    local {mode := Equal} $ do
+      compareT0 l1 l2
+      compareT0 r1 r2
+  compareTN' s@(Eq {}) t _ _ = clashT s t
+
+  compareTN' (DLam _ body1) (DLam _ body2) _ _ =
+    compareDST0 body1 body2
+  compareTN' s@(DLam {}) t _ _ = clashT s t
+
   compareTN' (CloT  {}) _ ps _ = void $ ps IsCloT
   compareTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
 
@@ -136,6 +152,11 @@ mutual
       compareT0 arg1 arg2
   compareEN' e@(_ :@ _) f _ _ = clashE e f
 
+  compareEN' (fun1 :% dim1) (fun2 :% dim2) _ _ = do
+    compareE0 fun1 fun2
+    compareD dim1 dim2
+  compareEN' e@(_ :% _) f _ _ = clashE e f
+
   -- [todo] is always checking the types are equal correct?
   compareEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
     compareT0 tm1 tm2
@@ -179,12 +200,18 @@ mutual
   compareE0 e f = compareEN (whnfE e) (whnfE f)
 
   export covering %inline
-  compareTS0 : CanEqual' q _ m => Eq q =>
+  compareST0 : CanEqual' q _ m => Eq q =>
                ScopeTerm q 0 n -> ScopeTerm q 0 n -> m ()
-  compareTS0 (TUnused body1) (TUnused body2) =
-    compareT0 body1 body2
-  compareTS0 body1 body2 =
-    compareT0 (fromScopeTerm body1) (fromScopeTerm body2)
+  compareST0 (TUnused body0) (TUnused body1) = compareT0 body0 body1
+  compareST0 body0 body1 = compareT0 body0.term body1.term
+
+  export covering %inline
+  compareDST0 : CanEqual' q _ m => Eq q =>
+                DScopeTerm q 0 n -> DScopeTerm q 0 n -> m ()
+  compareDST0 (DUnused body0) (DUnused body1) = compareT0 body0 body1
+  compareDST0 body0 body1 = do
+    compareT0 body0.zero body1.zero
+    compareT0 body0.one  body1.one
 
 
 private %inline
diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr
index 03ef47b..4ac727f 100644
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@@ -42,6 +42,8 @@ data PPrec
 = Outer
 | Ann  -- right of "::"
 | AnnL -- left  of "::"
+| Eq   -- "_ ≡ _ : _"
+| InEq -- arguments of ≡
   -- ...
 | App  -- term/dimension application
 | SApp -- substitution application
@@ -66,9 +68,17 @@ hlF' : Functor f => HL -> f (Doc HL) -> f (Doc HL)
 hlF' = map . hl'
 
 
+export %inline
+delims : Doc HL -> Doc HL -> Doc HL -> Doc HL
+delims l r doc = hl Delim l <+> doc <+> hl Delim r
+
 export %inline
 parens : Doc HL -> Doc HL
-parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
+parens = delims "(" ")"
+
+export %inline
+bracks : Doc HL -> Doc HL
+bracks = delims "[" "]"
 
 export %inline
 parensIf : Bool -> Doc HL -> Doc HL
@@ -125,10 +135,14 @@ withPrec d = local {prec := d}
 
 public export data BinderSort = T | D
 
+export %inline
+unders : HasEnv m => BinderSort -> List Name -> m a -> m a
+unders T xs = local {prec := Outer, tnames $= (xs ++)}
+unders D xs = local {prec := Outer, dnames $= (xs ++)}
+
 export %inline
 under : HasEnv m => BinderSort -> Name -> m a -> m a
-under T x = local {prec := Outer, tnames $= (x ::)}
-under D x = local {prec := Outer, dnames $= (x ::)}
+under t x = unders t [x]
 
 
 public export
diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index f3ae58c..102f6f7 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -67,7 +67,7 @@ prettyDSubst th =
     !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
 
 
-export FromVar Dim where fromVar = B
+public export FromVar Dim where fromVar = B
 
 export
 CanShift Dim where
@@ -106,3 +106,9 @@ DecEq (Dim d) where
   decEq (B i) (B j) with (decEq i j)
     _ | Yes prf    = Yes $ cong B prf
     _ | No  contra = No  $ contra . injective
+
+||| abbreviation for a bound variable like `BV 4` instead of
+||| `B (VS (VS (VS (VS VZ))))`
+public export %inline
+BV : (i : Nat) -> (0 _ : LT i d) => Dim d
+BV i = B $ V i
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index a9aa9ac..665e0fc 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -23,13 +23,15 @@ import Data.Vect
 
 
 infixl 8 :#
-infixl 9 :@
+infixl 9 :@, :%
 mutual
   public export
-  TSubst : Type -> Nat -> Nat -> Nat -> Type
-  TSubst q d = Subst (\n => Elim q d n)
+  0 TSubst : Type -> Nat -> Nat -> Nat -> Type
+  TSubst q d = Subst $ Elim q d
 
-  ||| first argument `d` is dimension scope size, second `n` is term scope size
+  ||| first argument `q` is quantity type;
+  ||| second argument `d` is dimension scope size;
+  ||| third `n` is term scope size
   public export
   data Term : (q : Type) -> (d, n : Nat) -> Type where
     ||| type of types
@@ -41,6 +43,12 @@ mutual
     ||| function term
     Lam : (x : Name) -> (body : ScopeTerm q d n) -> Term q d n
 
+    ||| equality type
+    Eq : (i : Name) -> (ty : DScopeTerm q d n) -> (l, r : Term q d n) ->
+         Term q d n
+    ||| equality term
+    DLam : (i : Name) -> (body : DScopeTerm q d n) -> Term q d n
+
     ||| elimination
     E : (e : Elim q d n) -> Term q d n
 
@@ -62,6 +70,9 @@ mutual
     ||| term application
     (:@) : (fun : Elim q d n) -> (arg : Term q d n) -> Elim q d n
 
+    ||| dim application
+    (:%) : (fun : Elim q d n) -> (arg : Dim d) -> Elim q d n
+
     ||| type-annotated term
     (:#) : (tm, ty : Term q d n) -> Elim q d n
 
@@ -93,10 +104,16 @@ mutual
 %name ScopeTerm body
 %name DScopeTerm body
 
+||| non dependent function type
 public export %inline
 Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n
 Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
 
+||| non dependent equality type
+public export %inline
+Eq0 : (ty, l, r : Term q d n) -> Term q d n
+Eq0 {ty, l, r} = Eq {i = "_", ty = DUnused ty, l, r}
+
 ||| same as `F` but as a term
 public export %inline
 FT : Name -> Term q d n
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index 27a0b00..3c9cf08 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -10,20 +10,18 @@ import Data.Vect
 %default total
 
 
-parameters {auto _ : Pretty.HasEnv m}
-  private %inline arrowD : m (Doc HL)
-  arrowD = hlF Syntax $ ifUnicode "→" "->"
+private %inline
+arrowD, lamD, eqndD, dlamD, annD : Pretty.HasEnv m => m (Doc HL)
+arrowD = hlF Syntax $ ifUnicode "→"  "->"
+lamD   = hlF Syntax $ ifUnicode "λ"  "fun"
+eqndD  = hlF Syntax $ ifUnicode "≡"  "=="
+dlamD  = hlF Syntax $ ifUnicode "λᴰ" "dfun"
+annD   = hlF Syntax $ ifUnicode "∷"  "::"
 
-  private %inline lamD : m (Doc HL)
-  lamD = hlF Syntax $ ifUnicode "λ" "fun"
-
-  private %inline annD : m (Doc HL)
-  annD = hlF Syntax $ ifUnicode "⦂" "::"
-
-private %inline typeD : Doc HL
-typeD = hl Syntax "Type"
-
-private %inline colonD : Doc HL
+private %inline
+typeD, eqD, colonD : Doc HL
+typeD  = hl Syntax "Type"
+eqD    = hl Syntax "Eq"
 colonD = hl Syntax ":"
 
 mutual
@@ -36,11 +34,23 @@ mutual
         !(prettyBinder [qty] x s) <++> !arrowD
           <//> !(under T x $ prettyM t)
     prettyM (Lam x t) =
-      parensIfM Outer $
-        sep [!lamD, hl TVar !(prettyM x), !arrowD]
-          <//> !(under T x $ prettyM t)
-    prettyM (E e) =
-      pure $ hl Delim "[" <+> !(prettyM e) <+> hl Delim "]"
+      let GotLams {names, body, _} = getLams' [x] t.term Refl in
+      prettyLams T (toList names) body
+    prettyM (Eq _ (DUnused ty) l r) =
+      parensIfM Eq !(withPrec InEq $ pure $
+        sep [!(prettyM l) <++> !eqndD, !(prettyM r) <++> colonD, !(prettyM ty)])
+    prettyM (Eq i (DUsed ty) l r) =
+      parensIfM App $
+        eqD <++>
+        sep [bracks !(withPrec Outer $ pure $ hang 2 $
+               sep [hl DVar !(prettyM i) <++> !arrowD,
+                    !(under D i $ prettyM ty)]),
+             !(withPrec Arg $ prettyM l),
+             !(withPrec Arg $ prettyM r)]
+    prettyM (DLam i t) =
+      let GotDLams {names, body, _} = getDLams' [i] t.term Refl in
+      prettyLams D (toList names) body
+    prettyM (E e) = bracks <$> prettyM e
     prettyM (CloT s th) =
       parensIfM SApp . hang 2 =<<
         [|withPrec SApp (prettyM s) </> prettyTSubst th|]
@@ -55,9 +65,11 @@ mutual
     prettyM (B i) =
       prettyVar TVar TVarErr (!ask).tnames i
     prettyM (e :@ s) =
-      let GotArgs f args _ = getArgs' e [s] in
-      parensIfM App =<< withPrec Arg
-        [|prettyM f <//> (align . sep <$> traverse prettyM args)|]
+      let GotArgs {fun, args, _} = getArgs' e [s] in
+      prettyApps fun args
+    prettyM (e :% d) =
+      let GotDArgs {fun, args, _} = getDArgs' e [d] in
+      prettyApps fun args
     prettyM (s :# a) =
       parensIfM Ann $ hang 2 $
         !(withPrec AnnL $ prettyM s) <++> !annD
@@ -71,7 +83,7 @@ mutual
 
   export covering
   PrettyHL q => PrettyHL (ScopeTerm q d n) where
-    prettyM body = prettyM $ fromScopeTerm body
+    prettyM body = prettyM body.term
 
   export covering
   prettyTSubst : Pretty.HasEnv m => PrettyHL q =>
@@ -86,3 +98,19 @@ mutual
       hsep [hl TVar !(prettyM x),
             sep [!(prettyQtyBinds pis),
                  hsep [colonD, !(withPrec Outer $ prettyM a)]]]
+
+  export covering
+  prettyLams : Pretty.HasEnv m => PrettyHL q =>
+               BinderSort -> List Name -> Term q _ _ -> m (Doc HL)
+  prettyLams sort names body = do
+    lam    <- case sort of T => lamD; D => dlamD
+    header <- sequence $ [hl TVar <$> prettyM x | x <- names] ++ [arrowD]
+    body   <- unders sort names $ prettyM body
+    parensIfM Outer $ sep (lam :: header) <//> body
+
+  export covering
+  prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a =>
+               f -> List a -> m (Doc HL)
+  prettyApps fun args =
+    parensIfM App =<< withPrec Arg
+      [|prettyM fun <//> (align . sep <$> traverse prettyM args)|]
diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Syntax/Term/Reduce.idr
index 5bce4dd..44e65fa 100644
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@@ -12,24 +12,29 @@ mutual
     NCTYPE : NotCloT $ TYPE _
     NCPi   : NotCloT $ Pi {}
     NCLam  : NotCloT $ Lam {}
+    NCEq   : NotCloT $ Eq {}
+    NCDLam : NotCloT $ DLam {}
     NCE    : NotCloE e -> NotCloT $ E e
 
   public export
   data NotCloE : Elim {} -> Type where
-    NCF   : NotCloE $ F _
-    NCB   : NotCloE $ B _
-    NCApp : NotCloE $ _ :@ _
-    NCAnn : NotCloE $ _ :# _
+    NCF    : NotCloE $ F _
+    NCB    : NotCloE $ B _
+    NCApp  : NotCloE $ _ :@ _
+    NCDApp : NotCloE $ _ :% _
+    NCAnn  : NotCloE $ _ :# _
 
 mutual
   export
   notCloT : (t : Term {}) -> Dec (NotCloT t)
-  notCloT (TYPE _) = Yes NCTYPE
-  notCloT (Pi {})  = Yes NCPi
-  notCloT (Lam {}) = Yes NCLam
-  notCloT (E e) with (notCloE e)
-    notCloT (E e) | Yes nc = Yes $ NCE nc
-    notCloT (E e) | No  c  = No  $ \case NCE nc => c nc
+  notCloT (TYPE _)  = Yes NCTYPE
+  notCloT (Pi {})   = Yes NCPi
+  notCloT (Lam {})  = Yes NCLam
+  notCloT (Eq {})   = Yes NCEq
+  notCloT (DLam {}) = Yes NCDLam
+  notCloT (E e) = case notCloE e of
+    Yes nc => Yes $ NCE nc
+    No  c  => No  $ \case NCE nc => c nc
   notCloT (CloT {})  = No $ \case _ impossible
   notCloT (DCloT {}) = No $ \case _ impossible
 
@@ -38,26 +43,27 @@ mutual
   notCloE (F _)      = Yes NCF
   notCloE (B _)      = Yes NCB
   notCloE (_ :@ _)   = Yes NCApp
+  notCloE (_ :% _)   = Yes NCDApp
   notCloE (_ :# _)   = Yes NCAnn
   notCloE (CloE  {}) = No $ \case _ impossible
   notCloE (DCloE {}) = No $ \case _ impossible
 
 ||| a term which is not a top level closure
 public export
-NotCloTerm : Type -> Nat -> Nat -> Type
-NotCloTerm q d n = Subset (Term q d n) NotCloT
+NonCloTerm : Type -> Nat -> Nat -> Type
+NonCloTerm q d n = Subset (Term q d n) NotCloT
 
 ||| an elimination which is not a top level closure
 public export
-NotCloElim : Type -> Nat -> Nat -> Type
-NotCloElim q d n = Subset (Elim q d n) NotCloE
+NonCloElim : Type -> Nat -> Nat -> Type
+NonCloElim q d n = Subset (Elim q d n) NotCloE
 
 public export %inline
-ncloT : (t : Term q d n) -> (0 _ : NotCloT t) => NotCloTerm q d n
+ncloT : (t : Term q d n) -> (0 _ : NotCloT t) => NonCloTerm q d n
 ncloT t @{p} = Element t p
 
 public export %inline
-ncloE : (e : Elim q d n) -> (0 _ : NotCloE e) => NotCloElim q d n
+ncloE : (e : Elim q d n) -> (0 _ : NotCloE e) => NonCloElim q d n
 ncloE e @{p} = Element e p
 
 
@@ -66,34 +72,38 @@ mutual
   ||| if the input term has any top-level closures, push them under one layer of
   ||| syntax
   export %inline
-  pushSubstsT : Term q d n -> NotCloTerm q d n
+  pushSubstsT : Term q d n -> NonCloTerm q d n
   pushSubstsT s = pushSubstsTWith id id s
 
   ||| if the input elimination has any top-level closures, push them under one
   ||| layer of syntax
   export %inline
-  pushSubstsE : Elim q d n -> NotCloElim q d n
+  pushSubstsE : Elim q d n -> NonCloElim q d n
   pushSubstsE e = pushSubstsEWith id id e
 
   export
   pushSubstsTWith : DSubst dfrom dto -> TSubst q dto from to ->
-                    Term q dfrom from -> NotCloTerm q dto to
+                    Term q dfrom from -> NonCloTerm q dto to
   pushSubstsTWith th ph (TYPE l) =
     ncloT $ TYPE l
   pushSubstsTWith th ph (Pi qty x a body) =
     ncloT $ Pi qty x (subs a th ph) (subs body th ph)
   pushSubstsTWith th ph (Lam x body) =
     ncloT $ Lam x $ subs body th ph
+  pushSubstsTWith th ph (Eq i ty l r) =
+    ncloT $ Eq i (subs ty th ph) (subs l th ph) (subs r th ph)
+  pushSubstsTWith th ph (DLam i body) =
+    ncloT $ DLam i $ subs body th ph
   pushSubstsTWith th ph (E e) =
-    let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
-  pushSubstsTWith th ph (CloT  s ps) =
-    pushSubstsTWith th (comp' th ps ph) s
+    let Element e nc = pushSubstsEWith th ph e in ncloT $ E e
+  pushSubstsTWith th ph (CloT s ps) =
+    pushSubstsTWith th (comp th ps ph) s
   pushSubstsTWith th ph (DCloT s ps) =
     pushSubstsTWith (ps . th) ph s
 
   export
   pushSubstsEWith : DSubst dfrom dto -> TSubst q dto from to ->
-                    Elim q dfrom from -> NotCloElim q dto to
+                    Elim q dfrom from -> NonCloElim q dto to
   pushSubstsEWith th ph (F x) =
     ncloE $ F x
   pushSubstsEWith th ph (B i) =
@@ -103,10 +113,12 @@ mutual
          No  _ => assert_total pushSubstsE res
   pushSubstsEWith th ph (f :@ s) =
     ncloE $ subs f th ph :@ subs s th ph
+  pushSubstsEWith th ph (f :% d) =
+    ncloE $ subs f th ph :% (d // th)
   pushSubstsEWith th ph (s :# a) =
     ncloE $ subs s th ph :# subs a th ph
-  pushSubstsEWith th ph (CloE  e ps) =
-    pushSubstsEWith th (comp' th ps ph) e
+  pushSubstsEWith th ph (CloE e ps) =
+    pushSubstsEWith th (comp th ps ph) e
   pushSubstsEWith th ph (DCloE e ps) =
     pushSubstsEWith (ps . th) ph e
 
@@ -121,57 +133,6 @@ parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to)
   pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
 
 
-public export %inline
-pushSubstsT' : Term q d n -> Term q d n
-pushSubstsT' s = (pushSubstsT s).fst
-
-public export %inline
-pushSubstsE' : Elim q d n -> Elim q d n
-pushSubstsE' e = (pushSubstsE e).fst
-
-
--- mutual
---   -- tightening a term/elim also causes substitutions to be pushed through.
---   -- this is because otherwise a variable in an unused part of the subst
---   -- would cause it to incorrectly fail
-
---   export covering
---   Tighten (Term d) where
---     tighten p (TYPE l) =
---       pure $ TYPE l
---     tighten p (Pi qty x arg res) =
---       Pi qty x <$> tighten p arg
---                <*> tighten p res
---     tighten p (Lam x body) =
---       Lam x <$> tighten p body
---     tighten p (E e) =
---       E <$> tighten p e
---     tighten p (CloT tm th) =
---       tighten p $ pushSubstsTWith' id th tm
---     tighten p (DCloT tm th) =
---       tighten p $ pushSubstsTWith' th id tm
-
---   export covering
---   Tighten (Elim d) where
---     tighten p (F x) =
---       pure $ F x
---     tighten p (B i) =
---       B <$> tighten p i
---     tighten p (fun :@ arg) =
---       [|tighten p fun :@ tighten p arg|]
---     tighten p (tm :# ty) =
---       [|tighten p tm :# tighten p ty|]
---     tighten p (CloE el th) =
---       tighten p $ pushSubstsEWith' id th el
---     tighten p (DCloE el th) =
---       tighten p $ pushSubstsEWith' th id el
-
---   export covering
---   Tighten (ScopeTerm d) where
---     tighten p (TUsed   body) = TUsed   <$> tighten (Keep p) body
---     tighten p (TUnused body) = TUnused <$> tighten p body
-
-
 public export %inline
 weakT : Term q d n -> Term q d (S n)
 weakT t = t //. shift 1
@@ -189,24 +150,26 @@ mutual
     IsDCloT    : IsRedexT $ DCloT {}
     IsERedex   : IsRedexE e -> IsRedexT $ E e
 
-  public export %inline
-  NotRedexT : Term q d n -> Type
-  NotRedexT = Not . IsRedexT
-
   public export
   data IsRedexE : Elim q d n -> Type where
     IsUpsilonE : IsRedexE $ E _ :# _
-    IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
+    IsBetaLam  : IsRedexE $ (Lam {}  :# Pi {}) :@ _
+    IsBetaDLam : IsRedexE $ (DLam {} :# Eq {}) :% _
     IsCloE     : IsRedexE $ CloE {}
     IsDCloE    : IsRedexE $ DCloE {}
 
-  public export %inline
-  NotRedexE : Elim q d n -> Type
-  NotRedexE = Not . IsRedexE
+public export %inline
+NotRedexT : Term q d n -> Type
+NotRedexT = Not . IsRedexT
+
+public export %inline
+NotRedexE : Elim q d n -> Type
+NotRedexE = Not . IsRedexE
 
 
 mutual
-  export %inline
+  -- [todo] PLEASE replace these with macros omfg
+  export
   isRedexT : (t : Term {}) -> Dec (IsRedexT t)
   isRedexT (E (tm :# ty)) = Yes IsUpsilonT
   isRedexT (CloT {})      = Yes IsCloT
@@ -216,16 +179,22 @@ mutual
   isRedexT (E e@(_ :@ _)) with (isRedexE e)
     _ | Yes yes = Yes $ IsERedex yes
     _ | No  no  = No  $ \case IsERedex p => no p
+  isRedexT (E e@(_ :% _)) with (isRedexE e)
+    _ | Yes yes = Yes $ IsERedex yes
+    _ | No  no  = No  $ \case IsERedex p => no p
   isRedexT (TYPE {}) = No $ \case _ impossible
   isRedexT (Pi   {}) = No $ \case _ impossible
   isRedexT (Lam  {}) = No $ \case _ impossible
+  isRedexT (Eq   {}) = No $ \case _ impossible
+  isRedexT (DLam {}) = No $ \case _ impossible
   isRedexT (E (F _)) = No $ \case IsERedex _ impossible
   isRedexT (E (B _)) = No $ \case IsERedex _ impossible
 
-  export %inline
+  export
   isRedexE : (e : Elim {}) -> Dec (IsRedexE e)
   isRedexE (E _ :# _)                    = Yes IsUpsilonE
-  isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
+  isRedexE ((Lam {}  :# Pi {}) :@ _)     = Yes IsBetaLam
+  isRedexE ((DLam {} :# Eq {}) :% _)     = Yes IsBetaDLam
   isRedexE (CloE {})                     = Yes IsCloE
   isRedexE (DCloE {})                    = Yes IsDCloE
   isRedexE (F x)                         = No $ \case _ impossible
@@ -233,21 +202,48 @@ mutual
   isRedexE (F _                    :@ _) = No $ \case _ impossible
   isRedexE (B _                    :@ _) = No $ \case _ impossible
   isRedexE (_ :@ _                 :@ _) = No $ \case _ impossible
+  isRedexE (_ :% _                 :@ _) = No $ \case _ impossible
+  isRedexE (CloE {}                :@ _) = No $ \case _ impossible
+  isRedexE (DCloE {}               :@ _) = No $ \case _ impossible
   isRedexE ((TYPE _   :# _)        :@ _) = No $ \case _ impossible
   isRedexE ((Pi {}    :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((Eq {}    :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((DLam {}  :# _)        :@ _) = No $ \case _ impossible
   isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \case _ impossible
-  isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# Lam  {})  :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# Eq   {})  :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# DLam {})  :@ _) = No $ \case _ impossible
   isRedexE ((Lam {}   :# E _)      :@ _) = No $ \case _ impossible
-  isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# CloT  {}) :@ _) = No $ \case _ impossible
   isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \case _ impossible
   isRedexE ((E _      :# _)        :@ _) = No $ \case _ impossible
   isRedexE ((CloT {}  :# _)        :@ _) = No $ \case _ impossible
   isRedexE ((DCloT {} :# _)        :@ _) = No $ \case _ impossible
-  isRedexE (CloE {}                :@ _) = No $ \case _ impossible
-  isRedexE (DCloE {}               :@ _) = No $ \case _ impossible
+  isRedexE ((TYPE _   :# _)        :% _) = No $ \case _ impossible
+  isRedexE ((Pi {}    :# _)        :% _) = No $ \case _ impossible
+  isRedexE ((Eq {}    :# _)        :% _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# _)        :% _) = No $ \case _ impossible
+  isRedexE ((DLam {}  :# TYPE _)   :% _) = No $ \case _ impossible
+  isRedexE ((DLam {}  :# Pi   {})  :% _) = No $ \case _ impossible
+  isRedexE ((DLam {}  :# Lam  {})  :% _) = No $ \case _ impossible
+  isRedexE ((DLam {}  :# DLam {})  :% _) = No $ \case _ impossible
+  isRedexE ((DLam {}  :# E _)      :% _) = No $ \case _ impossible
+  isRedexE ((DLam {}  :# CloT  {}) :% _) = No $ \case _ impossible
+  isRedexE ((DLam {}  :# DCloT {}) :% _) = No $ \case _ impossible
+  isRedexE ((E _      :# _)        :% _) = No $ \case _ impossible
+  isRedexE ((CloT {}  :# _)        :% _) = No $ \case _ impossible
+  isRedexE ((DCloT {} :# _)        :% _) = No $ \case _ impossible
+  isRedexE (F _                    :% _) = No $ \case _ impossible
+  isRedexE (B _                    :% _) = No $ \case _ impossible
+  isRedexE (_ :@ _                 :% _) = No $ \case _ impossible
+  isRedexE (_ :% _                 :% _) = No $ \case _ impossible
+  isRedexE (CloE {}                :% _) = No $ \case _ impossible
+  isRedexE (DCloE {}               :% _) = No $ \case _ impossible
   isRedexE (TYPE _   :# _)               = No $ \case _ impossible
   isRedexE (Pi {}    :# _)               = No $ \case _ impossible
   isRedexE (Lam {}   :# _)               = No $ \case _ impossible
+  isRedexE (Eq {}    :# _)               = No $ \case _ impossible
+  isRedexE (DLam {}  :# _)               = No $ \case _ impossible
   isRedexE (CloT {}  :# _)               = No $ \case _ impossible
   isRedexE (DCloT {} :# _)               = No $ \case _ impossible
 
@@ -272,8 +268,7 @@ NonRedexElim q d n = Subset (Elim q d n) NotRedexE
 ||| substitute a term with annotation for the bound variable of a `ScopeTerm`
 export %inline
 substScope : (arg, argTy : Term q d n) -> (body : ScopeTerm q d n) -> Term q d n
-substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
-substScope arg argTy (TUnused body) = body
+substScope arg argTy body = sub1 body (arg :# argTy)
 
 mutual
   export %inline
@@ -287,7 +282,12 @@ mutual
   stepE' : (e : Elim q d n) -> IsRedexE e -> Elim q d n
   stepE' (E e :# _) IsUpsilonE = e
   stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
-    substScope s arg body :# substScope s arg res
+    let s = s :# arg in sub1 body s :# sub1 res s
+  stepE' ((DLam {body, _} :# Eq {ty, l, r, _}) :% dim) IsBetaDLam =
+    case dim of
+      K Zero => l :# ty.zero
+      K One  => r :# ty.one
+      B _    => dsub1 body dim :# dsub1 ty dim
   stepE' (CloE  e th) IsCloE  = pushSubstsEWith' id th e
   stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
 
@@ -301,12 +301,38 @@ stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
 
 export covering
 whnfT : Term q d n -> NonRedexTerm q d n
-whnfT s = case stepT s of
-               Right s'   => whnfT s'
-               Left  done => Element s done
+whnfT s = case stepT s of Right s' => whnfT s'; Left done => Element s done
 
 export covering
 whnfE : Elim q d n -> NonRedexElim q d n
-whnfE e = case stepE e of
-               Right e'   => whnfE e'
-               Left  done => Element e done
+whnfE e = case stepE e of Right e' => whnfE e'; Left done => Element e done
+
+
+export
+notRedexNotCloE : (e : Elim {}) -> NotRedexE e -> NotCloE e
+notRedexNotCloE (F x)         f = NCF
+notRedexNotCloE (B i)         f = NCB
+notRedexNotCloE (fun :@ arg)  f = NCApp
+notRedexNotCloE (fun :% arg)  f = NCDApp
+notRedexNotCloE (tm :# ty)    f = NCAnn
+notRedexNotCloE (CloE el th)  f = absurd $ f IsCloE
+notRedexNotCloE (DCloE el th) f = absurd $ f IsDCloE
+
+export
+notRedexNotCloT : (t : Term {}) -> NotRedexT t -> NotCloT t
+notRedexNotCloT (TYPE _)   _ = NCTYPE
+notRedexNotCloT (Pi {})    _ = NCPi
+notRedexNotCloT (Lam {})   _ = NCLam
+notRedexNotCloT (Eq {})    _ = NCEq
+notRedexNotCloT (DLam {})  _ = NCDLam
+notRedexNotCloT (E e)      f = NCE $ notRedexNotCloE e $ f . IsERedex
+notRedexNotCloT (CloT  {}) f = absurd $ f IsCloT
+notRedexNotCloT (DCloT {}) f = absurd $ f IsDCloT
+
+export
+toNotCloE : NonRedexElim q d n -> NonCloElim q d n
+toNotCloE (Element e prf) = Element e $ notRedexNotCloE e prf
+
+export
+toNotCloT : NonRedexTerm q d n -> NonCloTerm q d n
+toNotCloT (Element t prf) = Element t $ notRedexNotCloT t prf
diff --git a/lib/Quox/Syntax/Term/Split.idr b/lib/Quox/Syntax/Term/Split.idr
index 297b893..091b227 100644
--- a/lib/Quox/Syntax/Term/Split.idr
+++ b/lib/Quox/Syntax/Term/Split.idr
@@ -10,41 +10,79 @@ import Data.Vect
 
 
 public export
-data IsLam : Term {} -> Type where
-  ItIsLam : IsLam $ Lam x body
+data IsLam : Pred $ Term {} where ItIsLam : IsLam $ Lam x body
 
 public export %inline
-isLam : (s : Term {}) -> Dec (IsLam s)
+isLam : Dec1 IsLam
 isLam (TYPE _)   = No $ \case _ impossible
 isLam (Pi {})    = No $ \case _ impossible
 isLam (Lam {})   = Yes ItIsLam
+isLam (Eq {})    = No $ \case _ impossible
+isLam (DLam {})  = No $ \case _ impossible
 isLam (E _)      = No $ \case _ impossible
 isLam (CloT {})  = No $ \case _ impossible
 isLam (DCloT {}) = No $ \case _ impossible
 
-public export %inline
-NotLam : Term {} -> Type
+public export
+0 NotLam : Pred $ Term {}
 NotLam = Not . IsLam
 
 
 public export
-data IsApp : Elim {} -> Type where
-  ItIsApp : IsApp $ f :@ s
+data IsDLam : Pred $ Term {} where ItIsDLam : IsDLam $ DLam i body
 
 public export %inline
-isApp : (e : Elim {}) -> Dec (IsApp e)
+isDLam : Dec1 IsDLam
+isDLam (TYPE _)   = No $ \case _ impossible
+isDLam (Pi {})    = No $ \case _ impossible
+isDLam (Eq {})    = No $ \case _ impossible
+isDLam (Lam {})   = No $ \case _ impossible
+isDLam (DLam {})  = Yes ItIsDLam
+isDLam (E _)      = No $ \case _ impossible
+isDLam (CloT {})  = No $ \case _ impossible
+isDLam (DCloT {}) = No $ \case _ impossible
+
+public export
+0 NotDLam : Pred $ Term {}
+NotDLam = Not . IsDLam
+
+
+public export
+data IsApp : Pred $ Elim {} where ItIsApp : IsApp $ f :@ s
+
+public export %inline
+isApp : Dec1 IsApp
 isApp (F _)      = No $ \case _ impossible
 isApp (B _)      = No $ \case _ impossible
 isApp (_ :@ _)   = Yes ItIsApp
+isApp (_ :% _)   = No $ \case _ impossible
 isApp (_ :# _)   = No $ \case _ impossible
 isApp (CloE {})  = No $ \case _ impossible
 isApp (DCloE {}) = No $ \case _ impossible
 
 public export
-NotApp : Elim {} -> Type
+0 NotApp : Pred $ Elim {}
 NotApp = Not . IsApp
 
 
+public export
+data IsDApp : Pred $ Elim {} where ItIsDApp : IsDApp $ f :% d
+
+public export %inline
+isDApp : Dec1 IsDApp
+isDApp (F _)      = No $ \case _ impossible
+isDApp (B _)      = No $ \case _ impossible
+isDApp (_ :@ _)   = No $ \case _ impossible
+isDApp (_ :% _)   = Yes ItIsDApp
+isDApp (_ :# _)   = No $ \case _ impossible
+isDApp (CloE {})  = No $ \case _ impossible
+isDApp (DCloE {}) = No $ \case _ impossible
+
+public export
+0 NotDApp : Pred $ Elim {}
+NotDApp = Not . IsDApp
+
+
 infixl 9 :@@
 ||| apply multiple arguments at once
 public export %inline
@@ -61,8 +99,8 @@ record GetArgs q d n where
 export
 getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
 getArgs' fun args with (isApp fun)
-  getArgs' (f :@ a) args | Yes yes = getArgs' f (a :: args)
-  getArgs' fun args      | No  no  = GotArgs {fun, args, notApp = no}
+  getArgs' (f :@ a) args | Yes _  = getArgs' f (a :: args)
+  getArgs' fun args      | No  no = GotArgs {fun, args, notApp = no}
 
 ||| splits an application into its head and arguments. if it's not an
 ||| application then the list is just empty
@@ -71,6 +109,32 @@ getArgs : Elim q d n -> GetArgs q d n
 getArgs e = getArgs' e []
 
 
+infixl 9 :%%
+||| apply multiple dimension arguments at once
+public export %inline
+(:%%) : Elim q d n -> List (Dim d) -> Elim q d n
+f :%% ss = foldl (:%) f ss
+
+public export
+record GetDArgs q d n where
+  constructor GotDArgs
+  fun       : Elim q d n
+  args      : List (Dim d)
+  0 notDApp : NotDApp fun
+
+export
+getDArgs' : Elim q d n -> List (Dim d) -> GetDArgs q d n
+getDArgs' fun args with (isDApp fun)
+  getDArgs' (f :% a) args | Yes yes = getDArgs' f (a :: args)
+  getDArgs' fun args      | No  no  = GotDArgs {fun, args, notDApp = no}
+
+||| splits a dimension application into its head and arguments. if it's not an
+||| d application then the list is just empty
+export %inline
+getDArgs : Elim q d n -> GetDArgs q d n
+getDArgs e = getDArgs' e []
+
+
 infixr 1 :\\
 public export
 absN : Vect m Name -> Term q d (m + n) -> Term q d n
@@ -83,9 +147,22 @@ public export %inline
 (:\\) = absN
 
 
+infixr 1 :\\%
+public export
+dabsN : Vect m Name -> Term q (m + d) n -> Term q d n
+dabsN {m = 0}   []        s = s
+dabsN {m = S m} (x :: xs) s = DLam x $ DUsed $ dabsN xs $
+                              rewrite sym $ plusSuccRightSucc m d in s
+
+public export %inline
+(:\\%) : Vect m Name -> Term q (m + d) n -> Term q d n
+(:\\%) = dabsN
+
+
 public export
 record GetLams q d n where
   constructor GotLams
+  {0 lams, rest : Nat}
   names    : Vect lams Name
   body     : Term q d rest
   0 eq     : lams + n = rest
@@ -93,16 +170,38 @@ record GetLams q d n where
 
 export
 getLams' : forall lams, rest.
-           Vect lams Name -> Term q d rest -> lams + n = rest -> GetLams q d n
+           Vect lams Name -> Term q d rest -> (0 eq : lams + n = rest) ->
+           GetLams q d n
 getLams' xs s eq with (isLam s)
-  getLams' xs (Lam x sbody) Refl | Yes ItIsLam =
-    let 0 s  = Lam x sbody
-        body = assert_smaller s $ fromScopeTerm sbody
-    in
+  getLams' xs (Lam x sbody) Refl | Yes _ =
+    let body = assert_smaller (Lam x sbody) sbody.term in
     getLams' (x :: xs) body Refl
-  getLams' xs s eq | No no =
-    GotLams xs s eq no
+  getLams' xs s eq | No no = GotLams xs s eq no
 
-export
+export %inline
 getLams : Term q d n -> GetLams q d n
 getLams s = getLams' [] s Refl
+
+
+public export
+record GetDLams q d n where
+  constructor GotDLams
+  {0 lams, rest : Nat}
+  names     : Vect lams Name
+  body      : Term q rest n
+  0 eq      : lams + d = rest
+  0 notDLam : NotDLam body
+
+export
+getDLams' : forall lams, rest.
+           Vect lams Name -> Term q rest n -> (0 eq : lams + d = rest) ->
+           GetDLams q d n
+getDLams' is s eq with (isDLam s)
+  getDLams' is (DLam i sbody) Refl | Yes _ =
+    let body = assert_smaller (DLam i sbody) sbody.term in
+    getDLams' (i :: is) body Refl
+  getDLams' is s eq | No no = GotDLams is s eq no
+
+export %inline
+getDLams : Term q d n -> GetDLams q d n
+getDLams s = getDLams' [] s Refl
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 8165edd..100bfc1 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -5,11 +5,61 @@ import Quox.Syntax.Term.Base
 %default total
 
 
-export FromVar (Elim q d) where fromVar = B
-export FromVar (Term q d) where fromVar = E . fromVar
+infixl 8 ///
+mutual
+  namespace Term
+    ||| does the minimal reasonable work:
+    ||| - deletes the closure around an atomic constant like `TYPE`
+    ||| - deletes an identity substitution
+    ||| - composes (lazily) with an existing top-level dim-closure
+    ||| - otherwise, wraps in a new closure
+    export
+    (///) : Term q dfrom n -> DSubst dfrom dto -> Term q dto n
+    s          /// Shift SZ = s
+    TYPE l     /// _        = TYPE l
+    DCloT s ph /// th       = DCloT s $ ph . th
+    s          /// th       = DCloT s th
+
+  namespace Elim
+    private
+    subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
+    subDArgs (f :% d) th = subDArgs f th :% (d // th)
+    subDArgs e        th = DCloE e th
+
+    ||| does the minimal reasonable work:
+    ||| - deletes the closure around a term variable
+    ||| - deletes an identity substitution
+    ||| - composes (lazily) with an existing top-level dim-closure
+    ||| - immediately looks up bound variables in a
+    |||   top-level sequence of dimension applications
+    ||| - otherwise, wraps in a new closure
+    export
+    (///) : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
+    e          /// Shift SZ = e
+    F x        /// _        = F x
+    B i        /// _        = B i
+    f :% d     /// th       = subDArgs (f :% d) th
+    DCloE e ph /// th       = DCloE e $ ph . th
+    e          /// th       = DCloE e th
+
+  namespace ScopeTerm
+    export
+    (///) : ScopeTerm q dfrom n -> DSubst dfrom dto -> ScopeTerm q dto n
+    TUsed   body /// th = TUsed   $ body /// th
+    TUnused body /// th = TUnused $ body /// th
+
+  namespace DScopeTerm
+    export
+    (///) : DScopeTerm q dfrom n -> DSubst dfrom dto -> DScopeTerm q dto n
+    DUsed   body /// th = DUsed   $ body /// push th
+    DUnused body /// th = DUnused $ body /// th
+
+
+export %inline FromVar (Elim q d) where fromVar = B
+export %inline FromVar (Term q d) where fromVar = E . fromVar
 
 ||| does the minimal reasonable work:
-||| - deletes the closure around a free name since it doesn't do anything
+||| - deletes the closure around a *free* name
 ||| - deletes an identity substitution
 ||| - composes (lazily) with an existing top-level closure
 ||| - immediately looks up a bound variable
@@ -38,34 +88,30 @@ CanSubst (Elim q d) (Term q d) where
                          Shift SZ => s
                          th       => CloT s th
 
-export
+export %inline
 CanSubst (Elim q d) (ScopeTerm q d) where
   TUsed   body // th = TUsed   $ body // push th
   TUnused body // th = TUnused $ body // th
 
-export CanSubst Var (Term      q d) where s // th = s // map (B {q, d}) th
-export CanSubst Var (Elim      q d) where e // th = e // map (B {q, d}) th
-export CanSubst Var (ScopeTerm q d) where s // th = s // map (B {q, d}) th
+export %inline
+CanSubst (Elim q d) (DScopeTerm q d) where
+  DUsed   body // th = DUsed   $ body // map (/// shift 1) th
+  DUnused body // th = DUnused $ body // th
+
+export %inline CanSubst Var (Term       q d) where s // th = s // map (B {q, d}) th
+export %inline CanSubst Var (Elim       q d) where e // th = e // map (B {q, d}) th
+export %inline CanSubst Var (ScopeTerm  q d) where s // th = s // map (B {q, d}) th
+export %inline CanSubst Var (DScopeTerm q d) where s // th = s // map (B {q, d}) th
 
 
 infixl 8 //., ///
 mutual
   namespace Term
     ||| applies a term substitution with a less ambiguous type
-    export
+    export %inline
     (//.) : Term q d from -> TSubst q d from to -> Term q d to
     t //. th = t // th
 
-    ||| applies a dimension substitution with the same behaviour as `(//)`
-    ||| above
-    export
-    (///) : Term q dfrom n -> DSubst dfrom dto -> Term q dto n
-    TYPE l     /// _        = TYPE l
-    E e        /// th       = E $ e /// th
-    DCloT s ph /// th       = DCloT s $ ph . th
-    s          /// Shift SZ = s
-    s          /// th       = DCloT s th
-
     ||| applies a term and dimension substitution
     public export %inline
     subs : Term q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
@@ -74,20 +120,10 @@ mutual
 
   namespace Elim
     ||| applies a term substitution with a less ambiguous type
-    export
+    export %inline
     (//.) : Elim q d from -> TSubst q d from to -> Elim q d to
     e //. th = e // th
 
-    ||| applies a dimension substitution with the same behaviour as `(//)`
-    ||| above
-    export
-    (///) : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
-    F x        /// _        = F x
-    B i        /// _        = B i
-    DCloE e ph /// th       = DCloE e $ ph . th
-    e          /// Shift SZ = e
-    e          /// th       = DCloE e th
-
     ||| applies a term and dimension substitution
     public export %inline
     subs : Elim q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
@@ -96,40 +132,65 @@ mutual
 
   namespace ScopeTerm
     ||| applies a term substitution with a less ambiguous type
-    export
+    export %inline
     (//.) : ScopeTerm q d from -> TSubst q d from to -> ScopeTerm q d to
     body //. th = body // th
 
-    ||| applies a dimension substitution with the same behaviour as `(//)`
-    ||| above
-    export
-    (///) : ScopeTerm q dfrom n -> DSubst dfrom dto -> ScopeTerm q dto n
-    TUsed   body /// th = TUsed   $ body /// th
-    TUnused body /// th = TUnused $ body /// th
-
     ||| applies a term and dimension substitution
     public export %inline
     subs : ScopeTerm q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
            ScopeTerm q dto to
     subs body th ph = body /// th // ph
 
-export CanShift (Term      q d) where s // by = s //. Shift by
-export CanShift (Elim      q d) where e // by = e //. Shift by
-export CanShift (ScopeTerm q d) where s // by = s //. Shift by
+  namespace DScopeTerm
+    ||| applies a term substitution with a less ambiguous type
+    export %inline
+    (//.) : DScopeTerm q d from -> TSubst q d from to -> DScopeTerm q d to
+    body //. th = body // th
+
+    ||| applies a term and dimension substitution
+    public export %inline
+    subs : DScopeTerm q dfrom from -> DSubst dfrom dto -> TSubst q dto from to ->
+           DScopeTerm q dto to
+    subs body th ph = body /// th // ph
+
+export %inline CanShift (Term      q d) where s // by = s //. Shift by
+export %inline CanShift (Elim      q d) where e // by = e //. Shift by
+export %inline CanShift (ScopeTerm q d) where s // by = s //. Shift by
 
 
 export %inline
-comp' : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
-        TSubst q dto from to
-comp' th ps ph = map (/// th) ps . ph
+comp : DSubst dfrom dto -> TSubst q dfrom from mid -> TSubst q dto mid to ->
+       TSubst q dto from to
+comp th ps ph = map (/// th) ps . ph
 
 
-export
-fromDScopeTerm : DScopeTerm q d n -> Term q (S d) n
-fromDScopeTerm (DUsed   body) = body
-fromDScopeTerm (DUnused body) = body /// shift 1
+namespace ScopeTerm
+  export %inline
+  (.term) : ScopeTerm q d n -> Term q d (S n)
+  (TUsed   body).term = body
+  (TUnused body).term = body //. shift 1
 
-export
-fromScopeTerm : ScopeTerm q d n -> Term q d (S n)
-fromScopeTerm (TUsed   body) = body
-fromScopeTerm (TUnused body) = body //. shift 1
+namespace DScopeTerm
+  export %inline
+  (.term) : DScopeTerm q d n -> Term q (S d) n
+  (DUsed   body).term = body
+  (DUnused body).term = body /// shift 1
+
+export %inline
+sub1 : ScopeTerm q d n -> Elim q d n -> Term q d n
+sub1 (TUsed   body) e = body // one e
+sub1 (TUnused body) e = body
+
+export %inline
+dsub1 : DScopeTerm q d n -> Dim d -> Term q d n
+dsub1 (DUsed   body) p = body /// one p
+dsub1 (DUnused body) p = body
+
+public export %inline
+(.zero) : DScopeTerm q d n -> Term q d n
+body.zero = dsub1 body $ K Zero
+
+public export %inline
+(.one) : DScopeTerm q d n -> Term q d n
+body.one = dsub1 body $ K One
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index 107cbf5..cedb87c 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -282,11 +282,3 @@ decEqFromBool i j =
 %transform "Var.decEq" varDecEq = decEqFromBool
 
 public export %inline DecEq (Var n) where decEq = varDecEq
-
--- export
--- Tighten Var where
---   tighten Id       i      = pure i
---   tighten (Drop q) VZ     = empty
---   tighten (Drop q) (VS i) = tighten q i
---   tighten (Keep q) VZ     = pure VZ
---   tighten (Keep q) (VS i) = VS <$> tighten q i
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index fd17293..87473fb 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -9,6 +9,15 @@ import Decidable.Decidable
 %default total
 
 
+public export
+0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
+CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m)
+
+public export
+0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type
+CanTC q = CanTC' q IsGlobal
+
+
 private covering %inline
 expectTYPE : HasErr q m => Term q d n -> m Universe
 expectTYPE s =
@@ -20,9 +29,17 @@ private covering %inline
 expectPi : HasErr q m => Term q d n ->
            m (q, Term q d n, ScopeTerm q d n)
 expectPi ty =
-  case (whnfT ty).fst of
-       Pi qty _ arg res => pure (qty, arg, res)
-       _                => throwError $ ExpectedPi ty
+  case whnfT ty of
+    Element (Pi qty _ arg res) _ => pure (qty, arg, res)
+    _ => throwError $ ExpectedPi ty
+
+private covering %inline
+expectEq : HasErr q m => Term q d n ->
+           m (DScopeTerm q d n, Term q d n, Term q d n)
+expectEq ty =
+  case whnfT ty of
+    Element (Eq _ ty l r) _ => pure (ty, l, r)
+    _ => throwError $ ExpectedEq ty
 
 private %inline
 expectEqualQ : HasErr q m => Eq q =>
@@ -52,6 +69,12 @@ lookupBound pi VZ ctx@(MkTyContext {tctx = _ :< ty, _}) =
 lookupBound pi (VS i) ctx =
   weakI $ lookupBound pi i (tail ctx)
 
+private
+lookupFree : IsQty q => CanTC q m => Name -> m (Definition q)
+lookupFree x =
+  case lookup x !ask of
+    Just d  => pure d
+    Nothing => throwError $ NotInScope x
 
 private %inline
 subjMult : IsQty q => (sg : SQty q) -> q -> SQty q
@@ -65,14 +88,6 @@ makeDimEq (DBind dctx)   = makeDimEq dctx :<? Nothing
 makeDimEq (DEq p q dctx) = set p q $ makeDimEq dctx
 
 
-public export
-0 CanTC' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
-CanTC' q isGlobal m = (HasErr q m, MonadReader (Definitions' q isGlobal) m)
-
-public export
-0 CanTC : (q : Type) -> IsQty q => (Type -> Type) -> Type
-CanTC q = CanTC' q IsGlobal
-
 parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  mutual
   -- [todo] it seems like the options here for dealing with substitutions are
@@ -80,76 +95,102 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   -- substitutions. both of them seem like the same amount of work for the
   -- computer but pushing is less work for the me
 
+  ||| `check ctx sg subj ty` checks that in the context `ctx`, the term
+  ||| `subj` has the type `ty`, with quantity `sg`. if so, returns the
+  ||| quantities of all bound variables that it used.
   export covering %inline
-  check : (ctx : TyContext q d n) -> (sg : SQty q) ->
-          (subj : Term q d n) -> (ty : Term q d n) ->
+  check : TyContext q d n -> SQty q -> Term q d n -> Term q d n ->
           m (CheckResult q n)
-  check ctx sg subj ty = check' ctx sg (pushSubstsT subj) ty
+  check ctx sg subj ty =
+    let Element subj nc = pushSubstsT subj in
+    check' ctx sg subj nc ty
 
+  ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`,
+  ||| and returns its type and the bound variables it used.
   export covering %inline
-  infer : (ctx : TyContext q d n) -> (sg : SQty q) ->
-          (subj : Elim q d n) ->
-          m (InferResult q d n)
-  infer ctx sg subj = infer' ctx sg (pushSubstsE subj)
+  infer : TyContext q d n -> SQty q -> Elim q d n -> m (InferResult q d n)
+  infer ctx sg subj =
+    let Element subj nc = pushSubstsE subj in
+    infer' ctx sg subj nc
 
 
   export covering
-  check' : (ctx : TyContext q d n) -> (sg : SQty q) ->
-           (subj : NotCloTerm q d n) -> (ty : Term q d n) ->
+  check' : TyContext q d n -> SQty q ->
+           (subj : Term q d n) -> (0 nc : NotCloT subj) -> Term q d n ->
            m (CheckResult q n)
 
-  check' ctx sg (Element (TYPE l) _) ty = do
+  check' ctx sg (TYPE l) _ ty = do
     l' <- expectTYPE ty
     expectEqualQ zero sg.fst
     unless (l < l') $ throwError $ BadUniverse l l'
     pure $ zeroFor ctx
 
-  check' ctx sg (Element (Pi qty x arg res) _) ty = do
+  check' ctx sg (Pi qty x arg res) _ ty = do
     l <- expectTYPE ty
     expectEqualQ zero sg.fst
     ignore $ check ctx szero arg (TYPE l)
     case res of
-         TUsed   res =>
-           ignore $ check (extendTy arg zero ctx) szero res (TYPE l)
-         TUnused res =>
-           ignore $ check ctx szero res (TYPE l)
+      TUsed   res => ignore $ check (extendTy arg zero ctx) szero res (TYPE l)
+      TUnused res => ignore $ check ctx szero res (TYPE l)
     pure $ zeroFor ctx
 
-  check' ctx sg (Element (Lam x body) _) ty = do
+  check' ctx sg (Lam x body) _ ty = do
     (qty, arg, res) <- expectPi ty
-    -- [todo] do this properly?
-    let body = fromScopeTerm body; res = fromScopeTerm res
-    qout <- check (extendTy arg (sg.fst * qty) ctx) sg body res
+    qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term
     popQ qty qout
 
-  check' ctx sg (Element (E e) _) ty = do
+  check' ctx sg (Eq i t l r) _ ty = do
+    u <- expectTYPE ty
+    expectEqualQ zero sg.fst
+    case t of
+      DUsed   t => ignore $ check (extendDim ctx) sg t (TYPE u)
+      DUnused t => ignore $ check ctx sg t (TYPE u)
+    ignore $ check ctx sg t.zero l
+    ignore $ check ctx sg t.one  r
+    pure $ zeroFor ctx
+
+  check' ctx sg (DLam i body) _ ty = do
+    (ty, l, r) <- expectEq ty
+    qout <- check (extendDim ctx) sg body.term ty.term
+    let eqs = makeDimEq ctx.dctx
+    equalTWith eqs body.zero l
+    equalTWith eqs body.one  r
+    pure qout
+
+  check' ctx sg (E e) _ ty = do
     infres <- infer ctx sg e
     ignore $ check ctx szero ty (TYPE UAny)
     subTWith (makeDimEq ctx.dctx) infres.type ty
     pure infres.qout
 
   export covering
-  infer' : (ctx : TyContext q d n) -> (sg : SQty q) ->
-           (subj : NotCloElim q d n) ->
+  infer' : TyContext q d n -> SQty q ->
+           (subj : Elim q d n) -> (0 nc : NotCloE subj) ->
            m (InferResult q d n)
 
-  infer' ctx sg (Element (F x) _) = do
-    Just g <- asks $ lookup x  | Nothing => throwError $ NotInScope x
-    when (isZero g) $ expectEqualQ sg.fst zero
+  infer' ctx sg (F x) _ = do
+    g <- lookupFree x
+    when (isYes $ isZero g) $ expectEqualQ sg.fst zero
     pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
 
-  infer' ctx sg (Element (B i) _) =
+  infer' ctx sg (B i) _ =
     pure $ lookupBound sg.fst i ctx
 
-  infer' ctx sg (Element (fun :@ arg) _) = do
+  infer' ctx sg (fun :@ arg) _ = do
     funres <- infer ctx sg fun
     (qty, argty, res) <- expectPi funres.type
-    let sg' = subjMult sg qty
-    argout <- check ctx sg' arg argty
-    pure $ InfRes {type = fromScopeTerm res //. ((arg :# argty) ::: id),
-                   qout = funres.qout + argout}
+    argout <- check ctx (subjMult sg qty) arg argty
+    pure $ InfRes {
+      type = sub1 res $ arg :# argty,
+      qout = funres.qout + argout
+    }
 
-  infer' ctx sg (Element (tm :# ty) _) = do
-    ignore $ check ctx szero ty (TYPE UAny)
-    qout <- check ctx sg tm ty
-    pure $ InfRes {type = ty, qout}
+  infer' ctx sg (fun :% dim) _ = do
+    InfRes {type, qout} <- infer ctx sg fun
+    (ty, _, _) <- expectEq type
+    pure $ InfRes {type = dsub1 ty dim, qout}
+
+  infer' ctx sg (term :# type) _ = do
+    ignore $ check ctx szero type (TYPE UAny)
+    qout <- check ctx sg term type
+    pure $ InfRes {type, qout}
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index d3f3450..efd5894 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -106,11 +106,13 @@ public export
 data Error q
 = ExpectedTYPE (Term q d n)
 | ExpectedPi   (Term q d n)
+| ExpectedEq   (Term q d n)
 | BadUniverse  Universe Universe
 
 | ClashT EqMode (Term q d n) (Term q d n)
 | ClashU EqMode Universe     Universe
 | ClashQ        q            q
+| ClashD        (Dim d)      (Dim d)
 | NotInScope    Name
 
 public export
diff --git a/tests/TermImpls.idr b/tests/TermImpls.idr
index ca3caf6..dfa9659 100644
--- a/tests/TermImpls.idr
+++ b/tests/TermImpls.idr
@@ -33,6 +33,13 @@ mutual
     Lam _ body1 == Lam _ body2 = body1 == body2
     Lam {} == _ = False
 
+    Eq _ ty1 l1 r1 == Eq _ ty2 l2 r2 =
+      ty1 == ty2 && l1 == l2 && r1 == r2
+    Eq {} == _ = False
+
+    DLam _ body1 == DLam _ body2 = body1 == body2
+    DLam {} == _ = False
+
     E e == E f = e == f
     E _ == _ = False
 
@@ -62,6 +69,9 @@ mutual
     (tm1 :# ty1) == (tm2 :# ty2) = tm1 == tm2 && ty1 == ty2
     (_ :# _) == _ = False
 
+    (fun1 :% dim1) == (fun2 :% dim2) = fun1 == fun2 && dim1 == dim2
+    (_ :% _) == _ = False
+
     CloE el1 th1 == CloE el2 th2 =
       case eqSubst th1 th2 of
            Just Refl => el1 == el2 && th1 == th2
@@ -81,6 +91,13 @@ mutual
     TUsed   _ == TUnused _ = False
     TUnused _ == TUsed   _ = False
 
+  export covering
+  Eq q => Eq (DScopeTerm q d n) where
+    DUsed   s == DUsed   t = s == t
+    DUnused s == DUnused t = s == t
+    DUsed   _ == DUnused _ = False
+    DUnused _ == DUsed   _ = False
+
 export covering
 PrettyHL q => Show (Term q d n) where
   showPrec d t = showParens (d /= Open) $ prettyStr True t
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 0b80cbc..f933f33 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -16,6 +16,9 @@ ToInfo (Error Three) where
   toInfo (ExpectedPi t) =
     [("type", "ExpectedPi"),
      ("got", prettyStr True t)]
+  toInfo (ExpectedEq t) =
+    [("type", "ExpectedEq"),
+     ("got", prettyStr True t)]
   toInfo (BadUniverse k l) =
     [("type", "BadUniverse"),
      ("low",  show k),
@@ -34,6 +37,10 @@ ToInfo (Error Three) where
     [("type", "ClashQ"),
      ("left",  prettyStr True pi),
      ("right", prettyStr True rh)]
+  toInfo (ClashD p q) =
+    [("type", "ClashD"),
+     ("left",  prettyStr True p),
+     ("right", prettyStr True q)]
 
 
 0 M : Type -> Type
@@ -127,6 +134,16 @@ tests = "equality & subtyping" :- [
         subT tm1 tm2
     ],
 
+    "eq type" :- [
+      testEq "(★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : ★₁)" $
+        let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in
+        equalT tm tm,
+      testEq "A ≔ ★₁ ⊢ (★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : A)"
+          {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $
+        equalT (Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
+               (Eq0 (FT "A") (TYPE 0) (TYPE 0))
+    ],
+
     "lambda" :- [
       testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $
         equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0),