From 756fc6003051206781baaac457214c601cd952a0 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 12 Jul 2023 22:56:35 +0200
Subject: [PATCH] wip

---
 lib/Quox/Context.idr            |  37 +-
 lib/Quox/FinExtra.idr           |  44 ++
 lib/Quox/Syntax/Dim.idr         | 116 ++---
 lib/Quox/Syntax/DimEq.idr       | 225 ++++-----
 lib/Quox/Syntax/Shift.idr       |  14 +
 lib/Quox/Syntax/Subst.idr       | 233 +++++-----
 lib/Quox/Syntax/Term/Base.idr   |  12 +-
 lib/Quox/Syntax/Term/Pretty.idr |   4 +-
 lib/Quox/Syntax/Term/Subst.idr  | 796 ++++++++++++++++++--------------
 lib/Quox/Syntax/Var.idr         |   9 -
 lib/Quox/Thin/Base.idr          |   2 +-
 lib/Quox/Thin/Comp.idr          |   6 +-
 lib/Quox/Thin/Term.idr          |  43 +-
 lib/Quox/Thin/View.idr          |  21 +-
 14 files changed, 890 insertions(+), 672 deletions(-)
 create mode 100644 lib/Quox/FinExtra.idr

diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index b1a9376..a376042 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -6,12 +6,16 @@ import Quox.Name
 
 import Data.DPair
 import Data.Nat
+import Data.Fin
+import Data.Singleton
 import Data.SnocList
 import Data.SnocVect
 import Data.Vect
 import Control.Monad.Identity
+import Derive.Prelude
 
 %default total
+%language ElabReflection
 
 
 ||| a sequence of bindings under an existing context. each successive element
@@ -83,6 +87,13 @@ export %inline
 toSnocList' : Telescope' a _ _ -> SnocList a
 toSnocList' = toSnocListWith id
 
+export %inline
+toSnocListRelevant : {n1 : Nat} -> Telescope tm n1 n2 -> SnocList (n ** tm n)
+toSnocListRelevant tel = toSnocList' $ snd $ go tel where
+  go : Telescope tm n1 n2' -> (Singleton n2', Telescope' (n ** tm n) n1 n2')
+  go [<]        = (Val n1, [<])
+  go (tel :< x) = let (Val n, tel) = go tel in (Val (S n), tel :< (n ** x))
+
 export %inline
 toList : Telescope tm _ _ -> List (Exists tm)
 toList = toListWith (Evidence _)
@@ -136,34 +147,34 @@ tel ++ (sx :< x) = (tel ++ sx) :< x
 
 public export
 getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
-               Shift len out -> Context tm len -> Var len -> tm out
-getShiftWith shft by (ctx :< t) VZ     = t `shft` ssDown by
-getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (ssDown by) ctx i
+               Shift len out -> Context tm len -> Fin len -> tm out
+getShiftWith shft by (ctx :< t) FZ     = t `shft` ssDown by
+getShiftWith shft by (ctx :< t) (FS i) = getShiftWith shft (ssDown by) ctx i
 
 public export %inline
-getShift : CanShift tm => Shift len out -> Context tm len -> Var len -> tm out
+getShift : CanShift tm => Shift len out -> Context tm len -> Fin len -> tm out
 getShift = getShiftWith (//)
 
 public export %inline
 getWith : (forall from, to. tm from -> Shift from to -> tm to) ->
-          Context tm len -> Var len -> tm len
+          Context tm len -> Fin len -> tm len
 getWith shft = getShiftWith shft SZ
 
 infixl 8 !!
 public export %inline
-(!!) : CanShift tm => Context tm len -> Var len -> tm len
+(!!) : CanShift tm => Context tm len -> Fin len -> tm len
 (!!) = getWith (//)
 
 infixl 8 !!!
 public export %inline
-(!!!) : Context' tm len -> Var len -> tm
+(!!!) : Context' tm len -> Fin len -> tm
 (!!!) = getWith const
 
 public export
 find : Alternative f =>
-       (forall n. tm n -> Bool) -> Context tm len -> f (Var len)
+       (forall n. tm n -> Bool) -> Context tm len -> f (Fin len)
 find p [<]        = empty
-find p (ctx :< x) = (guard (p x) $> VZ) <|> (VS <$> find p ctx)
+find p (ctx :< x) = (guard (p x) $> FZ) <|> (FS <$> find p ctx)
 
 
 export
@@ -320,6 +331,14 @@ export %inline
     where Show (Exists tm) where showPrec d t = showPrec d t.snd
 
 
+export
+implementation [ShowTelRelevant]
+  {n1 : Nat} -> ({n : Nat} -> Show (f n)) => Show (Telescope f n1 n2)
+where
+  showPrec d = showPrec d . toSnocListRelevant
+    where Show (n : Nat ** f n) where showPrec d (_ ** t) = showPrec d t
+
+
 parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
            (nameHL : HL)
            (pterm : forall n. BContext n -> tm n -> Eff Pretty (Doc opts))
diff --git a/lib/Quox/FinExtra.idr b/lib/Quox/FinExtra.idr
new file mode 100644
index 0000000..fffc8e3
--- /dev/null
+++ b/lib/Quox/FinExtra.idr
@@ -0,0 +1,44 @@
+module Quox.FinExtra
+
+import public Data.Fin
+import Quox.Decidable
+
+public export
+data LT : Rel (Fin n) where
+  LTZ : FZ `LT` FS i
+  LTS : i `LT` j -> FS i `LT` FS j
+%builtin Natural FinExtra.LT
+%name FinExtra.LT lt
+
+public export %inline
+GT : Rel (Fin n)
+GT = flip LT
+
+export
+Transitive (Fin n) LT where
+  transitive LTZ     (LTS _) = LTZ
+  transitive (LTS p) (LTS q) = LTS $ transitive p q
+
+export Uninhabited (i `FinExtra.LT` i) where uninhabited (LTS p) = uninhabited p
+export Uninhabited (FS i `LT` FZ) where uninhabited _ impossible
+
+
+public export
+data Compare : Rel (Fin n) where
+  IsLT : (lt : i `LT` j) -> Compare i j
+  IsEQ :                    Compare i i
+  IsGT : (gt : i `GT` j) -> Compare i j
+%name Compare cmp
+
+export
+compareS : Compare i j -> Compare (FS i) (FS j)
+compareS (IsLT lt) = IsLT (LTS lt)
+compareS IsEQ      = IsEQ
+compareS (IsGT gt) = IsGT (LTS gt)
+
+export
+compareP : (i, j : Fin n) -> Compare i j
+compareP FZ     FZ     = IsEQ
+compareP FZ     (FS j) = IsLT LTZ
+compareP (FS i) FZ     = IsGT LTZ
+compareP (FS i) (FS j) = compareS $ compareP i j
diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index 363e082..2f6666c 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -1,15 +1,18 @@
 module Quox.Syntax.Dim
 
-import Quox.Loc
-import Quox.Name
+import Quox.Thin
 import Quox.Syntax.Var
 import Quox.Syntax.Subst
 import Quox.Pretty
+import Quox.Name
+import Quox.Loc
 import Quox.Context
 
 import Decidable.Equality
 import Control.Function
 import Derive.Prelude
+import Data.DPair
+import Data.SnocVect
 
 %default total
 %language ElabReflection
@@ -39,38 +42,48 @@ DecEq DimConst where
 
 public export
 data Dim : Nat -> Type where
-  K : DimConst -> Loc -> Dim d
-  B : Var d -> Loc -> Dim d
+  K : DimConst -> Loc -> Dim 0
+  B : Loc -> Dim 1
 %name Dim.Dim p, q
 %runElab deriveIndexed "Dim" [Eq, Ord, Show]
 
 
+public export
+DimT : Nat -> Type
+DimT = Thinned Dim
+
+public export %inline
+KT : DimConst -> Loc -> DimT d
+KT e loc = Th zero $ K e loc
+
+
 ||| `endsOr l r x p` returns `ends l r ε` if `p` is a constant ε, and
 ||| `x` otherwise.
 public export
 endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
 endsOr l r x (K e _) = ends l r e
-endsOr l r x (B _ _) = x
+endsOr l r x (B _)   = x
 
 
 export
 Located (Dim d) where
   (K _ loc).loc = loc
-  (B _ loc).loc = loc
+  (B loc).loc   = loc
 
 export
 Relocatable (Dim d) where
   setLoc loc (K e _) = K e loc
-  setLoc loc (B i _) = B i loc
+  setLoc loc (B _)   = B loc
 
-export
-prettyDimConst : {opts : _} -> DimConst -> Eff Pretty (Doc opts)
-prettyDimConst = hl Dim . text . ends "0" "1"
+parameters {opts : LayoutOpts}
+  export
+  prettyDimConst : DimConst -> Eff Pretty (Doc opts)
+  prettyDimConst = hl Dim . text . ends "0" "1"
 
-export
-prettyDim : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts)
-prettyDim names (K e _) = prettyDimConst e
-prettyDim names (B i _) = prettyDBind $ names !!! i
+  export
+  prettyDim : {d : Nat} -> BContext d -> DimT d -> Eff Pretty (Doc opts)
+  prettyDim names (Th _ (K e _)) = prettyDimConst e
+  prettyDim names (Th i (B _)) = prettyDBind $ names !!! i.fin
 
 
 public export %inline
@@ -83,57 +96,54 @@ DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim
 
 
-public export FromVar Dim where fromVarLoc = B
+-- public export FromVar Dim where fromVarLoc = B
 
 
-export
-CanShift Dim where
-  K e loc // _  = K e loc
-  B i loc // by = B (i // by) loc
+-- export
+-- CanShift Dim where
+--   K e loc // _  = K e loc
+--   B i loc // by = B (i // by) loc
 
-export
+export %inline FromVar Dim where var = B
+
+export %inline
 CanSubstSelf Dim where
-  K e loc // _  = K e loc
-  B i loc // th = getLoc th i loc
+  Th _ (K e loc) // _  = KT e loc
+  Th i (B loc)   // th = get th i.fin
 
 
-export Uninhabited (B i loc1 = K e loc2) where uninhabited _ impossible
-export Uninhabited (K e loc1 = B i loc2) where uninhabited _ impossible
+export Uninhabited (B loc1   = K e loc2) where uninhabited _ impossible
+export Uninhabited (K e loc1 = B loc2)   where uninhabited _ impossible
 
-public export
-data Eqv : Dim d1 -> Dim d2 -> Type where
-  EK : K e _ `Eqv` K e _
-  EB : i `Eqv` j -> B i _ `Eqv` B j _
+-- public export
+-- data Eqv : Dim d1 -> Dim d2 -> Type where
+--   EK : K e _ `Eqv` K e _
+--   EB : i `Eqv` j -> B i _ `Eqv` B j _
 
-export Uninhabited (K e l1 `Eqv` B i l2) where uninhabited _ impossible
-export Uninhabited (B i l1 `Eqv` K e l2) where uninhabited _ impossible
+-- export Uninhabited (K e l1 `Eqv` B i l2) where uninhabited _ impossible
+-- export Uninhabited (B i l1 `Eqv` K e l2) where uninhabited _ impossible
 
-export
-injectiveB : B i loc1 `Eqv` B j loc2 -> i `Eqv` j
-injectiveB (EB e) = e
+-- export
+-- injectiveB : B i loc1 `Eqv` B j loc2 -> i `Eqv` j
+-- injectiveB (EB e) = e
 
-export
-injectiveK : K e loc1 `Eqv` K f loc2 -> e = f
-injectiveK EK = Refl
+-- export
+-- injectiveK : K e loc1 `Eqv` K f loc2 -> e = f
+-- injectiveK EK = Refl
 
-public export
-decEqv : Dec2 Dim.Eqv
-decEqv (K e _) (K f _) = case decEq e f of
-  Yes Refl => Yes EK
-  No  n    => No $ n . injectiveK
-decEqv (B i _) (B j _) = case decEqv i j of
-  Yes y => Yes $ EB y
-  No  n => No  $ \(EB y) => n y
-decEqv (B _ _) (K _ _) = No absurd
-decEqv (K _ _) (B _ _) = No absurd
+-- public export
+-- decEqv : Dec2 Dim.Eqv
+-- decEqv (K e _) (K f _) = case decEq e f of
+--   Yes Refl => Yes EK
+--   No  n    => No $ n . injectiveK
+-- decEqv (B i _) (B j _) = case decEqv i j of
+--   Yes y => Yes $ EB y
+--   No  n => No  $ \(EB y) => n y
+-- decEqv (B _ _) (K _ _) = No absurd
+-- decEqv (K _ _) (B _ _) = No absurd
 
 ||| 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) => (loc : Loc) -> Dim d
