From 3fb8580f85dd183e1473c774376dcd677afa6e35 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 17 Apr 2023 20:56:31 +0200
Subject: [PATCH] re-add tightening and use it when messing with scopes
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

e.g. "coe [_ ⇒ A] @p @q s" should immediately reduce to "s",
but if the "_ ⇒ A" happened to use an SY it didn't.

this will still happen if a wrong SY sneaks in but the alternative is
re-traversing the term over and over every time whnf runs
---
 lib/{on-hold => }/Quox/NatExtra.idr |   0
 lib/Quox/OPE.idr                    |  76 ++++++++
 lib/Quox/Parser/FromParser.idr      |   7 +-
 lib/Quox/Reduce.idr                 |  88 +++++----
 lib/Quox/Syntax/Shift.idr           |  21 ++-
 lib/Quox/Syntax/Subst.idr           |  13 ++
 lib/Quox/Syntax/Term.idr            |   1 +
 lib/Quox/Syntax/Term/Base.idr       |  22 +--
 lib/Quox/Syntax/Term/Split.idr      |   5 +-
 lib/Quox/Syntax/Term/Subst.idr      |  42 ++++-
 lib/Quox/Syntax/Term/Tighten.idr    | 274 ++++++++++++++++++++++++++++
 lib/Quox/Syntax/Var.idr             |  22 ++-
 lib/on-hold/Quox/OPE.idr            | 196 --------------------
 lib/quox-lib.ipkg                   |   3 +
 tests/Tests/PrettyTerm.idr          |  12 +-
 tests/Tests/Typechecker.idr         |  56 +++---
 16 files changed, 534 insertions(+), 304 deletions(-)
 rename lib/{on-hold => }/Quox/NatExtra.idr (100%)
 create mode 100644 lib/Quox/OPE.idr
 create mode 100644 lib/Quox/Syntax/Term/Tighten.idr
 delete mode 100644 lib/on-hold/Quox/OPE.idr

diff --git a/lib/on-hold/Quox/NatExtra.idr b/lib/Quox/NatExtra.idr
similarity index 100%
rename from lib/on-hold/Quox/NatExtra.idr
rename to lib/Quox/NatExtra.idr
diff --git a/lib/Quox/OPE.idr b/lib/Quox/OPE.idr
new file mode 100644
index 0000000..31203eb
--- /dev/null
+++ b/lib/Quox/OPE.idr
@@ -0,0 +1,76 @@
+||| "order preserving embeddings", for recording a correspondence between
+||| a smaller scope and part of a larger one.
+module Quox.OPE
+
+import Quox.NatExtra
+import Data.Nat
+
+%default total
+
+
+public export
+data OPE : Nat -> Nat -> Type where
+  Id   : OPE n n
+  Drop : OPE m n -> OPE m     (S n)
+  Keep : OPE m n -> OPE (S m) (S n)
+%name OPE p, q
+
+public export %inline Injective Drop where injective Refl = Refl
+public export %inline Injective Keep where injective Refl = Refl
+
+public export
+opeZero : {n : Nat} -> OPE 0 n
+opeZero {n = 0}   = Id
+opeZero {n = S n} = Drop opeZero
+
+public export
+(.) : OPE m n -> OPE n p -> OPE m p
+p      . Id     = p
+Id     . q      = q
+p      . Drop q = Drop $ p . q
+Drop p . Keep q = Drop $ p . q
+Keep p . Keep q = Keep $ p . q
+
+public export
+toLTE : {m : Nat} -> OPE m n -> m `LTE` n
+toLTE Id       = reflexive
+toLTE (Drop p) = lteSuccRight $ toLTE p
+toLTE (Keep p) = LTESucc      $ toLTE p
+
+
+public export
+keepN : (n : Nat) -> OPE a b -> OPE (n + a) (n + b)
+keepN 0     p = p
+keepN (S n) p = Keep $ keepN n p
+
+public export
+dropInner' : LTE' m n -> OPE m n
+dropInner' LTERefl      = Id
+dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
+
+public export
+dropInner : {n : Nat} -> LTE m n -> OPE m n
+dropInner = dropInner' . fromLte
+
+public export
+dropInnerN : (m : Nat) -> OPE n (m + n)
+dropInnerN 0     = Id
+dropInnerN (S m) = Drop $ dropInnerN m
+
+
+public export
+interface Tighten t where
+  tighten : OPE m n -> t n -> Maybe (t m)
+
+parameters {auto _ : Tighten t}
+  export %inline
+  tightenInner : {n : Nat} -> m `LTE` n -> t n -> Maybe (t m)
+  tightenInner = tighten . dropInner
+
+  export %inline
+  tightenN : (m : Nat) -> t (m + n) -> Maybe (t n)
+  tightenN m = tighten $ dropInnerN m
+
+  export %inline
+  tighten1 : t (S n) -> Maybe (t n)
+  tighten1 = tightenN 1
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 34ba61b..34bc3ba 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -164,9 +164,8 @@ mutual
         <*> fromPDimWith ds q
         <*> fromPTermWith ds ns val
 
-    -- [todo] direct translation for homo comp?
     Comp (i, ty) p q val r (j0, val0) (j1, val1) =>
-      map E $ CompH
+      map E $ CompH'
         <$> fromPTermDScope ds ns [< i] ty
         <*> fromPDimWith ds p
         <*> fromPDimWith ds q
@@ -201,7 +200,7 @@ mutual
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
     else
-      SY (fromSnocVect $ map (maybe Unused UN) xs)
+      ST (fromSnocVect $ map (maybe Unused UN) xs)
         <$> fromPTermWith ds (ns ++ xs) t
 
   private
@@ -213,7 +212,7 @@ mutual
     if all isNothing xs then
       SN <$> fromPTermWith ds ns t
     else
-      SY (fromSnocVect $ map (maybe Unused UN) xs)
+      DST (fromSnocVect $ map (maybe Unused UN) xs)
         <$> fromPTermWith (ds ++ xs) ns t
 
 
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 1b39cc6..abcbe76 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -251,8 +251,8 @@ mutual
     tycasePi (Pi {arg, res, _}) = pure (arg, res)
     tycasePi (E e) {tnf} = do
       ty <- computeElimType defs ctx e @{noOr2 tnf}
-      let arg  = E $ typeCase1 e ty KPi [< "Arg", "Ret"] (BVT 1)
-          res' = typeCase1 e (Arr Zero arg ty) KPi [< "Arg", "Ret"] (BVT 0)
+      let arg  = E $ typeCase1Y e ty KPi [< "Arg", "Ret"] (BVT 1)
+          res' = typeCase1Y e (Arr Zero arg ty) KPi [< "Arg", "Ret"] (BVT 0)
           res  = SY [< "Arg"] $ E $ weakE 1 res' :@ BVT 0
       pure (arg, res)
     tycasePi t = Left $ ExpectedPi ctx.names t
@@ -266,8 +266,8 @@ mutual
     tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
     tycaseSig (E e) {tnf} = do
       ty <- computeElimType defs ctx e @{noOr2 tnf}
-      let fst  = E $ typeCase1 e ty KSig [< "Fst", "Snd"] (BVT 1)
-          snd' = typeCase1 e (Arr Zero fst ty) KSig [< "Fst", "Snd"] (BVT 0)
+      let fst  = E $ typeCase1Y e ty KSig [< "Fst", "Snd"] (BVT 1)
+          snd' = typeCase1Y e (Arr Zero fst ty) KSig [< "Fst", "Snd"] (BVT 0)
           snd  = SY [< "Fst"] $ E $ weakE 1 snd' :@ BVT 0
       pure (fst, snd)
     tycaseSig t = Left $ ExpectedSig ctx.names t
