Use CoDebruijn syntax at top level.

8 files changed, 392 insertions, 235 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index df84fda..2456685 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -15,3 +15,4 @@ modules
   , Total.Reduction
   , Total.Syntax
   , Total.Term
+  , Total.Term.CoDebruijn
diff --git a/src/Thinning.idr b/src/Thinning.idr
index f9e76b5..70165d0 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -26,24 +26,16 @@ data Len : SnocList a -> Type where
 %name Len k, m, n
 
 %hint
-export
+public export
 length : (sx : SnocList a) -> Len sx
 length [<] = Z
 length (sx :< x) = S (length sx)
 
 %hint
 export
-lenSrc : sx `Thins` sy -> Len sx
-lenSrc Empty = Z
-lenSrc (Drop thin) = lenSrc thin
-lenSrc (Keep thin) = S (lenSrc thin)
-
-%hint
-export
-lenTgt : sx `Thins` sy -> Len sy
-lenTgt Empty = Z
-lenTgt (Drop thin) = S (lenTgt thin)
-lenTgt (Keep thin) = S (lenTgt thin)
+lenAppend : Len sx -> Len sy -> Len (sx ++ sy)
+lenAppend k Z = k
+lenAppend k (S m) = S (lenAppend k m)
 
 %hint
 export
@@ -101,6 +93,7 @@ data Triangle : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz -> Type where
   KeepDrop : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Drop thin1) (Drop thin)
   KeepKeep : Triangle thin2 thin1 thin -> Triangle (Keep thin2) (Keep thin1) (Keep thin)
 
+public export
 data Overlap = Covers | Partitions
 
 namespace Covering
@@ -190,10 +183,9 @@ export
 map : (forall ctx. t ctx -> u ctx) -> Thinned t ctx -> Thinned u ctx
 map f (value `Over` thin) = f value `Over` thin
 
-%hint
 export
-thinnedLen : Thinned t sx -> Len sx
-thinnedLen (value `Over` thin) = lenTgt thin
+drop : Thinned t ctx -> Thinned t (ctx :< ty)
+drop (value `Over` thin) = value `Over` Drop thin
 
 -- Properties ------------------------------------------------------------------
 
diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr
index 1a848c0..f56d1bc 100644
--- a/src/Total/Encoded/Util.idr
+++ b/src/Total/Encoded/Util.idr
@@ -14,22 +14,22 @@ namespace Bool
   B = N
 
   export
-  True : Term ctx B
-  True = Zero
+  true : FullTerm B [<]
+  true = zero
 
   export
-  False : Term ctx B
-  False = Suc Zero
+  false : FullTerm B [<]
+  false = suc zero
 
   export
-  If : Len ctx => Term ctx B -> Term ctx ty -> Term ctx ty -> Term ctx ty
-  If t u v = Rec t u (Abs $ wkn v (Drop id))
+  if' : FullTerm (B ~> ty ~> ty ~> ty) [<]
+  if' = abs' (S $ S $ S Z) (\b, t, f => rec b t (abs $ drop f))
 
 namespace Arb
   export