-BV i loc = B (V i) loc
-
-
-export
-weakD : (by : Nat) -> Dim d -> Dim (by + d)
-weakD by p = p // shift by
+BV : (i : Fin d) -> (loc : Loc) -> DimT d
+BV i loc = Th (one' i) $ B loc
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index c8079d8..aeb7a2b 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -6,11 +6,14 @@ import public Quox.Syntax.Subst
 import public Quox.Context
 import Quox.Pretty
 import Quox.Name
+import Quox.Thin
+import Quox.FinExtra
 
 import Data.Maybe
 import Data.Nat
 import Data.DPair
 import Data.Fun.Graph
+import Data.SnocVect
 import Decidable.Decidable
 import Decidable.Equality
 import Derive.Prelude
@@ -21,7 +24,7 @@ import Derive.Prelude
 
 public export
 DimEq' : Nat -> Type
-DimEq' = Context (Maybe . Dim)
+DimEq' = Context (Maybe . DimT)
 
 
 public export
@@ -29,7 +32,12 @@ data DimEq : Nat -> Type where
   ZeroIsOne : DimEq d
   C         : (eqs : DimEq' d) -> DimEq d
 %name DimEq eqs
-%runElab deriveIndexed "DimEq" [Eq, Ord, Show]
+%runElab deriveIndexed "DimEq" [Eq]
+
+export
+Show (DimEq d) where
+  showPrec d ZeroIsOne = "ZeroIsOne"
+  showPrec d (C eq')   = showCon d "C" $ showArg eq' @{ShowTelRelevant}
 
 
 public export
@@ -72,7 +80,7 @@ toMaybe (Just x) = Just x
 export
 fromGround' : Context' DimConst d -> DimEq' d
 fromGround' [<]        = [<]
-fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc)
+fromGround' (ctx :< e) = fromGround' ctx :< Just (KT e noLoc)
 
 export
 fromGround : Context' DimConst d -> DimEq d
@@ -94,39 +102,40 @@ new = C new'
 
 
 public export %inline
-get' : DimEq' d -> Var d -> Maybe (Dim d)
+get' : DimEq' d -> Fin d -> Maybe (DimT d)
 get' = getWith $ \p, by => map (// by) p
 
 public export %inline
-getVar : DimEq' d -> Var d -> Loc -> Dim d
-getVar eqs i loc = fromMaybe (B i loc) $ get' eqs i
-
-public export %inline
-getShift' : Shift len out -> DimEq' len -> Var len -> Maybe (Dim out)
+getShift' : Shift len out -> DimEq' len -> Fin len -> Maybe (DimT out)
 getShift' = getShiftWith $ \p, by => map (// by) p
 
 public export %inline
-get : DimEq' d -> Dim d -> Dim d
-get _   (K e loc) = K e loc
-get eqs (B i loc) = getVar eqs i loc
+get : {d : Nat} -> DimEq' d -> DimT d -> DimT d
+get eqs p@(Th _ (K {})) = p
+get eqs p@(Th i (B _))  = fromMaybe p $ get' eqs i.fin
 
 
 public export %inline
-equal : DimEq d -> (p, q : Dim d) -> Bool
+equal : {d : Nat} -> DimEq d -> (p, q : DimT d) -> Bool
 equal ZeroIsOne p q = True
 equal (C eqs)   p q = get eqs p == get eqs q
 
 
 infixl 7 :<?
 export %inline
-(:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d)
+(:<?) : {d : Nat} -> DimEq d -> Maybe (DimT d) -> DimEq (S d)
 ZeroIsOne :<? d = ZeroIsOne
 C eqs     :<? d = C $ eqs :< map (get eqs) d
 
 
 private %inline
-ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d)
-ifVar i p = map $ \q => if q == B i noLoc then p else q
+isVar : {d : Nat} -> Fin d -> DimT d -> Bool
+isVar i (Th j (B _))  = i == j.fin
+isVar i (Th _ (K {})) = False
+
+private %inline
+ifVar : {d : Nat} -> Fin d -> DimT d -> Maybe (DimT d) -> Maybe (DimT d)
+ifVar i p = map $ \q => if isVar i q then p else q
 
 -- (using decEq instead of (==) because of the proofs below)
 private %inline
@@ -135,43 +144,45 @@ checkConst e f eqs = if isYes $ e `decEq` f then C eqs else ZeroIsOne
 
 
 export
-setConst : Var d -> DimConst -> Loc -> DimEq' d -> DimEq d
-setConst VZ e loc (eqs :< Nothing) =
-  C $ eqs :< Just (K e loc)
-setConst VZ e _ (eqs :< Just (K f loc)) =
-  checkConst e f $ eqs :< Just (K f loc)
-setConst VZ e loc (eqs :< Just (B i _)) =
-  setConst i e loc eqs :<? Just (K e loc)
-setConst (VS i) e loc (eqs :< p) =
-  setConst i e loc eqs :<? ifVar i (K e loc) p
+setConst : {d : Nat} -> Fin d -> DimConst -> Loc -> DimEq' d -> DimEq d
+setConst FZ e loc (eqs :< Nothing) =
+  C $ eqs :< Just (KT e loc)
+setConst FZ e _ (eqs :< Just (Th _ (K f loc))) =
+  checkConst e f $ eqs :< Just (KT f loc)
+setConst FZ e loc (eqs :< Just (Th j (B _))) =
+  setConst j.fin e loc eqs :<? Just (KT e loc)
+setConst (FS i) e loc (eqs :< p) =
+  setConst i e loc eqs :<? ifVar i (KT e loc) p
 
 mutual
   private
-  setVar' : (i, j : Var d) -> (0 _ : i `LT` j) -> Loc -> DimEq' d -> DimEq d
-  setVar' VZ (VS i) LTZ loc (eqs :< Nothing) =
-    C eqs :<? Just (B i loc)
-  setVar' VZ (VS i) LTZ loc (eqs :< Just (K e eloc)) =
-    setConst i e loc eqs :<? Just (K e eloc)
-  setVar' VZ (VS i) LTZ loc (eqs :< Just (B j jloc)) =
-    setVar i j loc jloc eqs :<? Just (if j > i then B j jloc else B i loc)
-  setVar' (VS i) (VS j) (LTS lt) loc (eqs :< p) =
-    setVar' i j lt loc eqs :<? ifVar i (B j loc) p
+  setVar' : {d : Nat} ->
+            (i, j : Fin d) -> (0 _ : i `LT` j) -> Loc -> DimEq' d -> DimEq d
+  setVar' FZ (FS i) LTZ loc (eqs :< Nothing) =
+    C eqs :<? Just (BV i loc)
+  setVar' FZ (FS i) LTZ loc (eqs :< Just (Th _ (K e eloc))) =
+    setConst i e loc eqs :<? Just (KT e eloc)
+  setVar' FZ (FS i) LTZ loc (eqs :< Just (Th j (B jloc))) =
+    let j = j.fin in
+    setVar i j loc jloc eqs :<? Just (if j > i then BV j jloc else BV i loc)
+  setVar' (FS i) (FS j) (LTS lt) loc (eqs :< p) =
+    setVar' i j lt loc eqs :<? ifVar i (BV j loc) p
 
   export %inline
-  setVar : (i, j : Var d) -> Loc -> Loc -> DimEq' d -> DimEq d
-  setVar i j li lj eqs with (compareP i j) | (compare i.nat j.nat)
-    setVar i j li lj eqs | IsLT lt | LT = setVar' i j lt lj eqs
-    setVar i i li lj eqs | IsEQ    | EQ = C eqs
-    setVar i j li lj eqs | IsGT gt | GT = setVar' j i gt li eqs
+  setVar : {d : Nat} -> (i, j : Fin d) -> Loc -> Loc -> DimEq' d -> DimEq d
+  setVar i j li lj eqs with (compareP i j)
+    setVar i j li lj eqs | IsLT lt = setVar' i j lt lj eqs
+    setVar i i li lj eqs | IsEQ    = C eqs
+    setVar i j li lj eqs | IsGT gt = setVar' j i gt li eqs
 
 
 export %inline
-set : (p, q : Dim d) -> DimEq d -> DimEq d
+set : {d : Nat} -> (p, q : DimT d) -> DimEq d -> DimEq d
 set _ _ ZeroIsOne = ZeroIsOne
-set (K e eloc) (K f floc) (C eqs) = checkConst e f eqs
-set (K e eloc) (B i iloc) (C eqs) = setConst i e eloc eqs
-set (B i iloc) (K e eloc) (C eqs) = setConst i e eloc eqs
-set (B i iloc) (B j jloc) (C eqs) = setVar   i j iloc jloc eqs
+set (Th _ (K e _))  (Th _ (K f _))  (C eqs) = checkConst e f eqs
+set (Th _ (K e el)) (Th j (B _))    (C eqs) = setConst j.fin e el eqs
+set (Th i (B _))    (Th _ (K e el)) (C eqs) = setConst i.fin e el eqs
+set (Th i (B il))   (Th j (B jl))   (C eqs) = setVar i.fin j.fin il jl eqs
 
 
 public export %inline
@@ -179,97 +190,99 @@ Split : Nat -> Type
 Split d = (DimEq' d, DSubst (S d) d)
 
 export %inline
-split1 : DimConst -> Loc -> DimEq' (S d) -> Maybe (Split d)
-split1 e loc eqs = case setConst VZ e loc eqs of
+split1 : {d : Nat} -> DimConst -> Loc -> DimEq' (S d) -> Maybe (Split d)
+split1 e loc eqs = case setConst 0 e loc eqs of
   ZeroIsOne    => Nothing
-  C (eqs :< _) => Just (eqs, K e loc ::: id)
+  C (eqs :< _) => Just (eqs, id (B loc) :< KT e loc)
 
 export %inline
-split : Loc -> DimEq' (S d) -> List (Split d)
+split : {d : Nat} -> Loc -> DimEq' (S d) -> List (Split d)
 split loc eqs = toList (split1 Zero loc eqs) <+> toList (split1 One loc eqs)
 
 export
-splits' : Loc -> DimEq' d -> List (DSubst d 0)
-splits' _   [<]          = [id]
+splits' : {d : Nat} -> Loc -> DimEq' d -> List (DSubst d 0)
+splits' _   [<]          = [[<]]
 splits' loc eqs@(_ :< _) =
   [th . ph | (eqs', th) <- split loc eqs, ph <- splits' loc eqs']
 
 ||| the Loc is put into each of the DimConsts
 export %inline
-splits : Loc -> DimEq d -> List (DSubst d 0)
+splits : {d : Nat} -> Loc -> DimEq d -> List (DSubst d 0)
 splits _   ZeroIsOne = []
 splits loc (C eqs)   = splits' loc eqs
 
 
-private
-0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') ->
-                getShift' by (new' {d}) i = Nothing
-newGetShift (S d) VZ     by = Refl
-newGetShift (S d) (VS i) by = newGetShift d i (ssDown by)
+-- private
+-- 0 newGetShift : (d : Nat) -> (i : Fin d) -> (by : Shift d d') ->
+--                 getShift' by (new' {d}) i = Nothing
+-- newGetShift (S d) FZ     by = Refl
+-- newGetShift (S d) (FS i) by = newGetShift d i (ssDown by)
 
-export
-0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing
-newGet' d i = newGetShift d i SZ
+-- export
+-- 0 newGet' : (d : Nat) -> (i : Fin d) -> get' (new' {d}) i = Nothing
+-- newGet' d i = newGetShift d i SZ
 
-export
-0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
-newGet d (K e _) = Refl
-newGet d (B i _) = rewrite newGet' d i in Refl
+-- export
+-- 0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
+-- newGet d (K e _) = Refl
+-- newGet d (B i _) = rewrite newGet' d i in Refl
 
 
-export
-0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
-setSelf p ZeroIsOne = Refl
-setSelf (K Zero _) (C eqs) = Refl
-setSelf (K One _)  (C eqs) = Refl
-setSelf (B i _)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
-  _ | IsLT lt | LT = absurd lt
-  _ | IsEQ    | EQ = Refl
-  _ | IsGT gt | GT = absurd gt
+-- export
+-- 0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
+-- setSelf p ZeroIsOne = Refl
+-- setSelf (K Zero _) (C eqs) = Refl
+-- setSelf (K One _)  (C eqs) = Refl
+-- setSelf (B i _)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
+--   _ | IsLT lt | LT = absurd lt
+--   _ | IsEQ    | EQ = Refl
+--   _ | IsGT gt | GT = absurd gt
 
 
-private
-prettyDVars : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts))
-prettyDVars = traverse prettyDBind . toSnocList'
+parameters {opts : LayoutOpts}
+  private
+  prettyDVars : {d : Nat} -> BContext d -> Eff Pretty (SnocList (Doc opts))
+  prettyDVars = traverse prettyDBind . toSnocList'
 
-private
-prettyCst : {opts : _} -> BContext d -> Dim d -> Dim d -> Eff Pretty (Doc opts)
-prettyCst dnames p q =
-  hsep <$> sequence [prettyDim dnames p, cstD, prettyDim dnames q]
+  private
+  prettyCst : {d : Nat} -> BContext d -> DimT d -> DimT d -> Eff Pretty (Doc opts)
+  prettyCst dnames p q =
+    hsep <$> sequence [prettyDim dnames p, cstD, prettyDim dnames q]
 
-private
-prettyCsts : {opts : _} -> BContext d -> DimEq' d ->
-             Eff Pretty (SnocList (Doc opts))
-prettyCsts [<] [<] = pure [<]
-prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
-prettyCsts dnames (eqs :< Just q)  =
-  [|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 noLoc) (weakD 1 q)|]
+  private
+  prettyCsts : {d : Nat} -> BContext d -> DimEq' d ->
+               Eff Pretty (SnocList (Doc opts))
+  prettyCsts [<] [<] = pure [<]
+  prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
+  prettyCsts dnames (eqs :< Just q)  =
+    [|prettyCsts (tail dnames) eqs :<
+      prettyCst dnames (BV 0 noLoc) (weak 1 q)|]
 
-export
-prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
-prettyDimEq' dnames eqs = do
-  vars <- prettyDVars dnames
-  eqs  <- prettyCsts dnames eqs
-  let prec = if length vars <= 1 && null eqs then Arg else Outer
-  parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
+  export
+  prettyDimEq' : {d : Nat} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
+  prettyDimEq' dnames eqs = do
+    vars <- prettyDVars dnames
+    eqs  <- prettyCsts dnames eqs
+    let prec = if length vars <= 1 && null eqs then Arg else Outer
+    parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
 
-export
-prettyDimEq : {opts : _} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
-prettyDimEq dnames ZeroIsOne = do
-  vars <- prettyDVars dnames
-  cst  <- prettyCst [<] (K Zero noLoc) (K One noLoc)
-  pure $ separateTight !commaD $ vars :< cst
-prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs
+  export
+  prettyDimEq : {d : Nat} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
+  prettyDimEq dnames ZeroIsOne = do
+    vars <- prettyDVars dnames
+    cst  <- prettyCst [<] (KT Zero noLoc) (KT One noLoc)
+    pure $ separateTight !commaD $ vars :< cst
+  prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs
 
 
 public export
-wf' : DimEq' d -> Bool
-wf' [<]                   = True
-wf' (eqs :< Nothing)      = wf' eqs
-wf' (eqs :< Just (K e _)) = wf' eqs
-wf' (eqs :< Just (B i _)) = isNothing (get' eqs i) && wf' eqs
+wf' : {d : Nat} -> DimEq' d -> Bool
+wf' [<]                         = True
+wf' (eqs :< Nothing)            = wf' eqs
+wf' (eqs :< Just (Th _ (K {}))) = wf' eqs
+wf' (eqs :< Just (Th i (B _)))  = isNothing (get' eqs i.fin) && wf' eqs
 
 public export