@@ -281,7 +281,7 @@ mutual
     tycaseBOX (BOX _ a) = pure a
     tycaseBOX (E e) {tnf} = do
       ty <- computeElimType defs ctx e @{noOr2 tnf}
-      pure $ E $ typeCase1 e ty KBOX [< "Ty"] (BVT 0)
+      pure $ E $ typeCase1Y e ty KBOX [< "Ty"] (BVT 0)
     tycaseBOX t = Left $ ExpectedBOX ctx.names t
 
     ||| for Eq [i ⇒ A] l r, returns (A‹0/i›, A‹1/i›, A, l, r);
@@ -295,12 +295,12 @@ mutual
     tycaseEq (E e) {tnf} = do
       ty <- computeElimType defs ctx e @{noOr2 tnf}
       let names = [< "A0", "A1", "A", "L", "R"]
-          a0 = E $ typeCase1 e ty KEq names (BVT 4)
-          a1 = E $ typeCase1 e ty KEq names (BVT 3)
-          a' = typeCase1 e (Eq0 ty a0 a1) KEq names (BVT 2)
+          a0 = E $ typeCase1Y e ty KEq names (BVT 4)
+          a1 = E $ typeCase1Y e ty KEq names (BVT 3)
+          a' = typeCase1Y e (Eq0 ty a0 a1) KEq names (BVT 2)
           a  = SY [< "i"] $ E $ dweakE 1 a' :% BV 0
-          l  = E $ typeCase1 e a0 KEq names (BVT 1)
-          r  = E $ typeCase1 e a1 KEq names (BVT 0)
+          l  = E $ typeCase1Y e a0 KEq names (BVT 1)
+          r  = E $ typeCase1Y e a1 KEq names (BVT 0)
       pure (a0, a1, a, l, r)
     tycaseEq t = Left $ ExpectedEq ctx.names t
 
@@ -310,20 +310,20 @@ mutual
     private covering
     piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val, s : Term d n) ->
             Either Error (Subset (Elim d n) (No . isRedexE defs))
-    piCoe sty@(S i ty) p q val s = do
+    piCoe sty@(S [< i] ty) p q val s = do
       -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
       -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
       --   where 𝒔‹j› ≔ coe [i ⇒ A] @q @j s
       --
       -- type-case is used to expose A,B if the type is neutral
-      let ctx1 = extendDimN i ctx
+      let ctx1 = extendDim i ctx
       Element ty tynf <- whnf defs ctx1 ty.term
       (arg, res) <- tycasePi defs ctx1 ty