-  arb : {ty : Ty} -> Term [<] ty
-  arb {ty = N} = Zero
-  arb {ty = ty ~> ty'} = Abs (lift arb)
+  arb : {ty : Ty} -> FullTerm ty [<]
+  arb {ty = N} = zero
+  arb {ty = ty ~> ty'} = abs (lift arb)
 
 namespace Union
   export
@@ -40,33 +40,34 @@ namespace Union
   (t ~> t') <+> (u ~> u') = (t <+> u) ~> (t' <+> u')
 
   export
-  injL : {t, u : Ty} -> Term [<] (t ~> (t <+> u))
+  swap : {t, u : Ty} -> FullTerm ((t <+> u) ~> (u <+> t)) [<]
+  swap {t = N, u = N} = id
+  swap {t = N, u = u ~> u'} = id
+  swap {t = t ~> t', u = N} = id
+  swap {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop swap . f . drop swap)
+
+  export
+  injL : {t, u : Ty} -> FullTerm (t ~> (t <+> u)) [<]
   export
-  injR : {t, u : Ty} -> Term [<] (u ~> (t <+> u))
+  injR : {t, u : Ty} -> FullTerm (u ~> (t <+> u)) [<]
   export
-  prjL : {t, u : Ty} -> Term [<] ((t <+> u) ~> t)
+  prjL : {t, u : Ty} -> FullTerm ((t <+> u) ~> t) [<]
   export
-  prjR : {t, u : Ty} -> Term [<] ((t <+> u) ~> u)
+  prjR : {t, u : Ty} -> FullTerm ((t <+> u) ~> u) [<]
 
-  injL {t = N, u = N} = Abs' (S Z) id
-  injL {t = N, u = u ~> u'} = Abs' (S $ S Z) (\n, _ => App (lift (prjR . injL)) n)
-  injL {t = t ~> t', u = N} = Abs' (S Z) id
-  injL {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift injL . f . lift prjL)
+  injL {t = N, u = N} = id
+  injL {t = N, u = u ~> u'} = abs' (S $ S Z) (\n, _ => app (lift (prjR . injL)) n)
+  injL {t = t ~> t', u = N} = id
+  injL {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop injL . f . drop prjL)
 
-  injR {t = N, u = N} = Abs' (S Z) id
-  injR {t = N, u = u ~> u'} = Abs' (S Z) id
-  injR {t = t ~> t', u = N} = Abs' (S $ S Z) (\n, _ => App (lift (prjL . injR)) n)
-  injR {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift injR . f . lift prjR)
+  injR = swap . injL
 
-  prjL {t = N, u = N} = Abs' (S Z) id
-  prjL {t = N, u = u ~> u'} = Abs' (S Z) (\f => App (lift (prjL . injR) . f) (lift $ arb))
-  prjL {t = t ~> t', u = N} = Abs' (S Z) id
-  prjL {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift prjL . f . lift injL)
+  prjL {t = N, u = N} = id
+  prjL {t = N, u = u ~> u'} = abs' (S Z) (\f => app (drop (prjL . injR) . f) (drop arb))
+  prjL {t = t ~> t', u = N} = id
+  prjL {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop prjL . f . drop injL)
 
-  prjR {t = N, u = N} = Abs' (S Z) id
-  prjR {t = N, u = u ~> u'} = Abs' (S Z) id
-  prjR {t = t ~> t', u = N} = Abs' (S Z) (\f => App (lift (prjR . injL) . f) (lift $ arb))
-  prjR {t = t ~> t', u = u ~> u'} = Abs' (S Z) (\f => lift prjR . f . lift injR)
+  prjR = prjL . swap
 
 namespace Unit
   export
@@ -79,33 +80,33 @@ namespace Pair
   t * u = B ~> (t <+> u)
 
   export
-  pair : {t, u : Ty} -> Term [<] (t ~> u ~> (t * u))
-  pair = Abs' (S $ S $ S Z)
-    (\fst, snd, b => If b (App (lift injL) fst) (App (lift injR) snd))
+  pair : {t, u : Ty} -> FullTerm (t ~> u ~> (t * u)) [<]
+  pair = abs' (S $ S $ S Z)
+    (\fst, snd, b => app' (lift if') [<b, app (lift injL) fst, app (lift injR) snd])
 
   export
-  fst : {t, u : Ty} -> Term [<] ((t * u) ~> t)
-  fst = Abs' (S Z) (\p => App (lift prjL . p) True)
+  fst : {t, u : Ty} -> FullTerm ((t * u) ~> t) [<]
+  fst = abs' (S Z) (\p => app (drop prjL . p) (drop true))
 
   export
-  snd : {t, u : Ty} -> Term [<] ((t * u) ~> u)
-  snd = Abs' (S Z) (\p => App (lift prjR . p) False)
+  snd : {t, u : Ty} -> FullTerm ((t * u) ~> u) [<]
+  snd = abs' (S Z) (\p => app (drop prjR . p) (drop false))
 
   export
-  mapSnd : {t, u, v : Ty} -> Term [<] ((u ~> v) ~> (t * u) ~> (t * v))
-  mapSnd = Abs' (S $ S Z) (\f, p => App' (lift pair) [<App (lift fst) p , App (f . lift snd) p])
+  mapSnd : {t, u, v : Ty} -> FullTerm ((u ~> v) ~> (t * u) ~> (t * v)) [<]
+  mapSnd = abs' (S $ S Z) (\f, p => app' (lift pair) [<app (lift fst) p , app (f . lift snd) p])
 
   export
   Product : SnocList Ty -> Ty
   Product = foldl (*) Unit
 
   export
-  pair' : {tys : SnocList Ty} -> Term [<] (tys ~>* Product tys)
+  pair' : {tys : SnocList Ty} -> FullTerm (tys ~>* Product tys) [<]
   pair' {tys = [<]} = arb
-  pair' {tys = tys :< ty} = Abs' (S $ S Z) (\p, t => App' (lift pair) [<p, t]) .* pair' {tys}
+  pair' {tys = tys :< ty} = abs' (S $ S Z) (\p, t => app' (lift pair) [<p, t]) .* pair'
 
   export
-  project : {tys : SnocList Ty} -> Elem ty tys -> Term [<] (Product tys ~> ty)
+  project : {tys : SnocList Ty} -> Elem ty tys -> FullTerm (Product tys ~> ty) [<]
   project {tys = tys :< ty} Here = snd
   project {tys = tys :< ty} (There i) = project i . fst
 
@@ -113,15 +114,15 @@ namespace Pair
   mapProd :
     {ctx, tys, tys' : SnocList Ty} ->
     {auto 0 prf : SnocList.length tys = SnocList.length tys'} ->
-    All (Term ctx) (zipWith (~>) tys tys') ->
-    Term ctx (Product tys ~> Product tys')
-  mapProd {tys = [<], tys' = [<]} [<] = Abs (Var Here)
+    All (flip FullTerm ctx) (zipWith (~>) tys tys') ->
+    FullTerm (Product tys ~> Product tys') ctx
+  mapProd {tys = [<], tys' = [<]} [<] = lift id
   mapProd {tys = tys :< ty, tys' = tys' :< ty', prf} (fs :< f) =
-    Abs' (S Z)
+    abs' (S Z)
       (\p =>
-        App' (lift pair)
-          [<App (wkn (mapProd fs {prf = injective prf}) (Drop id) . lift fst) p
-          , App (wkn f (Drop id) . lift snd) p
+        app' (lift pair)
+          [<app (drop (mapProd fs {prf = injective prf}) . lift fst) p
+          , app (drop f . lift snd) p
           ])
 
   replicate : Nat -> a -> SnocList a
@@ -149,36 +150,36 @@ namespace Pair
   mapVect :
     {n : Nat} ->
     {ty, ty' : Ty} ->
-    Term [<] ((ty ~> ty') ~> Vect n ty ~> Vect n ty')
+    FullTerm ((ty ~> ty') ~> Vect n ty ~> Vect n ty') [<]
   mapVect =
-    Abs' (S Z)
+    abs' (S Z)
       (\f => mapProd {prf = trans (replicateLen n) (sym $ replicateLen n)} $ zipReplicate f)
 
   export
-  Nil : {ty : Ty} -> Term [<] (Vect 0 ty)
-  Nil = arb
+  nil : {ty : Ty} -> FullTerm (Vect 0 ty) [<]
+  nil = arb
 
   export
-  Cons : {n : Nat} -> {ty : Ty} -> Term [<] (ty ~> Vect n ty ~> Vect (S n) ty)
-  Cons = Abs' (S $ S Z) (\t, ts => App' (lift pair) [<ts, t])
+  cons : {n : Nat} -> {ty : Ty} -> FullTerm (ty ~> Vect n ty ~> Vect (S n) ty) [<]
+  cons = abs' (S $ S Z) (\t, ts => app' (lift pair) [<ts, t])
 
   export
-  head : {n : Nat} -> {ty : Ty} -> Term [<] (Vect (S n) ty ~> ty)
+  head : {n : Nat} -> {ty : Ty} -> FullTerm (Vect (S n) ty ~> ty) [<]
   head = snd
 
   export
-  tail : {n : Nat} -> {ty : Ty} -> Term [<] (Vect (S n) ty ~> Vect n ty)
+  tail : {n : Nat} -> {ty : Ty} -> FullTerm (Vect (S n) ty ~> Vect n ty) [<]
   tail = fst
 
   export
-  index : {n : Nat} -> {ty : Ty} -> (i : Fin n) -> Term [<] (Vect n ty ~> ty)
+  index : {n : Nat} -> {ty : Ty} -> (i : Fin n) -> FullTerm (Vect n ty ~> ty) [<]
   index FZ = head
   index (FS i) = index i . tail
 
   export
-  enumerate : (n : Nat) -> Term [<] (Vect n N)
+  enumerate : (n : Nat) -> FullTerm (Vect n N) [<]
   enumerate 0 = arb
-  enumerate (S k) = App' pair [<App' mapVect [<Abs' (S Z) Suc, enumerate k], Zero]
+  enumerate (S k) = app' pair [<app' mapVect [<abs' (S Z) suc, enumerate k], zero]
 
 namespace Sum
   export
@@ -186,20 +187,25 @@ namespace Sum
   t + u = B * (t <+> u)
 
   export
-  left : {t, u : Ty} -> Term [<] (t ~> (t + u))
-  left = Abs' (S Z) (\e => App' (lift pair) [<True, App (lift injL) e])
+  left : {t, u : Ty} -> FullTerm (t ~> (t + u)) [<]
+  left = abs' (S Z) (\e => app' (drop pair) [<drop true, app (drop injL) e])
+
+  export
+  right : {t, u : Ty} -> FullTerm (u ~> (t + u)) [<]
+  right = abs' (S Z) (\e => app' (drop pair) [<drop false, app (drop injR) e])
 
   export
-  right : {t, u : Ty} -> Term [<] (u ~> (t + u))
-  right = Abs' (S Z) (\e => App' (lift pair) [<False, App (lift injR) e])
+  case' : {t, u, ty : Ty} -> FullTerm ((t + u) ~> (t ~> ty) ~> (u ~> ty) ~> ty) [<]
+  case' = abs' (S $ S $ S Z)
+    (\s, f, g =>
+      app' (lift if')
+        [<app (lift fst) s
+        , app (f . lift (prjL . snd)) s
+        , app (g . lift (prjR . snd)) s])
 
   export
-  case' : {t, u, ty : Ty} -> Term [<] ((t ~> ty) ~> (u ~> ty) ~> (t + u) ~> ty)
-  case' = Abs' (S $ S $ S Z)
-    (\f, g, s =>
-      If (App (lift fst) s)
-        (App (f . lift (prjL . snd)) s)
-        (App (g . lift (prjR . snd)) s))
+  either : {t, u, ty : Ty} -> FullTerm ((t ~> ty) ~> (u ~> ty) ~> (t + u) ~> ty) [<]
+  either = abs' (S $ S $ S Z) (\f, g, s => app' (lift case') [<s, f, g])
 
   Sum' : Ty -> List Ty -> Ty
   Sum' ty [] = ty
@@ -213,88 +219,89 @@ namespace Sum
     {ty, ty' : Ty} ->
     {tys : List Ty} ->
     (i : Elem ty (ty' :: tys)) ->
-    Term [<] (ty ~> Sum' ty' tys)
-  put' {tys = []} Here = Abs' (S Z) id
+    FullTerm (ty ~> Sum' ty' tys) [<]
+  put' {tys = []} Here = id
   put' {tys = _ :: _} Here = left
   put' {tys = _ :: _} (There i) = right . put' i
 
   export
-  put : {tys : List1 Ty} -> {ty : Ty} -> (i : Elem ty (forget tys)) -> Term [<] (ty ~> Sum tys)
+  put : {tys : List1 Ty} -> {ty : Ty} -> (i : Elem ty (forget tys)) -> FullTerm (ty ~> Sum tys) [<]
   put {tys = _ ::: _} i = put' i
 
-  caseAll' :
+  any' :
     {ctx : SnocList Ty} ->
     {ty, ty' : Ty} ->
     {tys : List Ty} ->
-    All (Term ctx . (~> ty)) (ty' :: tys) ->
-    Term ctx (Sum' ty' tys ~> ty)
-  caseAll' (t :: []) = t
-  caseAll' (t :: u :: ts) = App' (lift case') [<t, caseAll' (u :: ts)]
+    All (flip FullTerm ctx . (~> ty)) (ty' :: tys) ->
+    FullTerm (Sum' ty' tys ~> ty) ctx
+  any' (t :: []) = t
+  any' (t :: u :: ts) = app' (lift either) [<t, any' (u :: ts)]
 
   export
-  caseAll :
+  any :
     {ctx : SnocList Ty} ->
     {tys : List1 Ty} ->
     {ty : Ty} ->
-    All (Term ctx . (~> ty)) (forget tys) ->
-    Term ctx (Sum tys ~> ty)
-  caseAll {tys = _ ::: _} = caseAll'
+    All (flip FullTerm ctx . (~> ty)) (forget tys) ->
+    FullTerm (Sum tys ~> ty) ctx
+  any {tys = _ ::: _} = any'
 
 namespace Nat
   export
-  IsZero : Term [<] (N ~> B)
-  IsZero = Abs' (S Z) (\m => Rec m (lift True) (Abs (lift False)))
+  isZero : FullTerm (N ~> B) [<]
+  isZero = abs' (S Z) (\m => rec m (drop true) (abs (lift false)))
 
   export
-  Add : Term [<] (N ~> N ~> N)
-  Add = Abs' (S $ S Z) (\m, n => Rec m n (Abs' (S Z) Suc))
+  add : FullTerm (N ~> N ~> N) [<]
+  add = abs' (S $ S Z) (\m, n => rec m n (abs' (S Z) suc))
 
   export
-  sum : {n : Nat} -> Term [<] (Vect n N ~> N)
-  sum {n = 0} = Abs Zero
-  sum {n = S k} = Abs' (S Z)
-    (\ns => App' (lift Add) [<App (lift head) ns, App (lift (sum . tail)) ns])
+  sum : {n : Nat} -> FullTerm (Vect n N ~> N) [<]
+  sum {n = 0} = abs zero
+  sum {n = S k} = abs' (S Z)
+    (\ns => app' (lift add) [<app (lift head) ns, app (lift (sum . tail)) ns])
 
   export
-  Pred : Term [<] (N ~> N)
-  Pred = Abs' (S Z)
+  pred : FullTerm (N ~> N) [<]
+  pred = abs' (S Z)
     (\m =>
-      App' (lift case')
-        [<Abs Zero
-        , Abs' (S Z) id
-        , Rec m
-            (lift $ App left (arb {ty = Unit}))
-            (App' (lift case')
-              [<Abs (lift $ App right Zero)
-              , Abs' (S Z) (\n => App (lift right) (Suc n))
+      app' (lift case')
+        [<rec m
+            (lift $ app left (arb {ty = Unit}))
+            (app' (lift either)
+              [<abs (lift $ app right zero)
+              , abs' (S Z) (\n => app (lift right) (suc n))
               ])
+        , abs zero
+        , drop id
         ])
 
   export
-  Sub : Term [<] (N ~> N ~> N)
-  Sub = Abs' (S $ S Z) (\m, n => Rec n m (lift Pred))
+  sub : FullTerm (N ~> N ~> N) [<]
+  sub = abs' (S $ S Z) (\m, n => rec n m (lift pred))
 
   export
-  LE : Term [<] (N ~> N ~> B)
-  LE = Abs' (S Z) (\m => lift IsZero . App (lift Sub) m)
+  le : FullTerm (N ~> N ~> B) [<]
+  le = abs' (S Z) (\m => lift isZero . app (lift sub) m)
 
   export
-  LT : Term [<] (N ~> N ~> B)
-  LT = Abs' (S Z) (\m => App (lift LE) (Suc m))
+  lt : FullTerm (N ~> N ~> B) [<]
+  lt = abs' (S Z) (\m => app (lift le) (suc m))
 
   export
-  Cond :
+  cond :
     {ctx : SnocList Ty} ->
     {ty : Ty} ->
-    List (Term ctx N, Term ctx (N ~> ty)) ->
-    Term ctx (N ~> ty)
-  Cond [] = lift arb
-  Cond ((n, v) :: xs) =
-    Abs' (S Z)
+    List (FullTerm N ctx, FullTerm (N ~> ty) ctx) ->
+    FullTerm (N ~> ty) ctx
+  cond [] = lift arb
+  cond ((n, v) :: xs) =
+    abs' (S Z)
       (\t =>
-        If (App' (lift LE) [<t, wkn n (Drop id)])
-          (App (wkn v (Drop id)) t)
-          (App (wkn (Cond xs) (Drop id)) (App' (lift Sub) [<t, wkn n (Drop id)])))
+        app' (lift if')
+          [<app' (lift le) [<t, drop n]
+          , app (drop v) t
+          , app (drop $ cond xs) (app' (lift sub) [<t, drop n])])
 
 namespace Data
   public export
@@ -323,7 +330,7 @@ namespace Data
   mapShape :
     {shape : Shape} ->
     {ty, ty' : Ty} ->
-    Term [<] ((ty ~> ty') ~> fillShape shape ty ~> fillShape shape ty')
+    FullTerm ((ty ~> ty') ~> fillShape shape ty ~> fillShape shape ty') [<]
   mapShape {shape = (shape, n)} = mapSnd . mapVect
 
   gmap :
@@ -347,55 +354,55 @@ namespace Data
     {ctx : SnocList Ty} ->
     {c : Container} ->
     {n : Nat} ->
-    (ts : Term ctx (Vect n (fix c))) ->
-    (acc : Term ctx N) ->
-    List (Term ctx N, Term ctx (N ~> N))
+    (ts : FullTerm (Vect n (fix c)) ctx) ->
+    (acc : FullTerm N ctx) ->
+    List (FullTerm N ctx, FullTerm (N ~> N) ctx)
   calcOffsets {n = 0} ts acc = []
   calcOffsets {n = S k} ts acc =
-    let hd = App (lift head) ts in
-    let n = App (lift $ project $ There $ There Here) hd in
-    let offset = App (lift $ project $ There Here) hd in
-    (n, App (lift Add) acc . offset) ::
+    let hd = app (lift head) ts in
+    let n = app (lift $ project $ There $ There Here) hd in
+    let offset = app (lift $ project $ There Here) hd in
+    (n, app (lift add) acc . offset) ::
     calcOffsets
-      (App (lift tail) ts)
-      (App' (lift Add) [<Suc n, acc])
+      (app (lift tail) ts)
+      (app' (lift add) [<suc n, acc])
 
   calcData :
     {ctx : SnocList Ty} ->
     {c : Container} ->
     {n : Nat} ->
-    (ts : Term ctx (Vect n (fix c))) ->
-    (acc : Term ctx N) ->
-    List (Term ctx N, Term ctx (N ~> fill c N))
+    (ts : FullTerm (Vect n (fix c)) ctx) ->
+    (acc : FullTerm N ctx) ->
+    List (FullTerm N ctx, FullTerm (N ~> fill c N) ctx)
   calcData {n = 0} ts acc = []
   calcData {n = S k} ts acc =
-    let hd = App (lift head) ts in
-    let n = App (lift $ project $ There $ There Here) hd in
-    (n, App (lift $ project Here) hd) ::
+    let hd = app (lift head) ts in
+    let n = app (lift $ project $ There $ There Here) hd in
+    (n, app (lift $ project Here) hd) ::
     calcData
-      (App (lift tail) ts)
-      (App' (lift Add) [<Suc n, acc])
+      (app (lift tail) ts)
+      (app' (lift add) [<suc n, acc])
 
   export
   intro :
     {c : Container} ->
     {shape : Shape} ->
     Elem shape (forget c) ->
-    Term [<] (fillShape shape (fix c) ~> fix c)
-  intro {shape = (shape, n)} i = Abs' (S Z)
+    FullTerm (fillShape shape (fix c) ~> fix c) [<]
+  intro {shape = (shape, n)} i = abs' (S Z)
     (\t =>
-      App' (lift $ pair' {tys = [<N, N ~> N, N ~> fill c N]})
-        [<App (lift (sum . App mapVect (Abs' (S Z) Suc . project (There $ There Here)) . snd)) t
-        , Cond ((Zero, Abs' (S Z) Suc) :: calcOffsets (App (lift snd) t) (Suc Zero))
-        , Cond
-          (  (Zero,
-              Abs
-                (App
+      app' (lift $ pair' {tys = [<N, N ~> N, N ~> fill c N]})
+        [<app (lift (sum . app mapVect (abs' (S Z) suc . project (There $ There Here)) . snd)) t
+        , cond ((zero, abs' (S Z) suc) :: calcOffsets (app (lift snd) t) (suc zero))
+        , cond
+          (  (zero,
+              abs
+                (app
                   (lift $ put {tys = map (flip fillShape N) c} $
                     rewrite forgetMap (flip fillShape N) c in
                     elemMap (flip fillShape N) i)
-                  (App' (lift mapSnd) [<Abs (lift $ enumerate n), wkn t (Drop id)])))
-          :: calcData (App (lift snd) t) (Suc Zero)
+                  (app' (lift mapSnd) [<abs (lift $ enumerate n), drop t])))
+          :: calcData (app (lift snd) t) (suc zero)
           )
         ])
 
@@ -404,28 +411,28 @@ namespace Data
     {c : Container} ->
     {ctx : SnocList Ty} ->
     {ty : Ty} ->
-    All (Term ctx . (~> ty) . flip Data.fillShape ty) (forget c) ->
-    Term ctx (fix c ~> ty)
-  elim cases = Abs' (S Z)
+    All (flip FullTerm ctx . (~> ty) . flip Data.fillShape ty) (forget c) ->
+    FullTerm (fix c ~> ty) ctx
+  elim cases = abs' (S Z)
     (\t =>
-      let tags = Suc (App (lift $ project $ There $ There Here) t) in
-      let offset = App (lift $ project $ There Here) (wkn t (Drop $ Drop id)) in
-      let vals = App (lift $ project $ Here) (wkn t (Drop $ Drop id)) in
-      App'
-        (Rec tags
+      let tags = suc (app (lift $ project $ There $ There Here) t) in
+      let offset = app (lift $ project $ There Here) (drop $ drop t) in
+      let vals = app (lift $ project $ Here) (drop $ drop t) in
+      app'
+        (rec tags
           (lift arb)
-          (Abs' (S $ S Z) (\rec, n =>
-            App
-              (caseAll {tys = map (flip fillShape N) c}
+          (abs' (S $ S Z) (\rec, n =>
+            app
+              (any {tys = map (flip fillShape N) c}
                 (rewrite forgetMap (flip fillShape N) c in
                  gmap
                    (\f =>
-                     wkn f (Drop $ Drop $ Drop id) .
-                     App (lift mapShape) (rec . App (lift Add) (App offset n)))
+                     drop (drop $ drop f) .
+                     app (lift mapShape) (rec . app (lift add) (app offset n)))
                    cases) .
                vals)
               n)))
-        [<Zero])
+        [<zero])
 
   -- elim cases (#tags-1,offset,data) =
   --   let
diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr
index ebde8d5..90bec66 100644
--- a/src/Total/LogRel.idr
+++ b/src/Total/LogRel.idr
@@ -181,19 +181,18 @@ allValid help (Abs t) sub allRels =
   (let
       rec =
         valid
-          (wknAll sub (Drop $ id @{termsLen sub}) :< Var Here)
-          (wknAllRel help allRels (Drop $ id @{termsLen sub}) :< help.var Here)
+          (wknAll sub (Drop id) :< Var Here)
+          (wknAllRel help allRels (Drop id) :< help.var Here)
     in
       help.abs rec
   , \thin, u, rel =>
     let
       eq :
         (subst
-          (wkn (subst t (wknAll sub (Drop $ id @{termsLen sub}) :< Var Here)) (Keep thin))
-          (Base (id @{length _}) :< u) =
+          (wkn (subst t (wknAll sub (Drop Thinning.id) :< Var Here)) (Keep thin))
+          (Base Thinning.id :< u) =
          subst t (wknAll sub thin :< u))
       eq =
-        rewrite lenUnique (termsLen sub) (length ctx') in
         Calc $
           |~ subst (wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin)) (Base id :< u)
           ~~ subst (subst t (wknAll sub (Drop id) :< Var Here)) (restrict (Base id :< u) (Keep thin))
@@ -219,8 +218,8 @@ allValid help (Abs t) sub allRels =
 allValid help (App t u) sub allRels =
   let (pt, app) = allValid help t sub allRels in
   let rel = allValid help u sub allRels in
-  rewrite sym $ wknId @{termsLen sub} (subst t sub) in
-    app (id @{termsLen sub}) (subst u sub) rel
+  rewrite sym $ wknId (subst t sub) in
+    app id (subst u sub) rel
 allValid help Zero sub allRels = help.zero
 allValid help (Suc t) sub allRels =
   let pt = allValid help t sub allRels in
@@ -240,4 +239,4 @@ allRel :
   (t : Term ctx ty) ->
   P t
 allRel help t =
-  rewrite sym $ substId @{length ctx} t in escape (allValid help t (Base $ id @{length ctx}) Base)
+  rewrite sym $ substId t in escape (allValid help t (Base id) Base)
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
index b11665b..a424515 100644
--- a/src/Total/Reduction.idr
+++ b/src/Total/Reduction.idr
@@ -70,28 +70,37 @@ RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step
 -- Properties ------------------------------------------------------------------
 
 lemma :
-  (0 len : Len ctx) ->
   (t : Term (ctx :< ty) ty') ->
   (thin : ctx `Thins` ctx') ->
   (u : Term ctx ty) ->
-  subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) = wkn (subst t (Base (id @{len}) :< u)) thin
-lemma len t thin u = Calc $
-  |~ subst (wkn t (Keep thin)) (Base id :< wkn u thin)
-  ~~ subst t (restrict (Base id :< wkn u thin) (Keep thin))
-    ...(substWkn t (Keep thin) (Base id :< wkn u thin))
-  ~~ subst t (Base (id . thin) :< wkn u thin)
-    ...(Refl)
-  ~~ subst t (Base (thin . id) :< wkn u thin)
-    ...(cong (subst t . (:< wkn u thin) . Base) $ trans (identityLeft thin) (sym $ identityRight thin))
-  ~~ wkn (subst t (Base id :< u)) thin
-    ...(sym $ wknSubst t (Base id :< u) thin)
+  subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) =
+  wkn (subst t (Base Thinning.id :< u)) thin
+lemma t thin u =
+  Calc $
+    |~ subst (wkn t (Keep thin)) (Base id :< wkn u thin)
+    ~~ subst t (restrict (Base id :< wkn u thin) (Keep thin))
+      ...(substWkn t (Keep thin) (Base id :< wkn u thin))
+    ~~ subst t (Base (id . thin) :< wkn u thin)
+      ...(Refl)
+    ~~ subst t (Base (thin . id) :< wkn u thin)
+      ...(cong (subst t . (:< wkn u thin) . Base) $ trans (identityLeft thin) (sym $ identityRight thin))
+    ~~ wkn (subst t (Base (id) :< u)) thin
+      ...(sym $ wknSubst t (Base (id @{length ctx}) :< u) thin)
 
 export
 wknStep : t > u -> wkn t thin > wkn u thin
 wknStep (AbsCong step) = AbsCong (wknStep step)
 wknStep (AppCong1 step) = AppCong1 (wknStep step)
 wknStep (AppCong2 step) = AppCong2 (wknStep step)
-wknStep (AppBeta len {t, u}) {thin} = rewrite sym $ lemma len t thin u in AppBeta _
+wknStep (AppBeta len {ctx, t, u}) {thin} =
+  let
+    0 eq :
+      (subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) =
+       wkn (subst t (Base (id @{len}) :< u)) thin)
+    eq = rewrite lenUnique len (length ctx) in lemma t thin u
+  in
+    rewrite sym eq in
+    AppBeta _
 wknStep (SucCong step) = SucCong (wknStep step)
 wknStep (RecCong1 step) = RecCong1 (wknStep step)
 wknStep (RecCong2 step) = RecCong2 (wknStep step)
diff --git a/src/Total/Syntax.idr b/src/Total/Syntax.idr
index 6c34250..fead586 100644
--- a/src/Total/Syntax.idr
+++ b/src/Total/Syntax.idr
@@ -5,9 +5,10 @@ import public Data.List.Quantifiers
 import public Data.SnocList
 import public Data.SnocList.Quantifiers
 import public Total.Term
+import public Total.Term.CoDebruijn
 
 infixr 20 ~>*
-infix 9 .*
+infixl 9 .~, .*
 
 public export
 (~>*) : SnocList Ty -> Ty -> Ty
@@ -31,47 +32,97 @@ before Z f x = x
 before (S k) f x = before k f (after k (. f) x)
 
 export
-Lit : Nat -> Term ctx N
-Lit 0 = Zero
-Lit (S n) = Suc (Lit n)
+lit : Len ctx => Nat -> FullTerm N ctx
+lit 0 = Zero `Over` empty
+lit (S n) = suc (lit n)
 
-AbsHelper :
+absHelper :
   (k : Len tys) ->
-  Fun k (flip Elem (ctx ++ tys)) (Term (ctx ++ tys) ty) ->
-  Term ctx (tys ~>* ty)
-AbsHelper Z x = x
-AbsHelper (S k) x =
-  AbsHelper k $
-  after k (\f => Term.Abs (f SnocList.Elem.Here)) $
+  Fun k (flip Elem (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
+  FullTerm (tys ~>* ty) ctx
+absHelper Z x = x
+absHelper (S k) x =
+  absHelper k $
+  after k (\f => CoDebruijn.abs (f SnocList.Elem.Here)) $
   before k SnocList.Elem.There x
 
 export
-Abs' :
+abs' :
+  (len : Len ctx) =>
   (k : Len tys) ->
-  Fun k (Term (ctx ++ tys)) (Term (ctx ++ tys) ty) ->
-  Term ctx (tys ~>* ty)
-Abs' k = AbsHelper k . before k Var
+  Fun k (flip FullTerm (ctx ++ tys)) (FullTerm ty (ctx ++ tys)) ->
+  FullTerm (tys ~>* ty) ctx
+abs' k = absHelper k . before k (var @{lenAppend len k})
 
 export
-App' : {tys : SnocList Ty} -> Term ctx (tys ~>* ty) -> All (Term ctx) tys -> Term ctx ty
-App' t [<] = t
-App' t (us :< u) = App (App' t us) u
+app' :
+  {tys : SnocList Ty} ->
+  FullTerm (tys ~>* ty) ctx ->
+  All (flip FullTerm ctx) tys ->
+  FullTerm ty ctx
+app' t [<] = t
+app' t (us :< u) = app (app' t us) u
+
+-- export
+-- compose :
+--   {ty, ty' : Ty} ->
+--   (t : FullTerm (ty' ~> ty'') ctx) ->
+--   (u : FullTerm (ty ~> ty') ctx) ->
+--   Len u.support =>
+--   Covering Covers t.thin u.thin ->
+--   CoTerm (ty ~> ty'') ctx
+-- compose (t `Over` thin1) (u `Over` thin2) cover =
+--   Abs
+--     (MakeBound
+--       (App
+--         (MakePair
+--           (t `Over` Drop thin1)
+--           (App
+--             (MakePair
+--               (u `Over` Drop id)
+--               (Var `Over` Keep empty)
+--               (DropKeep (coverIdLeft empty)))
+--            `Over` Keep thin2)
+--           (DropKeep cover)))
+--       (Keep Empty))
+
+-- export
+-- (.~) :
+--   Len ctx =>
+--   {ty, ty' : Ty} ->
+--   CoTerm (ty' ~> ty'') ctx ->
+--   CoTerm (ty ~> ty') ctx ->
+--   CoTerm (ty ~> ty'') ctx
+-- t .~ u = compose (t `Over` id) (u `Over` id) (coverIdLeft id)
 
 export
-(.) : Len ctx => {ty, ty' : Ty} -> Term ctx (ty' ~> ty'') -> Term ctx (ty ~> ty') -> Term ctx (ty ~> ty'')
-t . u = Abs' (S Z) (\x => App (wkn t (Drop id)) (App (wkn u (Drop id)) x))
+(.) :
+  Len ctx =>
+  {ty, ty' : Ty} ->
+  FullTerm (ty' ~> ty'') ctx ->
+  FullTerm (ty ~> ty') ctx ->
+  FullTerm (ty ~> ty'') ctx
+t . u = abs' (S Z) (\x => app (drop t) (app (drop u) x))
 
 export
 (.*) :
   Len ctx =>
   {ty : Ty} ->
   {tys : SnocList Ty} ->
-  Term ctx (ty ~> ty') ->
-  Term ctx (tys ~>* ty) ->
-  Term ctx (tys ~>* ty')
-(.*) {tys = [<]} t u = App t u
-(.*) {tys = tys :< ty''} t u = Abs' (S Z) (\f => wkn t (Drop id) . f) .*  u
+  FullTerm (ty ~> ty') ctx ->
+  FullTerm (tys ~>* ty) ctx ->
+  FullTerm (tys ~>* ty') ctx
+(.*) {tys = [<]} t u = app t u
+(.*) {tys = tys :< ty''} t u = abs' (S Z) (\f => drop t . f) .*  u
 
 export
-lift : {ctx : SnocList Ty} -> Term [<] ty -> Term ctx ty
+lift : Len ctx => FullTerm ty [<] -> FullTerm ty ctx
 lift t = wkn t empty
+
+export
+id' : CoTerm (ty ~> ty) [<]
+id' = Abs (MakeBound Var (Keep Empty))
+
+export
+id : FullTerm (ty ~> ty) [<]
+id = id' `Over` empty
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index d21ec73..8e3e42a 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -42,12 +42,6 @@ data Terms : SnocList Ty -> SnocList Ty -> Type where
 
 %name Terms sub
 
-%hint
-export
-termsLen : Terms ctx' ctx -> Len ctx'
-termsLen (Base thin) = lenTgt thin
-termsLen (sub :< t) = termsLen sub
-
 public export
 index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty
 index (Base thin) i = Var (index thin i)
@@ -60,7 +54,7 @@ wknAll (Base thin') thin = Base (thin . thin')
 wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin
 
 public export
-subst : Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
+subst : Len ctx' => Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
 subst (Var i) sub = index sub i
 subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop id) :< Var Here)
 subst (App t u) sub = App (subst t sub) (subst u sub)
@@ -75,7 +69,7 @@ restrict (sub :< t) (Drop thin) = restrict sub thin
 restrict (sub :< t) (Keep thin) = restrict sub thin :< t
 
 public export
-(.) : Terms ctx'' ctx' -> Terms ctx' ctx -> Terms ctx'' ctx
+(.) : Len ctx'' => Terms ctx'' ctx' -> Terms ctx' ctx -> Terms ctx'' ctx
 sub2 . (Base thin) = restrict sub2 thin
 sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2
 
@@ -179,7 +173,6 @@ wknSubst :
 wknSubst (Var i) sub thin =
   sym (indexWknAll sub thin i)
 wknSubst (Abs t) sub thin =
-  rewrite lenUnique (termsLen $ wknAll sub thin) (lenTgt thin) in
   cong Abs $ Calc $
     |~ wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin)
     ~~ subst t (wknAll (wknAll sub (Drop id)) (Keep thin) :< Var (index (Keep thin) Here))
@@ -208,7 +201,6 @@ substWkn :
 substWkn (Var i) thin sub =
   sym (indexRestrict thin sub i)
 substWkn (Abs t) thin sub =
-  rewrite lenUnique (termsLen $ restrict sub thin) (termsLen sub) in
   cong Abs $ Calc $
     |~ subst (wkn t $ Keep thin) (wknAll sub (Drop id) :< Var Here)
     ~~ subst t (restrict (wknAll sub (Drop id)) thin :< Var Here)
@@ -254,10 +246,7 @@ substCong :
   Equiv sub sub' ->
   subst t sub = subst t sub'
 substCong (Var i) prf = indexCong prf i
-substCong (Abs t) prf =
-  rewrite lenUnique (termsLen sub) (termsLen sub') in
-  rewrite lenUnique (termsLen sub') len in
-  cong Abs (substCong t (WknAll prf))
+substCong (Abs t) prf = cong Abs (substCong t (WknAll prf))
 substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf)
 substCong Zero prf = Refl
 substCong (Suc t) prf = cong Suc (substCong t prf)
@@ -329,7 +318,6 @@ export
 substId : (len : Len ctx) => (t : Term ctx ty) -> subst t (Base $ id @{len}) = t
 substId (Var i) = cong Var (indexId i)
 substId (Abs t) =
-  rewrite lenUnique (termsLen $ Base $ id @{len}) len in
   rewrite identitySquared len in
   cong Abs $ trans (sym $ substCong t Base) (substId t)
 substId (App t u) = cong2 App (substId t) (substId u)
@@ -346,7 +334,6 @@ substHomo :
 substHomo (Var i) sub1 sub2 =
   sym $ indexComp sub1 sub2 i
 substHomo (Abs t) sub1 sub2 =
-  rewrite lenUnique (termsLen $ sub2 . sub1) (termsLen sub2) in
   cong Abs $ Calc $
     |~ subst (subst t (wknAll sub1 (Drop id) :< Var Here)) (wknAll sub2 (Drop id) :< Var Here)
     ~~ subst t ((wknAll sub2 (Drop id) :< Var Here) . (wknAll sub1 (Drop id) :< Var Here))
diff --git a/src/Total/Term/CoDebruijn.idr b/src/Total/Term/CoDebruijn.idr
new file mode 100644
index 0000000..00abc31
--- /dev/null
+++ b/src/Total/Term/CoDebruijn.idr
@@ -0,0 +1,111 @@
+module Total.Term.CoDebruijn
+
+import public Data.SnocList.Elem
+import public Thinning
+import Syntax.PreorderReasoning
+import Total.Term
+
+%prefix_record_projections off
+
+public export
+data CoTerm : Ty -> SnocList Ty -> Type where
+  Var : CoTerm ty [<ty]
+  Abs : Binds [<ty] (CoTerm ty') ctx -> CoTerm (ty ~> ty') ctx
+  App : {ty : Ty} -> Pair (CoTerm (ty ~> ty')) (CoTerm ty) ctx -> CoTerm ty' ctx
+  Zero : CoTerm N [<]
+  Suc : CoTerm N ctx -> CoTerm N ctx
+  Rec : Pair (CoTerm N) (Pair (CoTerm ty) (CoTerm (ty ~> ty))) ctx -> CoTerm ty ctx
+
+%name CoTerm t, u, v
+
+public export
+FullTerm : Ty -> SnocList Ty -> Type
+FullTerm ty ctx = Thinned (CoTerm ty) ctx
+
+export
+var : Len ctx => Elem ty ctx -> FullTerm ty ctx
+var i = Var `Over` point i
+
+export
+abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx
+abs = map Abs . MkBound (S Z)
+
+export
+app : {ty : Ty} -> FullTerm (ty ~> ty') ctx -> FullTerm ty ctx -> FullTerm ty' ctx
+app t u = map App (MkPair t u)
+
+export
+zero : Len ctx => FullTerm N ctx
+zero = Zero `Over` empty
+
+export
+suc : FullTerm N ctx -> FullTerm N ctx
+suc = map Suc
+
+export
+rec : FullTerm N ctx -> FullTerm ty ctx -> FullTerm (ty ~> ty) ctx -> FullTerm ty ctx
+rec t u v = map Rec $ MkPair t (MkPair u v)
+
+export
+wkn : FullTerm ty ctx -> ctx `Thins` ctx' -> FullTerm ty ctx'
+wkn (t `Over` thin) thin' = t `Over` thin' . thin
+
+public export
+data CoTerms : SnocList Ty -> SnocList Ty -> Type where
+  Base : ctx `Thins` ctx' -> CoTerms ctx ctx'
+  (:<) : CoTerms ctx ctx' -> FullTerm ty ctx' -> CoTerms (ctx :< ty) ctx'
+
+%name CoTerms sub
+
+export
+shift : CoTerms ctx ctx' -> CoTerms ctx (ctx' :< ty)
+shift (Base thin) = Base (Drop thin)
+shift (sub :< (t `Over` thin)) = shift sub :< (t `Over` Drop thin)
+
+export
+lift : Len ctx' => CoTerms ctx ctx' -> CoTerms (ctx :< ty) (ctx' :< ty)
+lift sub = shift sub :< var Here
+
+export
+restrict : CoTerms ctx' ctx'' -> ctx `Thins` ctx' -> CoTerms ctx ctx''
+restrict (Base thin') thin = Base (thin' . thin)
+restrict (sub :< t) (Drop thin) = restrict sub thin
+restrict (sub :< t) (Keep thin) = restrict sub thin :< t
+
+export
+subst : Len ctx' => FullTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx'
+subst' : Len ctx' => CoTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx'
+
+subst (t `Over` thin) sub = subst' t (restrict sub thin)
+
+subst' t (Base thin) = t `Over` thin
+subst' Var (sub :< t) = t
+subst' (Abs (MakeBound t (Drop Empty))) sub@(_ :< _) = abs (subst' t $ shift sub)
+subst' (Abs (MakeBound t (Keep Empty))) sub@(_ :< _) = abs (subst' t $ lift sub)
+subst' (App (MakePair t u _)) sub@(_ :< _) = app (subst t sub) (subst u sub)
+subst' (Suc t) sub@(_ :< _) = suc (subst' t sub)
+subst' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub@(_ :< _) =
+  rec (subst t sub) (subst u (restrict sub thin)) (subst v (restrict sub thin))
+
+toTerm : CoTerm ty ctx -> ctx `Thins` ctx' -> Term ctx' ty
+toTerm Var thin = Var (index thin Here)
+toTerm (Abs (MakeBound t (Drop Empty))) thin = Abs (toTerm t (Drop thin))
+toTerm (Abs (MakeBound t (Keep Empty))) thin = Abs (toTerm t (Keep thin))
+toTerm (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
+  App (toTerm t (thin . thin1)) (toTerm u (thin . thin2))
+toTerm Zero thin = Zero
+toTerm (Suc t) thin = Suc (toTerm t thin)
+toTerm
+  (Rec
+    (MakePair
+      (t `Over` thin1)
+      (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin') _))
+  thin =
+  Rec
+    (toTerm t (thin . thin1))
+    (toTerm u ((thin . thin') . thin2))
+    (toTerm v ((thin . thin') . thin3))
+
+export
+Cast (FullTerm ty ctx) (Term ctx ty) where
+  cast (t `Over` thin) = toTerm t thin