-wf : DimEq d -> Bool
+wf : {d : Nat} -> DimEq d -> Bool
 wf ZeroIsOne = True
 wf (C eqs)   = wf' eqs
diff --git a/lib/Quox/Syntax/Shift.idr b/lib/Quox/Syntax/Shift.idr
index ecfe476..c519883 100644
--- a/lib/Quox/Syntax/Shift.idr
+++ b/lib/Quox/Syntax/Shift.idr
@@ -1,9 +1,11 @@
 module Quox.Syntax.Shift
 
 import public Quox.Syntax.Var
+import public Quox.Thin
 
 import Data.Nat
 import Data.So
+import Data.DPair
 
 %default total
 
@@ -220,3 +222,15 @@ namespace CanShift
 
   public export %inline
   [Const] CanShift (\_ => a) where x // _ = x
+
+
+export
+shiftOPE : {mask : Nat} -> (0 ope : OPE m n mask) ->
+           Shift n n' -> Subset Nat (OPE m n')
+shiftOPE ope SZ      = Element _ ope
+shiftOPE ope (SS by) =
+  let Element _ ope = shiftOPE ope by in Element _ $ drop ope
+
+export
+CanShift (Thinned f) where
+  Th ope tm // by = Th (shiftOPE ope by).snd tm
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index a14c232..8137b02 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -1,10 +1,9 @@
 module Quox.Syntax.Subst
 
-import public Quox.Syntax.Shift
-import Quox.Syntax.Var
-import Quox.Name
+import Quox.Thin
+import Quox.Loc
 
-import Data.Nat
+import Data.DPair
 import Data.List
 import Data.SnocVect
 import Derive.Prelude
@@ -14,149 +13,159 @@ import Derive.Prelude
 
 
 public export