-      let s0   = Coe (SY i arg) q p s
+      let s0   = CoeT i arg q p s
           body = E $ (val :# (ty // one p)) :@ E s0
-          s1   = Coe (SY i (arg // (BV 0 ::: shift 2))) (weakD 1 q) (BV 0)
-                     (s // shift 1)
-      whnf defs ctx $ Coe (SY i $ sub1 res s1) p q body
+          s1   = CoeT i (arg // (BV 0 ::: shift 2)) (weakD 1 q) (BV 0)
+                      (s // shift 1)
+      whnf defs ctx $ CoeT i (sub1 res s1) p q body
 
     ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body`
     private covering
@@ -331,7 +331,7 @@ mutual
              (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
              (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) ->
              Either Error (Subset (Elim d n) (No . isRedexE defs))
-    sigCoe qty sty@(S i ty) p q val ret body = do
+    sigCoe qty sty@(S [< i] ty) p q val ret body = do
       -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
       -- ⇝
       -- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
@@ -340,33 +340,33 @@ mutual
       --     (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @q b)/b] }
       --
       -- type-case is used to expose A,B if the type is neutral
-      let ctx1 = extendDimN i ctx
+      let ctx1 = extendDim i ctx
       Element ty tynf <- whnf defs ctx1 ty.term
       (tfst, tsnd) <- tycaseSig defs ctx1 ty
-      let a' = Coe (SY i $ weakT 2 tfst) p q (BVT 1)
+      let a' = CoeT i (weakT 2 tfst) p q (BVT 1)
           tsnd' = tsnd.term //
-            (Coe (SY i $ weakT 2 $ tfst // (BV 0 ::: shift 2))
+            (CoeT i (weakT 2 $ tfst // (BV 0 ::: shift 2))
               (weakD 1 p) (BV 0) (BVT 1) ::: shift 2)
-          b' = Coe (SY i tsnd') p q (BVT 0)
+          b' = CoeT i tsnd' p q (BVT 0)
       whnf defs ctx $ CasePair qty (val :# (ty // one p)) ret $
-        SY body.names $ body.term // (a' ::: b' ::: shift 2)
+        ST body.names $ body.term // (a' ::: b' ::: shift 2)
 
     ||| reduce a dimension application `Coe ty p q val :% r`
     private covering
     eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
             (r : Dim d) ->
             Either Error (Subset (Elim d n) (No . isRedexE defs))
-    eqCoe sty@(S j ty) p q val r = do
+    eqCoe sty@(S [< j] ty) p q val r = do
       -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
       -- ⇝
       -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
       --   { (r=0) j ⇒ L; (r=1) j ⇒ R }
-      let ctx1 = extendDimN j ctx
+      let ctx1 = extendDim j ctx
       Element ty tynf <- whnf defs ctx1 ty.term
       (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
-      let a'   = SY j $ dsub1 a (weakD 1 r)
+      let a'   = dsub1 a (weakD 1 r)
           val' = E $ (val :# (ty // one p)) :% r
-      whnf defs ctx $ CompH a' p q val' r (SY j s) (SY j t)
+      whnf defs ctx $ CompH j a' p q val' r j s j t
 
     ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
     private covering
@@ -374,17 +374,17 @@ mutual
              (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
              (ret : ScopeTerm d n) -> (body : ScopeTerm d n) ->
              Either Error (Subset (Elim d n) (No . isRedexE defs))
-    boxCoe qty sty@(S i ty) p q val ret body = do
+    boxCoe qty sty@(S [< i] ty) p q val ret body = do
       -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
       -- ⇝
       -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C
       -- of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
-      let ctx1 = extendDimN i ctx
+      let ctx1 = extendDim i ctx
       Element ty tynf <- whnf defs ctx1 ty.term
       ta <- tycaseBOX defs ctx1 ty
-      let a' = Coe (SY i $ weakT 1 ta) p q $ BVT 0
+      let a' = CoeT i (weakT 1 ta) p q $ BVT 0
       whnf defs ctx $ CaseBox qty (val :# (ty // one p)) ret $
-        SY body.names $ body.term // (a' ::: shift 1)
+        ST body.names $ body.term // (a' ::: shift 1)
 
 
   export covering
@@ -641,8 +641,8 @@ mutual
       -- just η expand it. then whnf for (:@) will handle it later
       -- this is how @xtt does it
       Lam body => do
-        let body' = Coe (SY [< i] ty) p q (Lam body)
-            term' = Lam (SY [< "y"] $ E $ weakE 1 body' :@ BVT 0)
+        let body' = CoeT i ty p q $ Lam body
+            term' = [< "y"] :\\ E (weakE 1 body' :@ BVT 0)
             type' = ty // one q
         whnf defs ctx $ term' :# type'
 
@@ -654,10 +654,10 @@ mutual
       Lam body => do
         let Pi {qty, arg, res} = ty
           | _ => Left $ ?err
-        let arg' = SY [< "j"] $ weakT 1 $ arg // (BV 0 ::: shift 2)
-            res' = SY [< i] $ res.term //
+        let arg' = ST [< "j"] $ weakT 1 $ arg // (BV 0 ::: shift 2)
+            res' = ST [< i] $ res.term //
                       (Coe arg' (weakD 1 q) (BV 0) (BVT 0) ::: shift 1)
-            body = SY body.names $ E $ Coe res' p q body.term
+            body = ST body.names $ E $ Coe res' p q body.term
         pure $ Element (Lam body :# Pi qty (arg // one q) (res // one q)) Ah
       -}
 
@@ -670,18 +670,17 @@ mutual
       Pair fst snd => do
         let Sig {fst = tfst, snd = tsnd} = ty
           | _ => Left $ ExpectedSig (extendDim i ctx.names) ty
-        let fst'  = E $ Coe (SY [< i] tfst) p q fst
-            tfst' = SY [< "j"] $ tfst `CanDSubst.(//)` (BV 0 ::: shift 2)
-            tsnd' = SY [< i] $ sub1 tsnd $
-                      Coe tfst' (weakD 1 p) (BV 0) $ dweakT 1 fst
-            snd'  = E $ Coe tsnd' p q snd
+        let fst'  = E $ CoeT i tfst p q fst
+            tfst' = tfst // (BV 0 ::: shift 2)
+            tsnd' = sub1 tsnd $ CoeT "j" tfst' (weakD 1 p) (BV 0) $ dweakT 1 fst
+            snd'  = E $ CoeT i tsnd' p q snd
         pure $
           Element (Pair fst' snd' :# Sig (tfst // one q) (tsnd // one q)) Ah
 
       -- η expand like λ
       DLam body => do
-        let body' = Coe (SY [< i] ty) p q (DLam body)
-            term' = DLam (SY [< "j"] $ E $ dweakE 1 body' :% BV 0)
+        let body' = CoeT i ty p q $ DLam body
+            term' = [< "j"] :\\% E (dweakE 1 body' :% BV 0)
             type' = ty // one q
         whnf defs ctx $ term' :# type'
 
@@ -700,10 +699,9 @@ mutual
       Box val => do
         let BOX {qty, ty = a} = ty
           | _ => Left $ ExpectedBOX (extendDim i ctx.names) ty
-        let a = SY [< i] a
-        pure $ Element (Box (E $ Coe a p q s) :# BOX qty (dsub1 a q)) Ah
+        pure $ Element (Box (E $ CoeT i a p q s) :# BOX qty (a // one q)) Ah
 
-      E e => pure $ Element (Coe (SY [< i] ty) p q (E e)) (snf `orNo` Ah)
+      E e => pure $ Element (CoeT i ty p q (E e)) (snf `orNo` Ah)
   where
     unwrapTYPE : Term (S d) n -> Either Error Universe
     unwrapTYPE (TYPE u) = pure u
diff --git a/lib/Quox/Syntax/Shift.idr b/lib/Quox/Syntax/Shift.idr
index b03830e..943ed8a 100644
--- a/lib/Quox/Syntax/Shift.idr
+++ b/lib/Quox/Syntax/Shift.idr
@@ -11,7 +11,7 @@ import Data.So
 
 ||| represents the difference between a smaller scope and a larger one.
 public export
-data Shift : (0 from, to : Nat) -> Type where
+data Shift : (from, to : Nat) -> Type where
   SZ : Shift from from
   SS : Shift from to -> Shift from (S to)
 %name Shift by, bz
@@ -120,6 +120,25 @@ ssDownViaNat by =
 %transform "Shift.ssDown" ssDown = ssDownViaNat
 
 
+public export
+weak : (s : Nat) -> Shift from to -> Shift (s + from) (s + to)
+weak s SZ = SZ
+weak s (SS by) {to = S to} =
+  rewrite sym $ plusSuccRightSucc s to in
+  SS $ weak s by
+
+private
+weakViaNat : (s : Nat) -> Shift from to -> Shift (s + from) (s + to)
+weakViaNat s by =
+  rewrite shiftDiff by in
+  rewrite plusAssociative s by.nat from in
+  rewrite plusCommutative s by.nat in
+  rewrite sym $ plusAssociative by.nat s from in
+  fromNat by.nat
+
+%transform "Shift.weak" Shift.weak = weakViaNat
+
+
 public export
 shift : Shift from to -> Var from -> Var to
 shift SZ      i = i
diff --git a/lib/Quox/Syntax/Subst.idr b/lib/Quox/Syntax/Subst.idr
index 4c744bc..af47df2 100644
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@@ -18,6 +18,12 @@ data Subst : (Nat -> Type) -> Nat -> Nat -> Type where
   (:::) : (t : Lazy (env to)) -> Subst env from to -> Subst env (S from) to
 %name Subst th, ph, ps
 
+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
+
 
 private
 Repr : (Nat -> Type) -> Nat -> Type
@@ -74,6 +80,13 @@ 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
diff --git a/lib/Quox/Syntax/Term.idr b/lib/Quox/Syntax/Term.idr
index 76894ec..b0dddec 100644
--- a/lib/Quox/Syntax/Term.idr
+++ b/lib/Quox/Syntax/Term.idr
@@ -4,3 +4,4 @@ import public Quox.Syntax.Term.Base
 import public Quox.Syntax.Term.Split
 import public Quox.Syntax.Term.Subst
 import public Quox.Syntax.Term.Pretty
+import public Quox.Syntax.Term.Tighten
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 2a874ad..5c01df4 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -228,9 +228,9 @@ s.name = name s
 
 ||| more convenient Pi
 public export %inline
-Pi_ : (qty : Qty) -> (x : BaseName) ->
+PiY : (qty : Qty) -> (x : BaseName) ->
       (arg : Term d n) -> (res : Term d (S n)) -> Term d n
-Pi_ {qty, x, arg, res} = Pi {qty, arg, res = S [< x] $ Y res}
+PiY {qty, x, arg, res} = Pi {qty, arg, res = SY [< x] res}
 
 ||| non dependent function type
 public export %inline
@@ -239,9 +239,9 @@ Arr {qty, arg, res} = Pi {qty, arg, res = SN res}
 
 ||| more convenient Sig
 public export %inline
-Sig_ : (x : BaseName) -> (fst : Term d n) ->
+SigY : (x : BaseName) -> (fst : Term d n) ->
        (snd : Term d (S n)) -> Term d n
-Sig_ {x, fst, snd} = Sig {fst, snd = S [< x] $ Y snd}
+SigY {x, fst, snd} = Sig {fst, snd = SY [< x] snd}
 
 ||| non dependent pair type
 public export %inline
@@ -250,9 +250,9 @@ And {fst, snd} = Sig {fst, snd = SN snd}
 
 ||| more convenient Eq
 public export %inline
-Eq_ : (i : BaseName) -> (ty : Term (S d) n) ->
+EqY : (i : BaseName) -> (ty : Term (S d) n) ->
       (l, r : Term d n) -> Term d n
-Eq_ {i, ty, l, r} = Eq {ty = S [< i] $ Y ty, l, r}
+EqY {i, ty, l, r} = Eq {ty = SY [< i] ty, l, r}
 
 ||| non dependent equality type
 public export %inline
@@ -290,9 +290,9 @@ typeCase : Elim d n -> Term d n ->
 typeCase ty ret arms def = TypeCase ty ret (fromList arms) def
 
 public export %inline
-typeCase1 : Elim d n -> Term d n ->
-            (k : TyConKind) -> NContext (arity k) -> Term d (arity k + n) ->
-            {default Nat def : Term d n} ->
-            Elim d n
-typeCase1 ty ret k ns body {def} =
+typeCase1Y : Elim d n -> Term d n ->
+             (k : TyConKind) -> NContext (arity k) -> Term d (arity k + n) ->
+             {default Nat def : Term d n} ->
+             Elim d n
+typeCase1Y ty ret k ns body {def} =
   typeCase ty ret [(k ** SY ns body)] def
diff --git a/lib/Quox/Syntax/Term/Split.idr b/lib/Quox/Syntax/Term/Split.idr
index 36574b8..eafda5d 100644
--- a/lib/Quox/Syntax/Term/Split.idr
+++ b/lib/Quox/Syntax/Term/Split.idr
@@ -2,6 +2,7 @@ module Quox.Syntax.Term.Split
 
 import Quox.Syntax.Term.Base
 import Quox.Syntax.Term.Subst
+import Quox.Syntax.Term.Tighten
 import Quox.Context
 
 import public Quox.No
@@ -133,7 +134,7 @@ infixr 1 :\\
 public export
 absN : NContext m -> Term d (m + n) -> Term d n
 absN [<]       s = s
-absN (xs :< x) s = absN xs $ Lam $ SY [< x] s
+absN (xs :< x) s = absN xs $ Lam $ ST [< x] s
 
 public export %inline
 (:\\) : NContext m -> Term d (m + n) -> Term d n
@@ -144,7 +145,7 @@ infixr 1 :\\%
 public export
 dabsN : NContext m -> Term (m + d) n -> Term d n
 dabsN [<]       s = s
-dabsN (xs :< x) s = dabsN xs $ DLam $ SY [< x] s
+dabsN (xs :< x) s = dabsN xs $ DLam $ DST [< x] s
 
 public export %inline
 (:\\%) : NContext m -> Term (m + d) n -> Term d n
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 3444feb..71adddf 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -2,6 +2,7 @@ module Quox.Syntax.Term.Subst
 
 import Quox.No
 import Quox.Syntax.Term.Base
+import Quox.Syntax.Term.Tighten
 import Data.SnocVect
 
 %default total
@@ -320,6 +321,29 @@ mutual
       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) -> Elim d n
+CompHY {ty, p, q, val, r, zero, one} =
+  let ty' = SY ty.names $ ty.term // (B VZ ::: shift 2) in
+  Comp {
+    ty = dsub1 ty q, p, q,
+    val = E $ Coe ty p q val, r,
+    zero = SY zero.names $ E $ Coe ty' (B VZ) (weakD 1 q) zero.term,
+    one  = SY one.names  $ E $ Coe ty' (B VZ) (weakD 1 q) one.term
+  }
+
+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) ->
+         Elim d n
+CompH' {ty, p, q, val, r, zero, one} =
+  case dsqueeze ty of
+    S _ (N ty) => Comp   {ty, p, q, val, r, zero, one}
+    S _ (Y _)  => CompHY {ty, p, q, val, r, zero, one}
+
 ||| heterogeneous composition, using Comp and Coe (and subst)
 |||
 ||| comp [i ⇒ A] @p @q s { (r=0) j ⇒ t₀; (r=1) j ⇒ t₁ }
@@ -329,13 +353,11 @@ mutual
 |||   (r=1) j ⇒ coe [i ⇒ A] @j @q t₁
 ||| }
 public export %inline
-CompH : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
-        (r : Dim d) -> (zero, one : DScopeTerm d n) -> Elim d n
-CompH {ty, p, q, val, r, zero, one} =
-  let ty' = SY ty.names $ ty.term // (B VZ ::: shift 2) in
-  Comp {
-    ty = dsub1 ty q, p, q,
-    val = E $ Coe ty p q val, r,
-    zero = SY zero.names $ E $ Coe ty' (B VZ) (weakD 1 q) zero.term,
-    one  = SY one.names  $ E $ Coe ty' (B VZ) (weakD 1 q) one.term
-  }
+CompH : (i : BaseName) -> (ty : Term (S d) n) ->
+        (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
+        (j0 : BaseName) -> (zero : Term (S d) n) ->
+        (j1 : BaseName) -> (one : Term (S d) n) ->
+        Elim d n
+CompH {i, ty, p, q, val, r, j0, zero, j1, one} =
+  CompH' {ty = SY [< i] ty, p, q, val, r,
+          zero = SY [< j0] zero, one = SY [< j0] one}
diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr
new file mode 100644
index 0000000..415669b
--- /dev/null
+++ b/lib/Quox/Syntax/Term/Tighten.idr
@@ -0,0 +1,274 @@
+module Quox.Syntax.Term.Tighten
+
+import Quox.Syntax.Term.Base
+import Quox.Syntax.Subst
+import public Quox.OPE
+
+%default total
+
+
+export
+Tighten (Shift from) where
+  -- `OPE m n` is a spicy `m ≤ n`,
+  -- and `Shift from n` is a (different) spicy `from ≤ n`
+  -- so the value is `from ≤ m` (as a `Shift`), if that is the case
+  tighten _        SZ      = Nothing
+  tighten Id       by      = Just by
+  tighten (Drop p) (SS by) = tighten p by
+  tighten (Keep p) (SS by) = [|SS $ tighten p by|]
+
+
+export
+tightenSub : (forall m, n. OPE m n -> env n -> Maybe (env m)) ->
+             OPE to1 to2 -> Subst env from to2 -> Maybe (Subst env from to1)
+tightenSub f p (Shift by) = [|Shift $ tighten p by|]
+tightenSub f p (t ::: th) = [|f p t !::: tightenSub f p th|]
+
+export
+Tighten env => Tighten (Subst env from) where
+  tighten p th = tightenSub tighten p th
+
+
+export
+tightenScope : (forall m, n. OPE m n -> f n -> Maybe (f m)) ->
+               {s : Nat} -> OPE m n -> Scoped s f n -> Maybe (Scoped s f m)
+tightenScope f p (S names (Y body)) = SY names <$> f (keepN s p) body
+tightenScope f p (S names (N body)) = S names . N <$> f p body
+
+export
+tightenDScope : {0 f : Nat -> Nat -> Type} ->
+                (forall m, n, k. OPE m n -> f n k -> Maybe (f m k)) ->
+                OPE m n -> Scoped s (f n) k -> Maybe (Scoped s (f m) k)
+tightenDScope f p (S names (Y body)) = SY names <$> f p body
+tightenDScope f p (S names (N body)) = S names . N <$> f p body
+
+
+mutual
+  private
+  tightenT : OPE n1 n2 -> Term d n2 -> Maybe (Term d n1)
+  tightenT p (TYPE l) = pure $ TYPE l
+  tightenT p (Pi qty arg res) =
+    Pi qty <$> tightenT p arg <*> tightenS p res
+  tightenT p (Lam body) = Lam <$> tightenS p body
+  tightenT p (Sig fst snd) = Sig <$> tightenT p fst <*> tightenS p snd
+  tightenT p (Pair fst snd) = Pair <$> tightenT p fst <*> tightenT p snd
+  tightenT p (Enum cases) = pure $ Enum cases
+  tightenT p (Tag tag) = pure $ Tag tag
+  tightenT p (Eq ty l r) =
+    Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r
+  tightenT p (DLam body) = DLam <$> tightenDS p body
+  tightenT p Nat = pure Nat
+  tightenT p Zero = pure Zero
+  tightenT p (Succ s) = Succ <$> tightenT p s
+  tightenT p (BOX qty ty) = BOX qty <$> tightenT p ty
+  tightenT p (Box val) = Box <$> tightenT p val
+  tightenT p (E e) = assert_total $ E <$> tightenE p e
+  tightenT p (CloT tm th) = do
+    th <- assert_total $ tightenSub tightenE p th
+    pure $ CloT tm th
+  tightenT p (DCloT tm th) = [|DCloT (tightenT p tm) (pure th)|]
+
+  private
+  tightenE : OPE n1 n2 -> Elim d n2 -> Maybe (Elim d n1)
+  tightenE p (F x) = pure $ F x
+  tightenE p (B i) = [|B $ tighten p i|]
+  tightenE p (fun :@ arg) = [|tightenE p fun :@ tightenT p arg|]
+  tightenE p (CasePair qty pair ret body) =
+    CasePair qty <$> tightenE p pair
+                 <*> tightenS p ret
+                 <*> tightenS p body
+  tightenE p (CaseEnum qty tag ret arms) =
+    CaseEnum qty <$> tightenE p tag
+                 <*> tightenS p ret
+                 <*> traverse (tightenT p) arms
+  tightenE p (CaseNat qty qtyIH nat ret zero succ) =
+    CaseNat qty qtyIH
+      <$> tightenE p nat
+      <*> tightenS p ret
+      <*> tightenT p zero
+      <*> tightenS p succ
+  tightenE p (CaseBox qty box ret body) =
+    CaseBox qty <$> tightenE p box
+                <*> tightenS p ret
+                <*> tightenS p body
+  tightenE p (fun :% arg) = (:% arg) <$> tightenE p fun
+  tightenE p (tm :# ty) = [|tightenT p tm :# tightenT p ty|]
+  tightenE p (Coe ty q0 q1 val) =
+    Coe <$> tightenDS p ty
+        <*> pure q0 <*> pure q1
+        <*> tightenT p val
+  tightenE p (Comp ty q0 q1 val r zero one) =
+    Comp <$> tightenT p ty
+         <*> pure q0 <*> pure q1
+         <*> tightenT p val
+         <*> pure r
+         <*> tightenDS p zero
+         <*> tightenDS p one
+  tightenE p (TypeCase ty ret arms def) =
+    TypeCase <$> tightenE p ty
+             <*> tightenT p ret
+             <*> traverse (tightenS p) arms
+             <*> tightenT p def
+  tightenE p (CloE el th) = do
+    th <- assert_total $ tightenSub tightenE p th
+    pure $ CloE el th
+  tightenE p (DCloE el th) = [|DCloE (tightenE p el) (pure th)|]
+
+  export
+  tightenS : {s : Nat} -> OPE m n ->
+             ScopeTermN s f n -> Maybe (ScopeTermN s f m)
+  tightenS = assert_total $ tightenScope tightenT
+
+  export
+  tightenDS : OPE m n -> DScopeTermN s f n -> Maybe (DScopeTermN s f m)
+  tightenDS = assert_total $ tightenDScope tightenT {f = \n, d => Term d n}
+
+export Tighten (Elim d) where tighten p e = tightenE p e
+export Tighten (Term d) where tighten p t = tightenT p t
+
+export
+Tighten Dim where
+  tighten p (K e) = pure $ K e
+  tighten p (B i) = B <$> tighten p i
+
+
+mutual
+  export
+  dtightenT : OPE d1 d2 -> Term d2 n -> Maybe (Term d1 n)
+  dtightenT p (TYPE l) = pure $ TYPE l
+  dtightenT p (Pi qty arg res) =
+    Pi qty <$> dtightenT p arg <*> dtightenS p res
+  dtightenT p (Lam body) =
+    Lam <$> dtightenS p body
+  dtightenT p (Sig fst snd) =
+    Sig <$> dtightenT p fst <*> dtightenS p snd
+  dtightenT p (Pair fst snd) =
+    Pair <$> dtightenT p fst <*> dtightenT p snd
+  dtightenT p (Enum cases) = pure $ Enum cases
+  dtightenT p (Tag tag) = pure $ Tag tag
+  dtightenT p (Eq ty l r) =
+    Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r
+  dtightenT p (DLam body) = DLam <$> dtightenDS p body
+  dtightenT p Nat = pure Nat
+  dtightenT p Zero = pure Zero
+  dtightenT p (Succ s) = Succ <$> dtightenT p s
+  dtightenT p (BOX qty ty) = BOX qty <$> dtightenT p ty
+  dtightenT p (Box val) = Box <$> dtightenT p val
+  dtightenT p (E e) = assert_total $ E <$> dtightenE p e
+  dtightenT p (CloT tm th) = do
+    tm <- dtightenT p tm
+    th <- assert_total $ traverse (dtightenE p) th
+    pure $ CloT tm th
+  dtightenT p (DCloT tm th) = do th <- tighten p th; pure $ DCloT tm th
+
+  export
+  dtightenE : OPE d1 d2 -> Elim d2 n -> Maybe (Elim d1 n)
+  dtightenE p (F x) = pure $ F x
+  dtightenE p (B i) = pure $ B i
+  dtightenE p (fun :@ arg) = [|dtightenE p fun :@ dtightenT p arg|]
+  dtightenE p (CasePair qty pair ret body) =
+    CasePair qty <$> dtightenE p pair
+                 <*> dtightenS p ret
+                 <*> dtightenS p body
+  dtightenE p (CaseEnum qty tag ret arms) =
+    CaseEnum qty <$> dtightenE p tag
+                 <*> dtightenS p ret
+                 <*> traverse (dtightenT p) arms
+  dtightenE p (CaseNat qty qtyIH nat ret zero succ) =
+    CaseNat qty qtyIH
+      <$> dtightenE p nat
+      <*> dtightenS p ret
+      <*> dtightenT p zero
+      <*> dtightenS p succ
+  dtightenE p (CaseBox qty box ret body) =
+    CaseBox qty <$> dtightenE p box
+                <*> dtightenS p ret
+                <*> dtightenS p body
+  dtightenE p (fun :% arg) = [|dtightenE p fun :% tighten p arg|]
+  dtightenE p (tm :# ty) = [|dtightenT p tm :# dtightenT p ty|]
+  dtightenE p (Coe ty q0 q1 val) =
+    [|Coe (dtightenDS p ty) (tighten p q0) (tighten p q1) (dtightenT p val)|]
+  dtightenE p (Comp ty q0 q1 val r zero one) =
+    [|Comp (dtightenT p ty) (tighten p q0) (tighten p q1)
+           (dtightenT p val) (tighten p r)
+           (dtightenDS p zero) (dtightenDS p one)|]
+  dtightenE p (TypeCase ty ret arms def) =
+    [|TypeCase (dtightenE p ty) (dtightenT p ret)
+               (traverse (dtightenS p) arms) (dtightenT p def)|]
+  dtightenE p (CloE el th) = do
+    el <- dtightenE p el
+    th <- assert_total $ traverse (dtightenE p) th
+    pure $ CloE el th
+  dtightenE p (DCloE el th) = do
+    th <- tighten p th
+    pure $ DCloE el th
+
+  export
+  dtightenS : OPE d1 d2 -> ScopeTermN s d2 n -> Maybe (ScopeTermN s d1 n)
+  dtightenS = assert_total $ tightenDScope dtightenT {f = Term}
+
+  export
+  dtightenDS : {s : Nat} -> OPE d1 d2 ->
+               DScopeTermN s d2 n -> Maybe (DScopeTermN s d1 n)
+  dtightenDS = assert_total $ tightenScope dtightenT
+
+
+export [TermD] Tighten (\d => Term d n) where tighten p t = dtightenT p t
+export [ElimD] Tighten (\d => Elim d n) where tighten p e = dtightenE p e
+
+
+-- versions of SY, etc, that try to tighten and use SN automatically
+
+public export
+ST : Tighten f => {s : Nat} -> NContext s -> f (s + n) -> Scoped s f n
+ST names body =
+  case tightenN s body of
+    Just body => S names $ N body
+    Nothing   => S names $ Y body
+
+public export
+DST : {s : Nat} -> NContext s -> Term (s + d) n -> DScopeTermN s d n
+DST names body =
+  case tightenN @{TermD} s body of
+    Just body => S names $ N body
+    Nothing   => S names $ Y body
+
+public export %inline
+PiT : (qty : Qty) -> (x : BaseName) ->
+      (arg : Term d n) -> (res : Term d (S n)) -> Term d n
+PiT {qty, x, arg, res} = Pi {qty, arg, res = ST [< x] res}
+
+public export %inline
+SigT : (x : BaseName) -> (fst : Term d n) ->
+       (snd : Term d (S n)) -> Term d n
+SigT {x, fst, snd} = Sig {fst, snd = ST [< x] snd}
+
+public export %inline
+EqT : (i : BaseName) -> (ty : Term (S d) n) ->
+      (l, r : Term d n) -> Term d n
+EqT {i, ty, l, r} = Eq {ty = DST [< i] ty, l, r}
+
+public export %inline
+CoeT : (i : BaseName) -> (ty : Term (S d) n) ->
+       (p, q : Dim d) -> (val : Term d n) -> Elim d n
+CoeT {i, ty, p, q, val} = Coe {ty = DST [< i] ty, p, q, val}
+
+public export %inline
+typeCase1T : Elim d n -> Term d n ->
+             (k : TyConKind) -> NContext (arity k) -> Term d (arity k + n) ->
+             {default Nat def : Term d n} ->
+             Elim d n
+typeCase1T ty ret k ns body {def} =
+  typeCase ty ret [(k ** ST ns body)] def
+
+
+export
+squeeze : {s : Nat} -> ScopeTermN s d n -> ScopeTermN s d n
+squeeze (S names (Y body)) = S names $ maybe (Y body) N $ tightenN s body
+squeeze (S names (N body)) = S names $ N body
+
+export
+dsqueeze : {s : Nat} -> DScopeTermN s d n -> DScopeTermN s d n
+dsqueeze (S names (Y body)) =
+  S names $ maybe (Y body) N $ tightenN s body @{TermD}
+dsqueeze (S names (N body)) = S names $ N body
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index cdff3ff..137c952 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -2,10 +2,11 @@ module Quox.Syntax.Var
 
 import Quox.Name
 import Quox.Pretty
--- import Quox.OPE
+import Quox.OPE
 
 import Data.Nat
 import Data.List
+import Data.Vect
 import public Quox.Decidable
 import Data.Bool.Decidable
 import Data.DPair
@@ -151,6 +152,16 @@ interface FromVar f where %inline fromVar : Var n -> f n
 
 public export FromVar Var where fromVar = id
 
+export
+tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
+            (n : Nat) -> Vect n (tm n)
+tabulateV f 0     = []
+tabulateV f (S n) = f VZ :: tabulateV (f . VS) n
+
+export
+allVars : (n : Nat) -> Vect n (Var n)
+allVars n = tabulateV id n
+
 
 public export
 data LT : Rel (Var n) where
@@ -287,3 +298,12 @@ decEqFromBool i j =
 %transform "Var.decEq" varDecEq = decEqFromBool
 
 public export %inline DecEq (Var n) where decEq = varDecEq
+
+
+export
+Tighten Var where
+  tighten Id       i      = Just i
+  tighten (Drop p) VZ     = Nothing
+  tighten (Drop p) (VS i) = tighten p i
+  tighten (Keep p) VZ     = Just VZ
+  tighten (Keep p) (VS i) = VS <$> tighten p i
diff --git a/lib/on-hold/Quox/OPE.idr b/lib/on-hold/Quox/OPE.idr
deleted file mode 100644
index 0f50df0..0000000
--- a/lib/on-hold/Quox/OPE.idr
+++ /dev/null
@@ -1,196 +0,0 @@
-||| "order preserving embeddings", for recording a correspondence between
-||| a smaller scope and part of a larger one.
-module Quox.OPE
-
-import Quox.NatExtra
-
-import Data.Nat
-
-%default total
-
-
-public export
-data OPE : Nat -> Nat -> Type where
-  Id   : OPE n n
-  Drop : OPE m n -> OPE m     (S n)
-  Keep : OPE m n -> OPE (S m) (S n)
-%name OPE p, q
-
-public export %inline Injective Drop where injective Refl = Refl
-public export %inline Injective Keep where injective Refl = Refl
-
-public export
-opeZero : {n : Nat} -> OPE 0 n
-opeZero {n = 0}   = Id
-opeZero {n = S n} = Drop opeZero
-
-public export
-(.) : OPE m n -> OPE n p -> OPE m p
-p      . Id     = p
-Id     . q      = q
-p      . Drop q = Drop $ p . q
-Drop p . Keep q = Drop $ p . q
-Keep p . Keep q = Keep $ p . q
-
-public export
-toLTE : {m : Nat} -> OPE m n -> m `LTE` n
-toLTE Id       = reflexive
-toLTE (Drop p) = lteSuccRight $ toLTE p
-toLTE (Keep p) = LTESucc      $ toLTE p
-
-
-public export
-dropInner' : LTE' m n -> OPE m n
-dropInner' LTERefl      = Id
-dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
-
-public export
-dropInner : {n : Nat} -> LTE m n -> OPE m n
-dropInner = dropInner' . fromLte
-
-public export
-dropInnerN : (m : Nat) -> OPE n (m + n)
-dropInnerN 0     = Id
-dropInnerN (S m) = Drop $ dropInnerN m
-
-
-public export
-interface Tighten t where
-  tighten : Alternative f => OPE m n -> t n -> f (t m)
-
-parameters {auto _ : Tighten t} {auto _ : Alternative f}
-  export
-  tightenInner : {n : Nat} -> m `LTE` n -> t n -> f (t m)
-  tightenInner = tighten . dropInner
-
-  export
-  tightenN : (m : Nat) -> t (m + n) -> f (t n)
-  tightenN m = tighten $ dropInnerN m
-
-  export
-  tighten1 : t (S n) -> f (t n)
-  tighten1 = tightenN 1
-
-
-
--- [todo] can this be done with fancy nats too?
--- with bitmasks sure but that might not be worth the effort
--- [the next day] it probably isn't
-
--- public export
--- data OPE' : Nat -> Nat -> Type where
---   None : OPE' 0 0
---   Drop : OPE' m n -> OPE' m (S n)
---   Keep : OPE' m n -> OPE' (S m) (S n)
--- %name OPE' q
-
-
--- public export %inline
--- drop' : Integer -> Integer
--- drop' n = n * 2
-
--- public export %inline
--- keep' : Integer -> Integer
--- keep' n = 1 + 2 * n
-
--- public export
--- data IsOPE : Integer -> (OPE' m n) -> Type where
---   IsNone : 0 `IsOPE` None
---   IsDrop : (0 _ : m `IsOPE` q) -> drop' m `IsOPE` Drop q
---   IsKeep : (0 _ : m `IsOPE` q) -> keep' m `IsOPE` Keep q
--- %name IsOPE p
-
-
--- public export
--- record OPE m n where
---   constructor MkOPE
---   value  : Integer
---   0 spec : OPE' m n
---   0 prf  : value `IsOPE` spec
---   0 pos  : So (value >= 0)
-
-
--- private
--- 0 idrisPleaseLearnAboutIntegers : {x, y : Integer} -> x = y
--- idrisPleaseLearnAboutIntegers {x, y} = believe_me $ Refl {x}
-
--- private
--- 0 natIntPlus : (m, n : Nat) ->
---                natToInteger (m + n) = natToInteger m + natToInteger n
--- natIntPlus m n = idrisPleaseLearnAboutIntegers
-
--- private
--- 0 shiftTwice : (x : Integer) -> (m, n : Nat) ->
---                x `shiftL` (m + n) = (x `shiftL` m) `shiftL` n
--- shiftTwice x m n = idrisPleaseLearnAboutIntegers
-
--- private
--- 0 shift1 : (x : Integer) -> (x `shiftL` 1) = 2 * x
--- shift1 x = idrisPleaseLearnAboutIntegers
-
--- private
--- 0 intPlusComm : (x, y : Integer) -> (x + y) = (y + x)
--- intPlusComm x y = idrisPleaseLearnAboutIntegers
-
--- private
--- 0 intTimes2Minus1 : (x : Integer) -> 2 * x - 1 = 2 * (x - 1) + 1
--- intTimes2Minus1 x = idrisPleaseLearnAboutIntegers
-
--- private
--- 0 intPosShift : So (x > 0) -> So (x `shiftL` i > 0)
--- intPosShift p = believe_me Oh
-
--- private
--- 0 intNonnegDec : {x : Integer} -> So (x > 0) -> So (x - 1 >= 0)
--- intNonnegDec p = believe_me Oh
-
-
--- private
--- 0 shiftSucc : (x : Integer) -> (n : Nat) ->
---               x `shiftL` S n = 2 * (x `shiftL` n)
--- shiftSucc x n = Calc $
---   |~  x `shiftL` S n
---   ~~  x `shiftL` (n + 1)
---         ...(cong (x `shiftL`) $ sym $ plusCommutative {})
---   ~~  (x `shiftL` n) `shiftL` 1
---         ...(shiftTwice {})
---   ~~  2 * (x `shiftL` n)
---         ...(shift1 {})
-
-
--- private
--- opeIdVal : (n : Nat) -> Integer
--- opeIdVal n = (1 `shiftL` n) - 1
-
--- private
--- 0 opeIdValSpec : (n : Nat) -> Integer
--- opeIdValSpec 0     = 0
--- opeIdValSpec (S n) = keep' $ opeIdValSpec n
-
--- private
--- 0 opeIdValOk :  (n : Nat) -> opeIdVal n = opeIdValSpec n
--- opeIdValOk 0     = Refl
--- opeIdValOk (S n) = Calc $
---   |~  (1 `shiftL` S n) - 1
---   ~~  2 * (1 `shiftL` n) - 1      ...(cong (\x => x - 1) $ shiftSucc {})
---   ~~  2 * (1 `shiftL` n - 1) + 1  ...(intTimes2Minus1 {})
---   ~~  1 + 2 * (1 `shiftL` n - 1)  ...(intPlusComm {})
---   ~~  1 + 2 * opeIdValSpec n      ...(cong (\x => 1 + 2 * x) $ opeIdValOk {})
-
--- private
--- 0 opeIdSpec : (n : Nat) -> OPE' n n
--- opeIdSpec 0     = None
--- opeIdSpec (S n) = Keep $ opeIdSpec n
-
--- private
--- 0 opeIdProof' : (n : Nat) -> opeIdValSpec n `IsOPE` opeIdSpec n
--- opeIdProof' 0     = IsNone
--- opeIdProof' (S n) = IsKeep (opeIdProof' n)
-
--- private
--- 0 opeIdProof : (n : Nat) -> opeIdVal n `IsOPE` opeIdSpec n
--- opeIdProof n = rewrite opeIdValOk n in opeIdProof' n
-
--- export
--- opeId : {n : Nat} -> OPE n n
--- opeId {n} = MkOPE {prf = opeIdProof n, pos = intNonnegDec $ intPosShift Oh, _}
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 82c52db..d9574e1 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -10,9 +10,11 @@ depends = base, contrib, elab-util, sop, snocvect, eff
 modules =
   Quox.BoolExtra,
   Quox.CharExtra,
+  Quox.NatExtra,
   Quox.EffExtra,
   Quox.Decidable,
   Quox.No,
+  Quox.OPE,
   Quox.Pretty,
   Quox.Syntax,
   Quox.Syntax.Dim,
@@ -23,6 +25,7 @@ modules =
   Quox.Syntax.Term,
   Quox.Syntax.Term.TyConKind,
   Quox.Syntax.Term.Base,
+  Quox.Syntax.Term.Tighten,
   Quox.Syntax.Term.Pretty,
   Quox.Syntax.Term.Split,
   Quox.Syntax.Term.Subst,
diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr
index dc01e78..3d8c921 100644
--- a/tests/Tests/PrettyTerm.idr
+++ b/tests/Tests/PrettyTerm.idr
@@ -70,11 +70,11 @@ tests = "pretty printing terms" :- [
   "function types" :- [
     testPrettyT [<] [<] (Arr One (FT "A") (FT "B")) "1.A → B" "1.A -> B",
     testPrettyT [<] [<]
-      (Pi_ One "x" (FT "A") (E $ F "B" :@ BVT 0))
+      (PiY One "x" (FT "A") (E $ F "B" :@ BVT 0))
       "1.(x : A) → B x"
       "1.(x : A) -> B x",
     testPrettyT [<] [<]
-      (Pi_ Zero "A" (TYPE 0) $ Arr Any (BVT 0) (BVT 0))
+      (PiY Zero "A" (TYPE 0) $ Arr Any (BVT 0) (BVT 0))
       "0.(A : ★₀) → ω.A → A"
       "0.(A : Type0) -> #.A -> A",
     testPrettyT [<] [<]
@@ -86,7 +86,7 @@ tests = "pretty printing terms" :- [
       "ω.A → ω.A → A"
       "#.A -> #.A -> A",
     testPrettyT [<] [<]
-      (Pi_ Zero "P" (Arr Zero (FT "A") (TYPE 0)) (E $ BV 0 :@ FT "a"))
+      (PiY Zero "P" (Arr Zero (FT "A") (TYPE 0)) (E $ BV 0 :@ FT "a"))
       "0.(P : 0.A → ★₀) → P a"
       "0.(P : 0.A -> Type0) -> P a"
   ],
@@ -94,12 +94,12 @@ tests = "pretty printing terms" :- [
   "pair types" :- [
     testPrettyT [<] [<] (FT "A" `And` FT "B") "A × B" "A ** B",
     testPrettyT [<] [<]
-      (Sig_ "x" (FT "A") (E $ F "B" :@ BVT 0))
+      (SigY "x" (FT "A") (E $ F "B" :@ BVT 0))
       "(x : A) × B x"
       "(x : A) ** B x",
     testPrettyT [<] [<]
-      (Sig_ "x" (FT "A") $
-       Sig_ "y" (E $ F "B" :@ BVT 0) $
+      (SigY "x" (FT "A") $
+       SigY "y" (E $ F "B" :@ BVT 0) $
        E $ F "C" :@@ [BVT 1, BVT 0])
       "(x : A) × (y : B x) × C x y"
       "(x : A) ** (y : B x) ** C x y",
diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr
index b7c0425..7daa180 100644
--- a/tests/Tests/Typechecker.idr
+++ b/tests/Tests/Typechecker.idr
@@ -33,8 +33,8 @@ inj = rethrow . mapFst TCError <=< lift . runExcept
 
 reflTy : Term d n
 reflTy =
-  Pi_ Zero "A" (TYPE 0) $
-  Pi_ One  "x" (BVT 0)  $
+  PiY Zero "A" (TYPE 0) $
+  PiY One  "x" (BVT 0)  $
   Eq0 (BVT 1) (BVT 0) (BVT 0)
 
 reflDef : Term d n
@@ -43,9 +43,9 @@ reflDef = [< "A","x"] :\\ [< "i"] :\\% BVT 0
 
 fstTy : Term d n
 fstTy =
-  (Pi_ Zero "A" (TYPE 1) $
-   Pi_ Zero "B" (Arr Any (BVT 0) (TYPE 1)) $
-   Arr Any (Sig_ "x" (BVT 1) $ E $ BV 1 :@ BVT 0) (BVT 1))
+  (PiY Zero "A" (TYPE 1) $
+   PiY Zero "B" (Arr Any (BVT 0) (TYPE 1)) $
+   Arr Any (SigY "x" (BVT 1) $ E $ BV 1 :@ BVT 0) (BVT 1))
 
 fstDef : Term d n
 fstDef =
@@ -54,9 +54,9 @@ fstDef =
 
 sndTy : Term d n
 sndTy =
-  (Pi_ Zero "A" (TYPE 1) $
-   Pi_ Zero "B" (Arr Any (BVT 0) (TYPE 1)) $
-   Pi_ Any  "p" (Sig_ "x" (BVT 1) $ E $ BV 1 :@ BVT 0) $
+  (PiY Zero "A" (TYPE 1) $
+   PiY Zero "B" (Arr Any (BVT 0) (TYPE 1)) $
+   PiY Any  "p" (SigY "x" (BVT 1) $ E $ BV 1 :@ BVT 0) $
    E (BV 1 :@ E (F "fst" :@@ [BVT 2, BVT 1, BVT 0])))
 
 sndDef : Term d n
@@ -80,8 +80,8 @@ defGlobals = fromList
    ("f",  mkPostulate gany  $ Arr One (FT "A") (FT "A")),
    ("g",  mkPostulate gany  $ Arr One (FT "A") (FT "B")),
    ("f2", mkPostulate gany  $ Arr One (FT "A") $ Arr One (FT "A") (FT "B")),
-   ("p",  mkPostulate gany  $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
-   ("q",  mkPostulate gany  $ Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0),
+   ("p",  mkPostulate gany  $ PiY One "x" (FT "A") $ E $ F "P" :@ BVT 0),
+   ("q",  mkPostulate gany  $ PiY One "x" (FT "A") $ E $ F "P" :@ BVT 0),
    ("refl", mkDef gany reflTy reflDef),
    ("fst",  mkDef gany fstTy fstDef),
    ("snd",  mkDef gany sndTy sndDef)]
@@ -185,7 +185,7 @@ tests = "typechecker" :- [
       check_ empty szero (Arr One (FT "C") (FT "D")) (TYPE 0),
     testTC "0 · (1·x : A) → P x ⇐ ★₀" $
       check_ empty szero
-        (Pi_ One "x" (FT "A") $ E $ F "P" :@ BVT 0)
+        (PiY One "x" (FT "A") $ E $ F "P" :@ BVT 0)
         (TYPE 0),
     testTCFail "0 · A ⊸ P ⇍ ★₀" $
       check_ empty szero (Arr One (FT "A") $ FT "P") (TYPE 0),
@@ -201,14 +201,14 @@ tests = "typechecker" :- [
       check_ empty szero (FT "A" `And` FT "P") (TYPE 0),
     testTC "0 · (x : A) × P x ⇐ ★₀" $
       check_ empty szero
-        (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0),
+        (SigY "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 0),
     testTC "0 · (x : A) × P x ⇐ ★₁" $
       check_ empty szero
-        (Sig_ "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1),
+        (SigY "x" (FT "A") $ E $ F "P" :@ BVT 0) (TYPE 1),
     testTC "0 · (A : ★₀) × A ⇐ ★₁" $
-      check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 1),
+      check_ empty szero (SigY "A" (TYPE 0) $ BVT 0) (TYPE 1),
     testTCFail "0 · (A : ★₀) × A ⇍ ★₀" $
-      check_ empty szero (Sig_ "A" (TYPE 0) $ BVT 0) (TYPE 0),
+      check_ empty szero (SigY "A" (TYPE 0) $ BVT 0) (TYPE 0),
     testTCFail "1 · A × A ⇍ ★₀" $
       check_ empty sone (FT "A" `And` FT "A") (TYPE 0)
   ],
@@ -282,7 +282,7 @@ tests = "typechecker" :- [
     testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
       check_ empty sone
         (Pair (FT "a") ([< "i"] :\\% FT "a"))
-        (Sig_ "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
+        (SigY "x" (FT "A") $ Eq0 (FT "A") (BVT 0) (FT "a"))
   ],
 
   "unpairing" :- [
@@ -334,7 +334,7 @@ tests = "typechecker" :- [
     testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
       inferAs empty szero
         (F "snd" :@@ [TYPE 0, [< "x"] :\\ BVT 0])
-        (Pi_ Any "A" (Sig_ "A" (TYPE 0) $ BVT 0) $
+        (PiY Any "A" (SigY "A" (TYPE 0) $ BVT 0) $
                 (E $ F "fst" :@@ [TYPE 0, [< "x"] :\\ BVT 0, BVT 0]))
   ],
 
@@ -395,14 +395,14 @@ tests = "typechecker" :- [
     testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
       check_ empty szero
         ([< "p","q"] :\\ [< "i"] :\\% BVT 1)
-        (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
-         Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
+        (PiY Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
+         PiY Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
          Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
     testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
       check_ empty szero
         ([< "p","q"] :\\ [< "i"] :\\% BVT 0)
-        (Pi_ Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
-         Pi_ Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
+        (PiY Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $
+         PiY Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $
          Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
   ],
 
@@ -463,10 +463,10 @@ tests = "typechecker" :- [
     testTC "cong" $
       check_ empty sone
         ([< "x", "y", "xy"] :\\ [< "i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
-        (Pi_ Zero "x"  (FT "A") $
-         Pi_ Zero "y"  (FT "A") $
-         Pi_ One  "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $
-         Eq_ "i" (E $ F "P" :@ E (BV 0 :% BV 0))
+        (PiY Zero "x"  (FT "A") $
+         PiY Zero "y"  (FT "A") $
+         PiY One  "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $
+         EqY "i" (E $ F "P" :@ E (BV 0 :% BV 0))
              (E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
     note "0·A : Type, 0·P : ω·A → Type,",
     note "ω·p q : (1·x : A) → P x",
@@ -476,11 +476,11 @@ tests = "typechecker" :- [
     testTC "funext" $
       check_ empty sone
         ([< "eq"] :\\ [< "i"] :\\% [< "x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
-        (Pi_ One "eq"
-          (Pi_ One "x" (FT "A")
+        (PiY One "eq"
+          (PiY One "x" (FT "A")
             (Eq0 (E $ F "P" :@ BVT 0)
                  (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)))
-          (Eq0 (Pi_ Any "x" (FT "A") $ E $ F "P" :@ BVT 0) (FT "p") (FT "q"))),
+          (Eq0 (PiY Any "x" (FT "A") $ E $ F "P" :@ BVT 0) (FT "p") (FT "q"))),
     todo "absurd (when coerce is in)"
     -- absurd : (`true ≡ `false : {true, false}) ⇾ (0·A : ★₀) → A ≔
     --   λ e ⇒