-data Subst : (Nat -> Type) -> Nat -> Nat -> Type where
-  Shift : Shift from to -> Subst env from to
-  (:::) : (t : Lazy (env to)) -> Subst env from to -> Subst env (S from) to
-%name Subst th, ph, ps
+Subst : (Nat -> Type) -> Nat -> Nat -> Type
+Subst env from to = SnocVect from (Lazy (Thinned env to))
 
-infixr 7 !:::
-||| in case the automatic laziness insertion gets confused
 public export
-(!:::) : env to -> Subst env from to -> Subst env (S from) to
-t !::: ts = t ::: ts
+Subst2 : (Nat -> Nat -> Type) -> Nat -> Nat -> Nat -> Type
+Subst2 env d from to = SnocVect from (Lazy (Thinned2 env d to))
 
 
-private
-Repr : (Nat -> Type) -> Nat -> Type
-Repr f to = (List (f to), Nat)
-
-private
-repr : Subst f from to -> Repr f to
-repr (Shift by) = ([], by.nat)
-repr (t ::: th) = let (ts, i) = repr th in (t::ts, i)
+public export
+get : Subst env f t -> Fin f -> Thinned env t
+get (sx :< x) FZ     = x
+get (sx :< x) (FS i) = get sx i
 
 
-export Eq   (f to) => Eq   (Subst f from to) where (==) = (==) `on` repr
-export Ord  (f to) => Ord  (Subst f from to) where compare = compare `on` repr
-export Show (f to) => Show (Subst f from to) where show = show . repr
+public export
+interface FromVar (0 term : Nat -> Type) where
+  var : Loc -> term 1
 
+public export
+0 FromVar2 : (Nat -> Nat -> Type) -> Type
+FromVar2 t = FromVar (t 0)
+
+public export
+varT : FromVar term => Fin n -> Loc -> Thinned term n
+varT i loc = Th (one' i) (var loc)
+
+public export
+varT2 : FromVar2 term => Fin n -> Loc -> Thinned2 term d n
+varT2 i loc = Th2 zero (one' i) (var loc)
 
 infixl 8 //
+namespace CanSubstSelf
+  public export
+  interface FromVar term => CanSubstSelf term where
+    (//) : {f : Nat} -> Thinned term f -> Subst term f t -> Thinned term t
+
+namespace CanSubstSelf2
+  public export
+  interface FromVar2 term => CanSubstSelf2 term where
+    (//) : {f : Nat} -> Thinned2 term d f ->
+           Subst2 term d f t -> Thinned2 term d t
+
 public export
-interface FromVar term => CanSubstSelf term where
-  (//) : term from -> Lazy (Subst term from to) -> term to
+(.) : {mid : Nat} -> CanSubstSelf f =>
+      Subst f from mid -> Subst f mid to -> Subst f from to
+th . ph = map (\(Delay x) => x // ph) th
+
+infixr 9 .%
+
+public export
+(.%) : {mid : Nat} -> CanSubstSelf2 f =>
+       Subst2 f d from mid -> Subst2 f d mid to -> Subst2 f d from to
+th .% ph = map (\(Delay x) => x // ph) th
 
 
 public export
-getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to
-getLoc (Shift by) i      loc = fromVarLoc (shift by i) loc
-getLoc (t ::: th) VZ     _   = t
-getLoc (t ::: th) (VS i) loc = getLoc th i loc
-
+tabulate : (n : Nat) -> SnocVect n (Fin n)
+tabulate n = go n id where
+  go : (n : Nat) -> (Fin n -> Fin n') -> SnocVect n (Fin n')
+  go 0     f = [<]
+  go (S n) f = go n (f . FS) :< f FZ
 
 public export
-CanSubstSelf Var where
-  i    // Shift by   = shift by i
-  VZ   // (t ::: th) = t
-  VS i // (t ::: th) = i // th
-
-
-public export %inline
-shift : (by : Nat) -> Subst env from (by + from)
-shift by = Shift $ fromNat by
-
-public export %inline
-shift0 : (by : Nat) -> Subst env 0 by
-shift0 by = rewrite sym $ plusZeroRightNeutral by in Shift $ fromNat by
-
+id : FromVar term => {n : Nat} -> (under : Nat) -> Loc ->
+     Subst term n (n + under)
+id under loc =
+  map (\i => delay $ varT (weakenN under i) loc) (tabulate n)
 
 public export
-(.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to
-Shift by      . Shift bz   = Shift $ by . bz
-Shift SZ      . ph         = ph
-Shift (SS by) . (t ::: th) = Shift by . th
-(t ::: th)    . ph         = (t // ph) ::: (th . ph)
+id2 : FromVar2 term => {n : Nat} -> Loc -> Subst2 term d n n
+id2 loc = map (\i => delay $ varT2 i loc) $ tabulate n
 
-public export %inline
-id : Subst f n n
-id = shift 0
-
-public export
-traverse : Applicative m =>
-           (f to -> m (g to)) -> Subst f from to -> m (Subst g from to)
-traverse f (Shift by) = pure $ Shift by
-traverse f (t ::: th) = [|f t !::: traverse f th|]
-
--- not in terms of traverse because this map can maintain laziness better
-public export
-map : (f to -> g to) -> Subst f from to -> Subst g from to
-map f (Shift by) = Shift by
-map f (t ::: th) = f t ::: map f th
-
-
-public export %inline
-push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
-push th = fromVar VZ ::: (th . shift 1)
-
--- [fixme] a better way to do this?
-public export
-pushN : CanSubstSelf f => (s : Nat) ->
-        Subst f from to -> Subst f (s + from) (s + to)
-pushN 0     th = th
-pushN (S s) th =
-  rewrite plusSuccRightSucc s from in
-  rewrite plusSuccRightSucc s to in
-  pushN s $ fromVar VZ ::: (th . shift 1)
-
-public export
-drop1 : Subst f (S from) to -> Subst f from to
-drop1 (Shift by) = Shift $ ssDown by
-drop1 (t ::: th) = th
-
-
-public export
-fromSnocVect : SnocVect s (f n) -> Subst f (s + n) n
-fromSnocVect [<]       = id
-fromSnocVect (xs :< x) = x ::: fromSnocVect xs
-
-public export %inline
-one : f n -> Subst f (S n) n
-one x = fromSnocVect [< x]
-
-
-||| whether two substitutions with the same codomain have the same shape
-||| (the same number of terms and the same shift at the end). if so, they
-||| also have the same domain
 export
-cmpShape : Subst env from1 to -> Subst env from2 to ->
-           Either Ordering (from1 = from2)
-cmpShape (Shift by) (Shift bz) = cmpLen by bz
-cmpShape (Shift _)  (_ ::: _)  = Left LT
-cmpShape (_ ::: _)  (Shift _)  = Left GT
-cmpShape (_ ::: th) (_ ::: ph) = cong S <$> cmpShape th ph
+select : {n, mask : Nat} -> (0 ope : OPE m n mask) ->
+         SnocVect n a -> SnocVect m a
+select ope sx with %syntactic (view ope)
+  select _ [<]       | StopV       = [<]
+  select _ (sx :< x) | DropV _ ope = select ope sx
+  select _ (sx :< x) | KeepV _ ope = select ope sx :< x
+
+export
+opeToFins : {n, mask : Nat} ->
+            (0 ope : OPE m n mask) -> SnocVect m (Fin n)
+opeToFins ope = select ope $ tabulate n
+
+export
+shift : FromVar term => {from : Nat} ->
+        (n : Nat) -> Loc -> Subst term from (n + from)
+shift n loc = map (\i => delay $ varT (shift n i) loc) $ tabulate from
+
+public export
+pushN : CanSubstSelf term => {to : Nat} -> (by : Nat) ->
+        Subst term from to -> Loc -> Subst term (by + from) (by + to)
+pushN by th loc =
+  rewrite plusCommutative by from in
+  (th . shift by loc) ++ id to loc
+
+public export %inline
+push : CanSubstSelf f => {to : Nat} ->
+       Subst f from to -> Loc -> Subst f (S from) (S to)
+push = pushN 1
+
+
+public export %inline
+one : Thinned f n -> Subst f 1 n
+one x = [< x]
+
+
+||| whether two substitutions with the same codomain have the same domain
+export
+cmpShape : SnocVect m a -> SnocVect n a -> Either Ordering (m = n)
+cmpShape [<]       [<]       = Right Refl
+cmpShape [<]       (sx :< _) = Left LT
+cmpShape (sx :< _) [<]       = Left GT
+cmpShape (sx :< _) (sy :< _) = cong S <$> cmpShape sx sy
 
 
 public export
 record WithSubst tm env n where
   constructor Sub
   term  : tm from
-  subst : Lazy (Subst env from n)
+  subst : Subst env from n
 
+{-
 export
-(Eq (env n), forall n. Eq (tm n)) => Eq (WithSubst tm env n) where
+(forall n. Eq (env n), forall n. Eq (tm n)) =>
+Eq (WithSubst tm env n) where
   Sub t1 s1 == Sub t2 s2 =
     case cmpShape s1 s2 of
       Left  _    => False
-      Right Refl => t1 == t2 && s1 == s2
+      Right Refl =>
+        t1 == t2 && concat @{All} (zipWith ((==) `on` force) s1 s2)
 
 export
-(Ord (env n), forall n. Ord (tm n)) => Ord (WithSubst tm env n) where
+(forall n. Ord (env n), forall n. Ord (tm n)) =>
+Ord (WithSubst tm env n) where
   Sub t1 s1 `compare` Sub t2 s2 =
     case cmpShape s1 s2 of
       Left  o    => o
-      Right Refl => compare (t1, s1) (t2, s2)
+      Right Refl =>
+        compare t1 t2 <+> concat (zipWith (compare `on` force) s1 s2)
 
 export %hint
-ShowWithSubst : (Show (env n), forall n. Show (tm n)) =>
+ShowWithSubst : {n : Nat} ->
+                (forall n. Show (env n), forall n. Show (tm n)) =>
                 Show (WithSubst tm env n)
-ShowWithSubst = deriveShow
+ShowWithSubst = deriveShow where
+  Show (Lazy (Thinned env n)) where showPrec d = showPrec d . force
+-}
+
+
+public export
+record WithSubst2 tm env d n where
+  constructor Sub2
+  term  : tm d from
+  subst : Subst2 env d from n
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 994b570..e024e41 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -129,7 +129,7 @@ data Term where
   E : Elim d n -> Term d n
 
   ||| term closure/suspended substitution
-  CloT  : WithSubst (Term d) (Elim d) n -> Term d n
+  CloT  : WithSubst2 Term Elim d n -> Term d n
   ||| dimension closure/suspended substitution
   DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
 
@@ -194,7 +194,7 @@ data Elim where
                       ] d n -> Loc -> Elim d n
 
   ||| term closure/suspended substitution
-  CloE  : WithSubst (Elim d) (Elim d) n -> Elim d n
+  CloE  : WithSubst2 Elim Elim d n -> Elim d n
   ||| dimension closure/suspended substitution
   DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
 
@@ -325,7 +325,7 @@ Located (Elim d n) where
   (Coe _ loc).loc          = loc
   (Comp _ loc).loc         = loc
   (TypeCase _ loc).loc     = loc
-  (CloE (Sub e _)).loc     = e.loc
+  (CloE (Sub2 e _)).loc    = e.loc
   (DCloE (Sub e _)).loc    = e.loc
 
 export
@@ -345,7 +345,7 @@ Located (Term d n) where
   (BOX _ _ loc).loc     = loc
   (Box _ loc).loc       = loc
   (E e).loc             = e.loc
-  (CloT (Sub t _)).loc  = t.loc
+  (CloT (Sub2 t _)).loc = t.loc
   (DCloT (Sub t _)).loc = t.loc
 
 
@@ -363,7 +363,7 @@ Relocatable (Elim d n) where
   setLoc loc (Coe ts _)               = Coe ts loc
   setLoc loc (Comp ts _)              = Comp ts loc
   setLoc loc (TypeCase ts _)          = TypeCase ts loc
-  setLoc loc (CloE (Sub term subst))  = CloE $ Sub (setLoc loc term) subst
+  setLoc loc (CloE (Sub2 term subst)) = CloE $ Sub2 (setLoc loc term) subst
   setLoc loc (DCloE (Sub term subst)) = DCloE $ Sub (setLoc loc term) subst
 
 export
@@ -383,5 +383,5 @@ Relocatable (Term d n) where
   setLoc loc (BOX qty ty _)           = BOX qty ty loc
   setLoc loc (Box val _)              = Box val loc
   setLoc loc (E e)                    = E $ setLoc loc e
-  setLoc loc (CloT (Sub term subst))  = CloT $ Sub (setLoc loc term) subst
+  setLoc loc (CloT (Sub2 term subst)) = CloT $ Sub2 (setLoc loc term) subst
   setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index e7addb1..a8a4c83 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -18,11 +18,11 @@ prettyUniverse = hl Universe . text . show
 
 
 export
-prettyTerm : {opts : _} -> BContext d -> BContext n -> Term d n ->
+prettyTerm : {opts : _} -> BContext d -> BContext n -> TermT d n ->
              Eff Pretty (Doc opts)
 
 export
-prettyElim : {opts : _} -> BContext d -> BContext n -> Elim d n ->
+prettyElim : {opts : _} -> BContext d -> BContext n -> ElimT d n ->
              Eff Pretty (Doc opts)
 
 private
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index c0b62f6..8d2b8b1 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -2,374 +2,462 @@ module Quox.Syntax.Term.Subst
 
 import Quox.No
 import Quox.Syntax.Term.Base
-import Quox.Syntax.Term.Tighten
+import Quox.Syntax.Subst
+
 import Data.SnocVect
+import Data.Singleton
 
 %default total
 
-namespace CanDSubst
-  public export
-  interface CanDSubst (0 tm : TermLike) where
-    (//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n
 
-||| 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
-CanDSubst Term where
-  s                // Shift SZ = s
-  TYPE l loc       // _        = TYPE l loc
-  DCloT (Sub s ph) // th       = DCloT $ Sub s $ ph . th
-  s                // th       = DCloT $ Sub s th
+infixl 8 ///
 
-private
-subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
-subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
-subDArgs e              th = DCloE $ Sub e th
+parameters {0 f : Nat -> Nat -> Type}
+  private
+  th0 : f 0 0 -> Thinned2 f d n
+  th0 = Th2 zero zero
 
-||| 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
-CanDSubst Elim where
-  e                // Shift SZ = e
-  F x u loc        // _        = F x u loc
-  B i loc          // _        = B i loc
-  e@(DApp {})      // th       = subDArgs e th
-  DCloE (Sub e ph) // th       = DCloE $ Sub e $ ph . th
-  e                // th       = DCloE $ Sub e th
+  private
+  th1 : {d, n : Nat} -> f d n -> Thinned2 f d n
+  th1 = Th2 id' id'
 
-namespace DSubst.ScopeTermN
-  export %inline
-  (//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
-         ScopeTermN s d2 n
-  S ns (Y body) // th = S ns $ Y $ body // th
-  S ns (N body) // th = S ns $ N $ body // th
+private dsubTerm : {d1, d2, n : Nat} -> Term d1 n -> DSubst d1 d2 -> TermT d2 n
+private dsubElim : {d1, d2, n : Nat} -> Elim d1 n -> DSubst d1 d2 -> ElimT d2 n
 
-namespace DSubst.DScopeTermN
-  export %inline
-  (//) : {s : Nat} ->
-         DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
-         DScopeTermN s d2 n
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
-  S ns (N body) // th = S ns $ N $ body // th
+dsubTerm (TYPE l loc) th = th0 $ TYPE l loc
+dsubTerm (Enum strs loc) th = th0 $ Enum strs loc
+dsubTerm (Tag str loc) th = th0 $ Tag str loc
+dsubTerm (Nat loc) th = th0 $ Nat loc
+dsubTerm (Zero loc) th = th0 $ Zero loc
+dsubTerm (E e) th =
+  let Th2 dope tope e' = dsubElim e th in
+  Th2 dope tope $ E e'
+dsubTerm (DCloT (Sub t ph)) th = th1 $ DCloT $ Sub t $ ph . th
+dsubTerm t th = th1 $ DCloT $ Sub t th
 
-
-export %inline FromVar (Elim d) where fromVarLoc = B
-export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
-
-
-||| does the minimal reasonable work:
-||| - 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
-||| - otherwise, wraps in a new closure
-export
-CanSubstSelf (Elim d) where
-  F x u loc       // _  = F x u loc
-  B i loc         // th = getLoc th i loc
-  CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
-  e               // th = case force th of
-                               Shift SZ => e
-                               th       => CloE $ Sub e th
-
-namespace CanTSubst
-  public export
-  interface CanTSubst (0 tm : TermLike) where
-    (//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
-
-||| 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 closure
-||| - goes inside `E` in case it is a simple variable or something
-||| - otherwise, wraps in a new closure
-export
-CanTSubst Term where
-  TYPE l loc      // _  = TYPE l loc
-  E e             // th = E $ e // th
-  CloT (Sub s ph) // th = CloT $ Sub s $ ph . th
-  s               // th = case force th of
-                               Shift SZ => s
-                               th       => CloT $ Sub s th
-
-namespace ScopeTermN
-  export %inline
-  (//) : {s : Nat} ->
-         ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
-         ScopeTermN s d n2
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
-  S ns (N body) // th = S ns $ N $ body // th
-
-namespace DScopeTermN
-  export %inline
-  (//) : {s : Nat} ->
-         DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
-  S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
-  S ns (N body) // th = S ns $ N $ body // th
-
-export %inline CanShift (Term d) where s // by = s // Shift by
-export %inline CanShift (Elim d) where e // by = e // Shift by
-
-export %inline
-{s : Nat} -> CanShift (ScopeTermN s d) where
-  b // by = b // Shift by
-
-
-export %inline
-comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
-comp th ps ph = map (// th) ps . ph
-
-
-public export %inline
-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 by t = t // shift by
-
-
-public export %inline
-weakT : (by : Nat) -> Term d n -> Term d (by + n)
-weakT by t = t // shift by
-
-public export %inline
-weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
-weakE by t = t // shift by
-
-
-parameters {s : Nat}
-  namespace ScopeTermBody
-    export %inline
-    (.term) : ScopedBody s (Term d) n -> Term d (s + n)
-    (Y b).term = b
-    (N b).term = weakT s b
-
-  namespace ScopeTermN
-    export %inline
-    (.term) : ScopeTermN s d n -> Term d (s + n)
-    t.term = t.body.term
-
-  namespace DScopeTermBody
-    export %inline
-    (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
-    (Y b).term = b
-    (N b).term = dweakT s b
-
-  namespace DScopeTermN
-    export %inline
-    (.term) : DScopeTermN s d n -> Term (s + d) n
-    t.term = t.body.term
-
-
-export %inline
-subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
-subN (S _ (Y body)) es = body // fromSnocVect es
-subN (S _ (N body)) _  = body
-
-export %inline
-sub1 : ScopeTerm d n -> Elim d n -> Term d n
-sub1 t e = subN t [< e]
-
-export %inline
-dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
-dsubN (S _ (Y body)) ps = body // fromSnocVect ps
-dsubN (S _ (N body)) _  = body
-
-export %inline
-dsub1 : DScopeTerm d n -> Dim d -> Term d n
-dsub1 t p = dsubN t [< p]
-
-
-public export %inline
-(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
-body.zero = dsub1 body $ K Zero loc
-
-public export %inline
-(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
-body.one = dsub1 body $ K One loc
-
-
-public export
-0 CloTest : TermLike -> Type
-CloTest tm = forall d, n. tm d n -> Bool
-
-interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
-  pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
-                   tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
-
-public export
-0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
-NotClo = No . isClo
-
-public export
-0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
-           PushSubsts tm isClo => TermLike
-NonClo tm d n = Subset (tm d n) NotClo
-
-public export %inline
-nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
-       (t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
-nclo t = Element t nc
-
-parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
-  ||| if the input term has any top-level closures, push them under one layer of
-  ||| syntax
-  export %inline
-  pushSubsts : tm d n -> NonClo tm d n
-  pushSubsts s = pushSubstsWith id id s
-
-  export %inline
-  pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
-  pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
-
-  export %inline
-  pushSubsts' : tm d n -> tm d n
-  pushSubsts' s = fst $ pushSubsts s
+dsubElim (F x l loc) th = th0 $ F x l loc
+dsubElim (B loc) th = Th2 zero id' $ B loc
+dsubElim (DCloE (Sub e ph)) th = th1 $ DCloE $ Sub e $ ph . th
+dsubElim e th = th1 $ DCloE $ Sub e th
 
 mutual
-  public export
-  isCloT : CloTest Term
-  isCloT (CloT  {}) = True
-  isCloT (DCloT {}) = True
-  isCloT (E e)      = isCloE e
-  isCloT _          = False
+  namespace Term
+    export
+    (///) : {d1, d2, n : Nat} -> TermT d1 n -> DSubst d1 d2 -> TermT d2 n
+    Th2 dope tope term /// th =
+      let Val tscope = appOpe n tope; Val dscope = appOpe d1 dope
+          Th2 dope' tope' term' = dsubTerm term (select dope th)
+      in
+      Th2 dope' (tope . tope') term'
 
-  public export
-  isCloE : CloTest Elim
-  isCloE (CloE  {}) = True
-  isCloE (DCloE {}) = True
-  isCloE _          = False
-
-mutual
-  export
-  PushSubsts Term Subst.isCloT where
-    pushSubstsWith th ph (TYPE l loc) =
-      nclo $ TYPE l loc
-    pushSubstsWith th ph (Pi qty a body loc) =
-      nclo $ Pi qty (a // th // ph) (body // th // ph) loc
-    pushSubstsWith th ph (Lam body loc) =
-      nclo $ Lam (body // th // ph) loc
-    pushSubstsWith th ph (Sig a b loc) =
-      nclo $ Sig (a // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (Pair s t loc) =
-      nclo $ Pair (s // th // ph) (t // th // ph) loc
-    pushSubstsWith th ph (Enum tags loc) =
-      nclo $ Enum tags loc
-    pushSubstsWith th ph (Tag tag loc) =
-      nclo $ Tag tag loc
-    pushSubstsWith th ph (Eq ty l r loc) =
-      nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
-    pushSubstsWith th ph (DLam body loc) =
-      nclo $ DLam (body // th // ph) loc
-    pushSubstsWith _ _ (Nat loc) =
-      nclo $ Nat loc
-    pushSubstsWith _ _ (Zero loc) =
-      nclo $ Zero loc
-    pushSubstsWith th ph (Succ n loc) =
-      nclo $ Succ (n // th // ph) loc
-    pushSubstsWith th ph (BOX pi ty loc) =
-      nclo $ BOX pi (ty // th // ph) loc
-    pushSubstsWith th ph (Box val loc) =
-      nclo $ Box (val // th // ph) loc
-    pushSubstsWith th ph (E e) =
-      let Element e nc = pushSubstsWith th ph e in nclo $ E e
-    pushSubstsWith th ph (CloT (Sub s ps)) =
-      pushSubstsWith th (comp th ps ph) s
-    pushSubstsWith th ph (DCloT (Sub s ps)) =
-      pushSubstsWith (ps . th) ph s
-
-  export
-  PushSubsts Elim Subst.isCloE where
-    pushSubstsWith th ph (F x u loc) =
-      nclo $ F x u loc
-    pushSubstsWith th ph (B i loc) =
-      let res = getLoc ph i loc in
-      case nchoose $ isCloE res of
-        Left  yes => assert_total pushSubsts res
-        Right no  => Element res no
-    pushSubstsWith th ph (App f s loc) =
-      nclo $ App (f // th // ph) (s // th // ph) loc
-    pushSubstsWith th ph (CasePair pi p r b loc) =
-      nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (CaseEnum pi t r arms loc) =
-      nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
-               (map (\b => b // th // ph) arms) loc
-    pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
-      nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
-               (z // th // ph) (s // th // ph) loc
-    pushSubstsWith th ph (CaseBox pi x r b loc) =
-      nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (DApp f d loc) =
-      nclo $ DApp (f // th // ph) (d // th) loc
-    pushSubstsWith th ph (Ann s a loc) =
-      nclo $ Ann (s // th // ph) (a // th // ph) loc
-    pushSubstsWith th ph (Coe ty p q val loc) =
-      nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
-    pushSubstsWith th ph (Comp ty p q val r zero one loc) =
-      nclo $ Comp (ty // th // ph) (p // th) (q // th)
-                  (val // th // ph) (r // th)
-                  (zero // th // ph) (one // th // ph) loc
-    pushSubstsWith th ph (TypeCase ty ret arms def loc) =
-      nclo $ TypeCase (ty // th // ph) (ret  // th // ph)
-        (map (\t => t // th // ph) arms) (def // th // ph) loc
-    pushSubstsWith th ph (CloE (Sub e ps)) =
-      pushSubstsWith th (comp th ps ph) e
-    pushSubstsWith th ph (DCloE (Sub e ps)) =
-      pushSubstsWith (ps . th) ph e
+  namespace Elim
+    export
+    (///) : {d1, d2, n : Nat} -> ElimT d1 n -> DSubst d1 d2 -> ElimT d2 n
+    Th2 dope tope elim /// th =
+      let Val tscope = appOpe n tope; Val dscope = appOpe d1 dope
+          Th2 dope' tope' elim' = dsubElim elim (select dope th)
+      in
+      Th2 dope' (tope . tope') elim'
 
 
-private %inline
-CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
-         (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
-CompHY {ty, p, q, val, r, zero, one, loc} =
-  let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
-  Comp {
-    ty = dsub1 ty q, p, q,
-    val = E $ Coe ty p q val val.loc, r,
-    -- [fixme] better locations for these vars?
-    zero = SY zero.names $ E $
-      Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
-    one = SY one.names $ E $
-      Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
-    loc
-  }
+public export
+TSubst : Nat -> Nat -> Nat -> Type
+TSubst = Subst2 Elim
 
-public export %inline
-CompH' : (ty : DScopeTerm d n) ->
-         (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-         (zero : DScopeTerm d n) ->
-         (one : DScopeTerm d n) ->
-         (loc : Loc) ->
-         Elim d n
-CompH' {ty, p, q, val, r, zero, one, loc} =
-  case dsqueeze ty of
-    S _ (N ty) => Comp   {ty, p, q, val, r, zero, one, loc}
-    S _ (Y _)  => CompHY {ty, p, q, val, r, zero, one, loc}
 
-||| heterogeneous composition, using Comp and Coe (and subst)
-|||
-||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
-||| ≔
-||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
-|||   0 j ⇒ coe [i ⇒ A] @j @q t₀;
-|||   1 j ⇒ coe [i ⇒ A] @j @q t₁
-||| }
-public export %inline
-CompH : (i : BindName) -> (ty : Term (S d) n) ->
-        (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-        (j0 : BindName) -> (zero : Term (S d) n) ->
-        (j1 : BindName) -> (one : Term (S d) n) ->
-        (loc : Loc) ->
-        Elim d n
-CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
-  CompH' {ty = SY [< i] ty, p, q, val, r,
-          zero = SY [< j0] zero, one = SY [< j0] one, loc}
+public export %inline FromVar (Elim 0) where var = B
+
+export CanSubstSelf2 Elim
+
+private subTerm : {d, n1, n2 : Nat} -> Term d n1 -> TSubst d n1 n2 -> TermT d n2
+private subElim : {d, n1, n2 : Nat} -> Elim d n1 -> TSubst d n1 n2 -> ElimT d n2
+
+subTerm (TYPE l loc) th = th0 $ TYPE l loc
+subTerm (Nat loc) th = th0 $ Nat loc
+subTerm (Zero loc) th = th0 $ Zero loc
+subTerm (E e) th = let Th2 dope tope e' = subElim e th in Th2 dope tope $ E e'
+subTerm (CloT (Sub2 s ph)) th = th1 $ CloT $ Sub2 s $ ph .% th
+subTerm s th = th1 $ CloT $ Sub2 s th
+
+subElim (F x k loc) th = th0 $ F x k loc
+subElim (B loc) [< e] = e
+subElim (CloE (Sub2 e ph)) th = th1 $ CloE $ Sub2 e $ ph .% th
+subElim e th = th1 $ CloE $ Sub2 e th
+
+
+
+export
+CanSubstSelf2 Elim where
+  Th2 dope tope elim // th =
+    let
+        th' = select tope th
+    in
+    ?sube2
+
+-- namespace CanDSubst
+--   public export
+--   interface CanDSubst (0 tm : TermLike) where
+--     (//) : {d1 : Nat} -> Thinned2 tm d1 n -> Lazy (DSubst d1 d2) ->
+--            Thinned2 tm d2 n
+
+-- ||| 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
+-- CanDSubst Term where
+--   Th2 _ _ (TYPE l loc)       // _        = Th2 zero zero $ TYPE l loc
+--   Th2 i j (DCloT (Sub s ph)) // th       =
+--     Th2 ?i' j $ DCloT $ Sub s $ ph . ?th'
+--   Th2 i j s                  // th       = ?sdf -- DCloT $ Sub s th
+
+-- -- private
+-- -- subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
+-- -- subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
+-- -- subDArgs e              th = DCloE $ Sub 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
+-- -- CanDSubst Elim where
+-- --   e                // Shift SZ = e
+-- --   F x u loc        // _        = F x u loc
+-- --   B i loc          // _        = B i loc
+-- --   e@(DApp {})      // th       = subDArgs e th
+-- --   DCloE (Sub e ph) // th       = DCloE $ Sub e $ ph . th
+-- --   e                // th       = DCloE $ Sub e th
+
+-- -- namespace DSubst.ScopeTermN
+-- --   export %inline
+-- --   (//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
+-- --          ScopeTermN s d2 n
+-- --   S ns (Y body) // th = S ns $ Y $ body // th
+-- --   S ns (N body) // th = S ns $ N $ body // th
+
+-- -- namespace DSubst.DScopeTermN
+-- --   export %inline
+-- --   (//) : {s : Nat} ->
+-- --          DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
+-- --          DScopeTermN s d2 n
+-- --   S ns (Y body) // th = S ns $ Y $ body // pushN s th
+-- --   S ns (N body) // th = S ns $ N $ body // th
+
+
+-- -- export %inline FromVar (Elim d) where fromVarLoc = B
+-- -- export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
+
+
+-- -- ||| does the minimal reasonable work:
+-- -- ||| - 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
+-- -- ||| - otherwise, wraps in a new closure
+-- -- export
+-- -- CanSubstSelf (Elim d) where
+-- --   F x u loc       // _  = F x u loc
+-- --   B i loc         // th = getLoc th i loc
+-- --   CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
+-- --   e               // th = case force th of
+-- --                                Shift SZ => e
+-- --                                th       => CloE $ Sub e th
+
+-- -- namespace CanTSubst
+-- --   public export
+-- --   interface CanTSubst (0 tm : TermLike) where
+-- --     (//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
+
+-- -- ||| 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 closure
+-- -- ||| - goes inside `E` in case it is a simple variable or something
+-- -- ||| - otherwise, wraps in a new closure
+-- -- export
+-- -- CanTSubst Term where
+-- --   TYPE l loc      // _  = TYPE l loc
+-- --   E e             // th = E $ e // th
+-- --   CloT (Sub s ph) // th = CloT $ Sub s $ ph . th
+-- --   s               // th = case force th of
+-- --                                Shift SZ => s
+-- --                                th       => CloT $ Sub s th
+
+-- -- namespace ScopeTermN
+-- --   export %inline
+-- --   (//) : {s : Nat} ->
+-- --          ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
+-- --          ScopeTermN s d n2
+-- --   S ns (Y body) // th = S ns $ Y $ body // pushN s th
+-- --   S ns (N body) // th = S ns $ N $ body // th
+
+-- -- namespace DScopeTermN
+-- --   export %inline
+-- --   (//) : {s : Nat} ->
+-- --          DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
+-- --   S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
+-- --   S ns (N body) // th = S ns $ N $ body // th
+
+-- -- export %inline CanShift (Term d) where s // by = s // Shift by
+-- -- export %inline CanShift (Elim d) where e // by = e // Shift by
+
+-- -- export %inline
+-- -- {s : Nat} -> CanShift (ScopeTermN s d) where
+-- --   b // by = b // Shift by
+
+
+-- -- export %inline
+-- -- comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
+-- -- comp th ps ph = map (// th) ps . ph
+
+
+-- -- public export %inline
+-- -- 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 by t = t // shift by
+
+
+-- -- public export %inline
+-- -- weakT : (by : Nat) -> Term d n -> Term d (by + n)
+-- -- weakT by t = t // shift by
+
+-- -- public export %inline
+-- -- weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
+-- -- weakE by t = t // shift by
+
+
+-- -- parameters {s : Nat}
+-- --   namespace ScopeTermBody
+-- --     export %inline
+-- --     (.term) : ScopedBody s (Term d) n -> Term d (s + n)
+-- --     (Y b).term = b
+-- --     (N b).term = weakT s b
+
+-- --   namespace ScopeTermN
+-- --     export %inline
+-- --     (.term) : ScopeTermN s d n -> Term d (s + n)
+-- --     t.term = t.body.term
+
+-- --   namespace DScopeTermBody
+-- --     export %inline
+-- --     (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
+-- --     (Y b).term = b
+-- --     (N b).term = dweakT s b
+
+-- --   namespace DScopeTermN
+-- --     export %inline
+-- --     (.term) : DScopeTermN s d n -> Term (s + d) n
+-- --     t.term = t.body.term
+
+
+-- -- export %inline
+-- -- subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
+-- -- subN (S _ (Y body)) es = body // fromSnocVect es
+-- -- subN (S _ (N body)) _  = body
+
+-- -- export %inline
+-- -- sub1 : ScopeTerm d n -> Elim d n -> Term d n
+-- -- sub1 t e = subN t [< e]
+
+-- -- export %inline
+-- -- dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
+-- -- dsubN (S _ (Y body)) ps = body // fromSnocVect ps
+-- -- dsubN (S _ (N body)) _  = body
+
+-- -- export %inline
+-- -- dsub1 : DScopeTerm d n -> Dim d -> Term d n
+-- -- dsub1 t p = dsubN t [< p]
+
+
+-- -- public export %inline
+-- -- (.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+-- -- body.zero = dsub1 body $ K Zero loc
+
+-- -- public export %inline
+-- -- (.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+-- -- body.one = dsub1 body $ K One loc
+
+
+-- -- public export
+-- -- 0 CloTest : TermLike -> Type
+-- -- CloTest tm = forall d, n. tm d n -> Bool
+
+-- -- interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
+-- --   pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
+-- --                    tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
+
+-- -- public export
+-- -- 0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
+-- -- NotClo = No . isClo
+
+-- -- public export
+-- -- 0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
+-- --            PushSubsts tm isClo => TermLike
+-- -- NonClo tm d n = Subset (tm d n) NotClo
+
+-- -- public export %inline
+-- -- nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
+-- --        (t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
+-- -- nclo t = Element t nc
+
+-- -- parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
+-- --   ||| if the input term has any top-level closures, push them under one layer of
+-- --   ||| syntax
+-- --   export %inline
+-- --   pushSubsts : tm d n -> NonClo tm d n
+-- --   pushSubsts s = pushSubstsWith id id s
+
+-- --   export %inline
+-- --   pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
+-- --   pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
+
+-- --   export %inline
+-- --   pushSubsts' : tm d n -> tm d n
+-- --   pushSubsts' s = fst $ pushSubsts s
+
+-- -- mutual
+-- --   public export
+-- --   isCloT : CloTest Term
+-- --   isCloT (CloT  {}) = True
+-- --   isCloT (DCloT {}) = True
+-- --   isCloT (E e)      = isCloE e
+-- --   isCloT _          = False
+
+-- --   public export
+-- --   isCloE : CloTest Elim
+-- --   isCloE (CloE  {}) = True
+-- --   isCloE (DCloE {}) = True
+-- --   isCloE _          = False
+
+-- -- mutual
+-- --   export
+-- --   PushSubsts Term Subst.isCloT where
+-- --     pushSubstsWith th ph (TYPE l loc) =
+-- --       nclo $ TYPE l loc
+-- --     pushSubstsWith th ph (Pi qty a body loc) =
+-- --       nclo $ Pi qty (a // th // ph) (body // th // ph) loc
+-- --     pushSubstsWith th ph (Lam body loc) =
+-- --       nclo $ Lam (body // th // ph) loc
+-- --     pushSubstsWith th ph (Sig a b loc) =
+-- --       nclo $ Sig (a // th // ph) (b // th // ph) loc
+-- --     pushSubstsWith th ph (Pair s t loc) =
+-- --       nclo $ Pair (s // th // ph) (t // th // ph) loc
+-- --     pushSubstsWith th ph (Enum tags loc) =
+-- --       nclo $ Enum tags loc
+-- --     pushSubstsWith th ph (Tag tag loc) =
+-- --       nclo $ Tag tag loc
+-- --     pushSubstsWith th ph (Eq ty l r loc) =
+-- --       nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
+-- --     pushSubstsWith th ph (DLam body loc) =
+-- --       nclo $ DLam (body // th // ph) loc
+-- --     pushSubstsWith _ _ (Nat loc) =
+-- --       nclo $ Nat loc
+-- --     pushSubstsWith _ _ (Zero loc) =
+-- --       nclo $ Zero loc
+-- --     pushSubstsWith th ph (Succ n loc) =
+-- --       nclo $ Succ (n // th // ph) loc
+-- --     pushSubstsWith th ph (BOX pi ty loc) =
+-- --       nclo $ BOX pi (ty // th // ph) loc
+-- --     pushSubstsWith th ph (Box val loc) =
+-- --       nclo $ Box (val // th // ph) loc
+-- --     pushSubstsWith th ph (E e) =
+-- --       let Element e nc = pushSubstsWith th ph e in nclo $ E e
+-- --     pushSubstsWith th ph (CloT (Sub s ps)) =
+-- --       pushSubstsWith th (comp th ps ph) s
+-- --     pushSubstsWith th ph (DCloT (Sub s ps)) =
+-- --       pushSubstsWith (ps . th) ph s
+
+-- --   export
+-- --   PushSubsts Elim Subst.isCloE where
+-- --     pushSubstsWith th ph (F x u loc) =
+-- --       nclo $ F x u loc
+-- --     pushSubstsWith th ph (B i loc) =
+-- --       let res = getLoc ph i loc in
+-- --       case nchoose $ isCloE res of
+-- --         Left  yes => assert_total pushSubsts res
+-- --         Right no  => Element res no
+-- --     pushSubstsWith th ph (App f s loc) =
+-- --       nclo $ App (f // th // ph) (s // th // ph) loc
+-- --     pushSubstsWith th ph (CasePair pi p r b loc) =
+-- --       nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
+-- --     pushSubstsWith th ph (CaseEnum pi t r arms loc) =
+-- --       nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
+-- --                (map (\b => b // th // ph) arms) loc
+-- --     pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
+-- --       nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
+-- --                (z // th // ph) (s // th // ph) loc
+-- --     pushSubstsWith th ph (CaseBox pi x r b loc) =
+-- --       nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
+-- --     pushSubstsWith th ph (DApp f d loc) =
+-- --       nclo $ DApp (f // th // ph) (d // th) loc
+-- --     pushSubstsWith th ph (Ann s a loc) =
+-- --       nclo $ Ann (s // th // ph) (a // th // ph) loc
+-- --     pushSubstsWith th ph (Coe ty p q val loc) =
+-- --       nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
+-- --     pushSubstsWith th ph (Comp ty p q val r zero one loc) =
+-- --       nclo $ Comp (ty // th // ph) (p // th) (q // th)
+-- --                   (val // th // ph) (r // th)
+-- --                   (zero // th // ph) (one // th // ph) loc
+-- --     pushSubstsWith th ph (TypeCase ty ret arms def loc) =
+-- --       nclo $ TypeCase (ty // th // ph) (ret  // th // ph)
+-- --         (map (\t => t // th // ph) arms) (def // th // ph) loc
+-- --     pushSubstsWith th ph (CloE (Sub e ps)) =
+-- --       pushSubstsWith th (comp th ps ph) e
+-- --     pushSubstsWith th ph (DCloE (Sub e ps)) =
+-- --       pushSubstsWith (ps . th) ph e
+
+
+-- -- private %inline
+-- -- CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
+-- --          (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
+-- -- CompHY {ty, p, q, val, r, zero, one, loc} =
+-- --   let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
+-- --   Comp {
+-- --     ty = dsub1 ty q, p, q,
+-- --     val = E $ Coe ty p q val val.loc, r,
+-- --     -- [fixme] better locations for these vars?
+-- --     zero = SY zero.names $ E $
+-- --       Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
+-- --     one = SY one.names $ E $
+-- --       Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
+-- --     loc
+-- --   }
+
+-- -- public export %inline
+-- -- CompH' : (ty : DScopeTerm d n) ->
+-- --          (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
+-- --          (zero : DScopeTerm d n) ->
+-- --          (one : DScopeTerm d n) ->
+-- --          (loc : Loc) ->
+-- --          Elim d n
+-- -- CompH' {ty, p, q, val, r, zero, one, loc} =
+-- --   case dsqueeze ty of
+-- --     S _ (N ty) => Comp   {ty, p, q, val, r, zero, one, loc}
+-- --     S _ (Y _)  => CompHY {ty, p, q, val, r, zero, one, loc}
+
+-- -- ||| heterogeneous composition, using Comp and Coe (and subst)
+-- -- |||
+-- -- ||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
+-- -- ||| ≔
+-- -- ||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
+-- -- |||   0 j ⇒ coe [i ⇒ A] @j @q t₀;
+-- -- |||   1 j ⇒ coe [i ⇒ A] @j @q t₁
+-- -- ||| }
+-- -- public export %inline
+-- -- CompH : (i : BindName) -> (ty : Term (S d) n) ->
+-- --         (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
+-- --         (j0 : BindName) -> (zero : Term (S d) n) ->
+-- --         (j1 : BindName) -> (one : Term (S d) n) ->
+-- --         (loc : Loc) ->
+-- --         Elim d n
+-- -- CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
+-- --   CompH' {ty = SY [< i] ty, p, q, val, r,
+-- --           zero = SY [< j0] zero, one = SY [< j0] one, loc}
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index f9a648e..9edfb5c 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -138,15 +138,6 @@ export
 weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
 
 
-public export
-interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
-
-public export %inline
-fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
-fromVar x = fromVarLoc x loc
-
-public export FromVar Var where fromVarLoc x _ = x
-
 export
 tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
             (n : Nat) -> Vect n (tm n)
diff --git a/lib/Quox/Thin/Base.idr b/lib/Quox/Thin/Base.idr
index a60c185..1f24e5b 100644
--- a/lib/Quox/Thin/Base.idr
+++ b/lib/Quox/Thin/Base.idr
@@ -53,7 +53,7 @@ id {m = 0}   = Element _ Stop
 id {m = S m} = Element _ $ Keep id.snd Refl
 
 public export %inline
-0 id' : OPE m m Base.id.fst
+0 id' : {m : Nat} -> OPE m m (fst (Base.id {m}))
 id' = id.snd
 
 ||| nothing selected
diff --git a/lib/Quox/Thin/Comp.idr b/lib/Quox/Thin/Comp.idr
index 4561898..7352cfb 100644
--- a/lib/Quox/Thin/Comp.idr
+++ b/lib/Quox/Thin/Comp.idr
@@ -2,6 +2,7 @@ module Quox.Thin.Comp
 
 import public Quox.Thin.Base
 import public Quox.Thin.View
+import Quox.NatExtra
 import Data.Singleton
 
 %default total
@@ -52,8 +53,3 @@ export
 0 (.) : (ope1 : OPE n p mask1) -> (ope2 : OPE m n mask2) ->
         OPE m p (comp ope1 ope2).mask
 ope1 . ope2 = (comp ope1 ope2).ope
-
--- export
--- 0 compMask : (ope1 : OPE n p mask1) -> (ope2 : OPE m n mask2) ->
---              (ope3 : OPE m p mask3) -> Comp ope1 ope2 ope3 ->
---              mask3 = ?aaa
diff --git a/lib/Quox/Thin/Term.idr b/lib/Quox/Thin/Term.idr
index 25313e4..74f2420 100644
--- a/lib/Quox/Thin/Term.idr
+++ b/lib/Quox/Thin/Term.idr
@@ -5,6 +5,7 @@ import public Quox.Thin.Comp
 import public Quox.Thin.List
 import Quox.Thin.Eqv
 import public Quox.Thin.Cover
+import Quox.Thin.Append
 import Quox.Name
 import Quox.Loc
 import Data.DPair
@@ -15,6 +16,13 @@ import Decidable.Equality
 
 %default total
 
+private
+cmpMask : (m, n : Nat) -> Either Ordering (m = n)
+cmpMask 0     0     = Right Refl
+cmpMask 0     (S n) = Left  LT
+cmpMask (S m) 0     = Left  GT
+cmpMask (S m) (S n) = map (cong S) $ cmpMask m n
+
 public export
 record Thinned f n where
   constructor Th
@@ -26,9 +34,20 @@ record Thinned f n where
 
 export
 (forall n. Eq (f n)) => Eq (Thinned f n) where
-  s == t = case decEq s.scopeMask t.scopeMask of
-    Yes eq => s.term == (rewrite maskEqInner s.ope t.ope eq in t.term)
-    No  _  => False
+  s == t = case cmpMask s.scopeMask t.scopeMask of
+    Left  _  => False
+    Right eq => s.term == (rewrite maskEqInner s.ope t.ope eq in t.term)
+
+export
+(forall n. Ord (f n)) => Ord (Thinned f n) where
+  compare s t = case cmpMask s.scopeMask t.scopeMask of
+    Left  o  => o
+    Right eq => compare s.term (rewrite maskEqInner s.ope t.ope eq in t.term)
+
+export
+{n : Nat} -> (forall s. Show (f s)) => Show (Thinned f n) where
+  showPrec d (Th ope term) =
+    showCon d "Th" $ showArg (unVal $ maskToOpe ope) ++ showArg term
 
 export
 (forall n. Located (f n)) => Located (Thinned f n) where
@@ -47,6 +66,10 @@ namespace Thinned
   join : {n : Nat} -> Thinned (Thinned f) n -> Thinned f n
   join (Th ope1 (Th ope2 term)) = Th (ope1 . ope2) term
 
+  export
+  weak : {n : Nat} -> (by : Nat) -> Thinned f n -> Thinned f (by + n)
+  weak by (Th ope term) = Th (zero ++ ope).snd term
+
 
 public export
 record ScopedN (s : Nat) (f : Nat -> Type) (n : Nat) where
@@ -104,6 +127,14 @@ export
                  rewrite maskEqInner s.tope t.tope teq in t.term)
     _ => False
 
+export
+{d, n : Nat} -> (forall sd, sn. Show (f sd sn)) => Show (Thinned2 f d n) where
+  showPrec d (Th2 dope tope term) =
+    showCon d "Th2" $
+      showArg (unVal $ maskToOpe dope) ++
+      showArg (unVal $ maskToOpe tope) ++
+      showArg term
+
 export
 (forall d, n. Located (f d n)) => Located (Thinned2 f d n) where
   term.loc = term.term.loc
@@ -122,6 +153,12 @@ namespace Thinned2
   join (Th2 dope1 tope1 (Th2 dope2 tope2 term)) =
     Th2 (dope1 . dope2) (tope1 . tope2) term
 
+  export
+  weak : {d, n : Nat} -> (dby, nby : Nat) ->
+         Thinned2 f d n -> Thinned2 f (dby + d) (nby + n)
+  weak dby nby (Th2 dope tope term) =
+    Th2 (zero ++ dope).snd (zero ++ tope).snd term
+
 
 namespace TermList
   public export
diff --git a/lib/Quox/Thin/View.idr b/lib/Quox/Thin/View.idr
index 59a5269..480f9db 100644
--- a/lib/Quox/Thin/View.idr
+++ b/lib/Quox/Thin/View.idr
@@ -4,6 +4,7 @@ import public Quox.Thin.Base
 import Quox.NatExtra
 import Data.Singleton
 import Data.SnocVect
+import Data.Fin
 
 %default total
 
@@ -52,6 +53,12 @@ view {n = S n} ope with %syntactic (half mask)
   _ | HalfEven mask' with %syntactic 0 (fromDrop ope)
     _ | (ope' ** eq) = rewrite eq in DropV mask' ope'
 
+export
+(.fin) : {n, mask : Nat} -> (0 ope : OPE 1 n mask) -> Fin n
+ope.fin with (view ope)
+  _.fin | DropV _ ope = FS ope.fin
+  _.fin | KeepV _ ope = FZ
+
 
 export
 appOpe : {0 m : Nat} -> (n : Nat) -> {mask : Nat} ->
@@ -83,21 +90,11 @@ viewStop = Refl
 export
 0 viewDrop : (ope : OPE m n mask) -> (eq : mask2 = mask + mask) ->
              view (Drop {mask} ope eq) = DropV mask ope
-viewDrop ope eq with (view (Drop ope eq))
+viewDrop ope eq with %syntactic (view (Drop ope eq))
   viewDrop ope Refl | DropV _ ope = Refl
 
 export
 0 viewKeep : (ope : OPE m n mask) -> (eq : mask2 = S (mask + mask)) ->
              view (Keep {mask} ope eq) = KeepV mask ope
-viewKeep ope eq with (view (Keep ope eq))
+viewKeep ope eq with %syntactic (view (Keep ope eq))
   viewKeep ope Refl | KeepV _ ope = Refl
-
-
-namespace SnocVect
-  export
-  select : {n, mask : Nat} -> (0 ope : OPE m n mask) ->
-           SnocVect n a -> SnocVect m a
-  select ope sx with (view ope)
-    select _ [<]       | StopV       = [<]
-    select _ (sx :< x) | DropV _ ope = select ope sx
-    select _ (sx :< x) | KeepV _ ope = select ope sx :< x