From cedc6109895a53ce6ed667e0391b232bf5463387 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 15 Jun 2023 16:09:42 +0100
Subject: WIP : use smarter weakenings.

---
 src/Total/Term.idr | 485 ++++++++++++++++++++++-------------------------------
 1 file changed, 197 insertions(+), 288 deletions(-)

(limited to 'src/Total/Term.idr')

diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 129662a..7d6fba0 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -1,13 +1,19 @@
 module Total.Term
 
+import Control.Relation
 import public Data.SnocList.Elem
+import public Subst
 import public Thinning
+
 import Syntax.PreorderReasoning
+import Syntax.PreorderReasoning.Generic
 
 %prefix_record_projections off
 
 infixr 10 ~>
 
+-- Types -----------------------------------------------------------------------
+
 public export
 data Ty : Type where
   N : Ty
@@ -15,64 +21,48 @@ data Ty : Type where
 
 %name Ty ty
 
+-- Definition ------------------------------------------------------------------
+
 public export
-data Term : SnocList Ty -> Ty -> Type where
-  Var : (i : Elem ty ctx) -> Term ctx ty
-  Abs : Term (ctx :< ty) ty' -> Term ctx (ty ~> ty')
-  App : {ty : Ty} -> Term ctx (ty ~> ty') -> Term ctx ty -> Term ctx ty'
-  Zero : Term ctx N
-  Suc : Term ctx N -> Term ctx N
-  Rec : Term ctx N -> Term ctx ty -> Term ctx (ty ~> ty) -> Term ctx ty
+data Term : Ty -> SnocList Ty -> Type where
+  Var : (i : Elem ty ctx) -> Term ty ctx
+  Abs : Term ty' (ctx :< ty) -> Term (ty ~> ty') ctx
+  App : {ty : Ty} -> Term (ty ~> ty') ctx -> Term ty ctx -> Term ty' ctx
+  Zero : Term N ctx
+  Suc : Term N ctx -> Term N ctx
+  Rec : Term N ctx -> Term ty ctx -> Term (ty ~> ty) ctx -> Term ty ctx
 
 %name Term t, u, v
 
-public export
-wkn : Term ctx ty -> ctx `Thins` ctx' -> Term ctx' ty
-wkn (Var i) thin = Var (index thin i)
-wkn (Abs t) thin = Abs (wkn t $ Keep thin)
-wkn (App t u) thin = App (wkn t thin) (wkn u thin)
-wkn Zero thin = Zero
-wkn (Suc t) thin = Suc (wkn t thin)
-wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin)
+-- Raw Interfaces --------------------------------------------------------------
 
-public export
-data Terms : SnocList Ty -> SnocList Ty -> Type where
-  Base : ctx `Thins` ctx' -> Terms ctx' ctx
-  (:<) : Terms ctx' ctx -> Term ctx' ty -> Terms ctx' (ctx :< ty)
+export
+Point Ty Term where
+  point = Var
 
-%name Terms sub
+export
+Weaken Ty Term where
+  wkn (Var i) thin = Var (index thin i)
+  wkn (Abs t) thin = Abs (wkn t (keep thin _))
+  wkn (App t u) thin = App (wkn t thin) (wkn u thin)
+  wkn Zero thin = Zero
+  wkn (Suc t) thin = Suc (wkn t thin)
+  wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin)
 
-public export
-index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty
-index (Base thin) i = Var (index thin i)
-index (sub :< t) Here = t
-index (sub :< t) (There i) = index sub i
+export
+PointWeaken Ty Term where
 
-public export
-wknAll : Terms ctx' ctx -> ctx' `Thins` ctx'' -> Terms ctx'' ctx
-wknAll (Base thin') thin = Base (thin . thin')
-wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin
+-- Substitution ----------------------------------------------------------------
 
 public export
-subst : Len ctx' => Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
+subst : Term ty ctx -> Subst Term ctx ctx' -> Term ty ctx'
 subst (Var i) sub = index sub i
-subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop id) :< Var Here)
+subst (Abs t) sub = Abs (subst t $ lift sub)
 subst (App t u) sub = App (subst t sub) (subst u sub)
 subst Zero sub = Zero
 subst (Suc t) sub = Suc (subst t sub)
 subst (Rec t u v) sub = Rec (subst t sub) (subst u sub) (subst v sub)
 
-public export
-restrict : Terms ctx'' ctx' -> ctx `Thins` ctx' -> Terms 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
-
-public export
-(.) : 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
-
 -- Properties ------------------------------------------------------------------
 
 -- Utilities
@@ -84,106 +74,63 @@ cong3 f Refl Refl Refl = Refl
 -- Weakening
 
 export
-wknHomo :
-  (t : Term ctx ty) ->
-  (thin1 : ctx `Thins` ctx') ->
-  (thin2 : ctx' `Thins` ctx'') ->
-  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
-wknHomo (Var i) thin1 thin2 =
-  cong Var (indexHomo thin2 thin1 i)
-wknHomo (Abs t) thin1 thin2 =
-  cong Abs (wknHomo t (Keep thin1) (Keep thin2))
-wknHomo (App t u) thin1 thin2 =
-  cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
-wknHomo Zero thin1 thin2 =
-  Refl
-wknHomo (Suc t) thin1 thin2 =
-  cong Suc (wknHomo t thin1 thin2)
-wknHomo (Rec t u v) thin1 thin2 =
-  cong3 Rec (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) (wknHomo v thin1 thin2)
+FullWeaken Ty Term where
+  shiftIsWkn t = Refl
+
+  wknId (Var i) = cong Var $ indexId i
+  wknId (Abs t) = cong Abs $ trans (cong (wkn t) (keepId _ _)) (wknId t)
+  wknId (App t u) = cong2 App (wknId t) (wknId u)
+  wknId Zero = Refl
+  wknId (Suc t) = cong Suc (wknId t)
+  wknId (Rec t u v) = cong3 Rec (wknId t) (wknId u) (wknId v)
+
+  wknHomo (Var i) thin1 thin2 = cong Var $ indexHomo thin1 thin2 i
+  wknHomo (Abs t) thin1 thin2 =
+    cong Abs $
+      trans
+        (wknHomo t (keep thin1 _) (keep thin2 _))
+        (cong (wkn t) $ keepHomo thin2 thin1 _)
+  wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
+  wknHomo Zero thin1 thin2 = Refl
+  wknHomo (Suc t) thin1 thin2 = cong Suc (wknHomo t thin1 thin2)
+  wknHomo (Rec t u v) thin1 thin2 =
+    cong3 Rec
+      (wknHomo t thin1 thin2)
+      (wknHomo u thin1 thin2)
+      (wknHomo v thin1 thin2)
 
 export
-wknId : Len ctx => (t : Term ctx ty) -> wkn t Thinning.id = t
-wknId (Var i) = cong Var (indexId i)
-wknId (Abs t) = cong Abs (wknId t)
-wknId (App t u) = cong2 App (wknId t) (wknId u)
-wknId Zero = Refl
-wknId (Suc t) = cong Suc (wknId t)
-wknId (Rec t u v) = cong3 Rec (wknId t) (wknId u) (wknId v)
-
-indexWknAll :
-  (sub : Terms ctx' ctx) ->
-  (thin : ctx' `Thins` ctx'') ->
-  (i : Elem ty ctx) ->
-  index (wknAll sub thin) i = wkn (index sub i) thin
-indexWknAll (Base thin') thin i = sym $ cong Var $ indexHomo thin thin' i
-indexWknAll (sub :< t) thin Here = Refl
-indexWknAll (sub :< t) thin (There i) = indexWknAll sub thin i
-
-wknAllHomo :
-  (sub : Terms ctx ctx''') ->
-  (thin1 : ctx `Thins` ctx') ->
-  (thin2 : ctx' `Thins` ctx'') ->
-  wknAll (wknAll sub thin1) thin2 = wknAll sub (thin2 . thin1)
-wknAllHomo (Base thin) thin1 thin2 = cong Base (assoc thin2 thin1 thin)
-wknAllHomo (sub :< t) thin1 thin2 = cong2 (:<) (wknAllHomo sub thin1 thin2) (wknHomo t thin1 thin2)
-
--- Restrict
-
-indexRestrict :
-  (thin : ctx `Thins` ctx') ->
-  (sub : Terms ctx'' ctx') ->
-  (i : Elem ty ctx) ->
-  index (restrict sub thin) i = index sub (index thin i)
-indexRestrict thin (Base thin') i = sym $ cong Var $ indexHomo thin' thin i
-indexRestrict (Drop thin) (sub :< t) i = indexRestrict thin sub i
-indexRestrict (Keep thin) (sub :< t) Here = Refl
-indexRestrict (Keep thin) (sub :< t) (There i) = indexRestrict thin sub i
-
-restrictId : (len : Len ctx) => (sub : Terms ctx' ctx) -> restrict sub (id @{len}) = sub
-restrictId (Base thin) = cong Base (identityRight thin)
-restrictId {len = S k} (sub :< t) = cong (:< t) (restrictId sub)
-
-restrictHomo :
-  (sub : Terms ctx ctx''') ->
-  (thin1 : ctx'' `Thins` ctx''') ->
-  (thin2 : ctx' `Thins` ctx'') ->
-  restrict sub (thin1 . thin2) = restrict (restrict sub thin1) thin2
-restrictHomo (Base thin) thin1 thin2 = cong Base (assoc thin thin1 thin2)
-restrictHomo (sub :< t) (Drop thin1) thin2 = restrictHomo sub thin1 thin2
-restrictHomo (sub :< t) (Keep thin1) (Drop thin2) = restrictHomo sub thin1 thin2
-restrictHomo (sub :< t) (Keep thin1) (Keep thin2) = cong (:< t) $ restrictHomo sub thin1 thin2
-
-wknAllRestrict :
-  (thin1 : ctx `Thins` ctx') ->
-  (sub : Terms ctx'' ctx') ->
-  (thin2 : ctx'' `Thins` ctx''') ->
-  restrict (wknAll sub thin2) thin1 = wknAll (restrict sub thin1) thin2
-wknAllRestrict thin1 (Base thin) thin2 = sym $ cong Base $ assoc thin2 thin thin1
-wknAllRestrict (Drop thin) (sub :< t) thin2 = wknAllRestrict thin sub thin2
-wknAllRestrict (Keep thin) (sub :< t) thin2 = cong (:< wkn t thin2) (wknAllRestrict thin sub thin2)
+FullPointWeaken Ty Term where
+  wknPoint i thin = Refl
 
 -- Substitution & Weakening
 
+export
+substCong :
+  (t : Term ty ctx) ->
+  {0 sub1, sub2 : Subst Term ctx ctx'} ->
+  Equiv sub1 sub2 ->
+  subst t sub1 = subst t sub2
+substCong (Var i) e = e.equiv i
+substCong (Abs t) e = cong Abs $ substCong t (liftCong e)
+substCong (App t u) e = cong2 App (substCong t e) (substCong u e)
+substCong Zero e = Refl
+substCong (Suc t) e = cong Suc (substCong t e)
+substCong (Rec t u v) e = cong3 Rec (substCong t e) (substCong u e) (substCong v e)
+
 export
 wknSubst :
-  (t : Term ctx ty) ->
-  (sub : Terms ctx' ctx) ->
+  (t : Term ty ctx) ->
+  (sub : Subst Term ctx ctx') ->
   (thin : ctx' `Thins` ctx'') ->
-  wkn (subst t sub) thin = subst t (wknAll sub thin)
+  wkn (subst t sub) thin = subst t (wkn sub thin)
 wknSubst (Var i) sub thin =
-  sym (indexWknAll sub thin i)
-wknSubst (Abs t) sub thin =
+  indexWkn sub thin i
+wknSubst (Abs {ty} t) sub thin =
   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))
-      ...(wknSubst t (wknAll sub (Drop id) :< Var Here) (Keep thin))
-    ~~ subst t (wknAll sub (Keep thin . Drop id) :< Var Here)
-      ...(cong (subst t . (:< Var Here)) (wknAllHomo sub (Drop id) (Keep thin)))
-    ~~ subst t (wknAll sub (Drop id . thin) :< Var Here)
-      ...(cong (subst t . (:< Var Here) . wknAll sub . Drop) $ trans (identityRight thin) (sym $ identityLeft thin))
-    ~~ subst t (wknAll (wknAll sub thin) (Drop id) :< Var Here)
-      ...(sym $ cong (subst t . (:< Var Here)) $ wknAllHomo sub thin (Drop id))
+    |~ wkn (subst t (lift sub)) (keep thin ty)
+    ~~ subst t (wkn (lift sub) (keep thin ty)) ...(wknSubst t (lift sub) (keep thin _))
+    ~~ subst t (lift (wkn sub thin))           ...(substCong t (wknLift sub thin))
 wknSubst (App t u) sub thin =
   cong2 App (wknSubst t sub thin) (wknSubst u sub thin)
 wknSubst Zero sub thin =
@@ -195,163 +142,125 @@ wknSubst (Rec t u v) sub thin =
 
 export
 substWkn :
-  (t : Term ctx ty) ->
+  (t : Term ty ctx) ->
+  (sub : Subst Term ctx' ctx'') ->
   (thin : ctx `Thins` ctx') ->
-  (sub : Terms ctx'' ctx') ->
   subst (wkn t thin) sub = subst t (restrict sub thin)
-substWkn (Var i) thin sub =
-  sym (indexRestrict thin sub i)
-substWkn (Abs t) thin sub =
-  cong Abs $ Calc $
-    |~ subst (wkn t $ Keep thin) (wknAll sub (Drop id) :< Var Here)
-    ~~ subst t (restrict (wknAll sub (Drop id)) thin :< Var Here)
-      ...(substWkn t (Keep thin) (wknAll sub (Drop id) :< Var Here))
-    ~~ subst t (wknAll (restrict sub thin) (Drop id) :< Var Here)
-      ...(cong (subst t . (:< Var Here)) $ wknAllRestrict thin sub (Drop id))
-substWkn (App t u) thin sub =
-  cong2 App (substWkn t thin sub) (substWkn u thin sub)
-substWkn Zero thin sub =
-  Refl
-substWkn (Suc t) thin sub =
-  cong Suc (substWkn t thin sub)
-substWkn (Rec t u v) thin sub =
-  cong3 Rec (substWkn t thin sub) (substWkn u thin sub) (substWkn v thin sub)
-
-namespace Equiv
-  public export
-  data Equiv : Terms ctx' ctx -> Terms ctx' ctx -> Type where
-    Base : Equiv (Base (Keep thin)) (Base (Drop thin) :< Var Here)
-    WknAll :
-      (len : Len ctx) =>
-      Equiv sub sub' ->
-      Equiv
-        (wknAll sub (Drop $ id @{len}) :< Var Here)
-        (wknAll sub' (Drop $ id @{len}) :< Var Here)
-
-  %name Equiv prf
-
-indexCong : Equiv sub sub' -> (i : Elem ty ctx) -> index sub i = index sub' i
-indexCong Base Here = Refl
-indexCong Base (There i) = Refl
-indexCong (WknAll prf) Here = Refl
-indexCong (WknAll {sub, sub'} prf) (There i) = Calc $
-  |~ index (wknAll sub (Drop id)) i
-  ~~ wkn (index sub i) (Drop id)     ...(indexWknAll sub (Drop id) i)
-  ~~ wkn (index sub' i) (Drop id)    ...(cong (flip wkn (Drop id)) $ indexCong prf i)
-  ~~ index (wknAll sub' (Drop id)) i ...(sym $ indexWknAll sub' (Drop id) i)
-
-substCong :
-  (len : Len ctx') =>
-  (t : Term ctx ty) ->
-  {0 sub, sub' : Terms ctx' ctx} ->
-  Equiv sub sub' ->
-  subst t sub = subst t sub'
-substCong (Var i) prf = indexCong prf i
-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)
-substCong (Rec t u v) prf = cong3 Rec (substCong t prf) (substCong u prf) (substCong v prf)
-
-substBase : (t : Term ctx ty) -> (thin : ctx `Thins` ctx') -> subst t (Base thin) = wkn t thin
-substBase (Var i) thin = Refl
-substBase (Abs t) thin =
-  rewrite identityLeft thin in
-  cong Abs $ Calc $
-    |~ subst t (Base (Drop thin) :< Var Here)
-    ~~ subst t (Base $ Keep thin)             ...(sym $ substCong t Base)
-    ~~ wkn t (Keep thin)                      ...(substBase t (Keep thin))
-substBase (App t u) thin = cong2 App (substBase t thin) (substBase u thin)
-substBase Zero thin = Refl
-substBase (Suc t) thin = cong Suc (substBase t thin)
-substBase (Rec t u v) thin = cong3 Rec (substBase t thin) (substBase u thin) (substBase v thin)
-
--- Substitution Composition
-
-indexComp :
-  (sub1 : Terms ctx' ctx) ->
-  (sub2 : Terms ctx'' ctx') ->
-  (i : Elem ty ctx) ->
-  index (sub2 . sub1) i = subst (index sub1 i) sub2
-indexComp (Base thin) sub2 i = indexRestrict thin sub2 i
-indexComp (sub1 :< t) sub2 Here = Refl
-indexComp (sub1 :< t) sub2 (There i) = indexComp sub1 sub2 i
-
-wknAllComp :
-  (sub1 : Terms ctx' ctx) ->
-  (sub2 : Terms ctx'' ctx') ->
-  (thin : ctx'' `Thins` ctx''') ->
-  wknAll sub2 thin . sub1 = wknAll (sub2 . sub1) thin
-wknAllComp (Base thin') sub2 thin = wknAllRestrict thin' sub2 thin
-wknAllComp (sub1 :< t) sub2 thin =
-  cong2 (:<)
-    (wknAllComp sub1 sub2 thin)
-    (sym $ wknSubst t sub2 thin)
-
-compDrop :
-  (sub1 : Terms ctx' ctx) ->
-  (thin : ctx' `Thins` ctx'') ->
-  (sub2 : Terms ctx''' ctx'') ->
-  sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
-compDrop (Base thin') thin sub2 = restrictHomo sub2 thin thin'
-compDrop (sub1 :< t) thin sub2 = cong2 (:<) (compDrop sub1 thin sub2) (substWkn t thin sub2)
-
-export
-compWknAll :
-  (sub1 : Terms ctx' ctx) ->
-  (sub2 : Terms ctx''' ctx'') ->
-  (thin : ctx' `Thins` ctx'') ->
-  sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
-compWknAll (Base thin') sub2 thin = restrictHomo sub2 thin thin'
-compWknAll (sub1 :< t) sub2 thin = cong2 (:<) (compWknAll sub1 sub2 thin) (substWkn t thin sub2)
-
-export
-baseComp :
-  (thin : ctx' `Thins` ctx'') ->
-  (sub : Terms ctx' ctx) ->
-  Base thin . sub = wknAll sub thin
-baseComp thin (Base thin') = Refl
-baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin)
-
--- Substitution
-
-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 identitySquared len in
-  cong Abs $ trans (sym $ substCong t Base) (substId t)
-substId (App t u) = cong2 App (substId t) (substId u)
-substId Zero = Refl
-substId (Suc t) = cong Suc (substId t)
-substId (Rec t u v) = cong3 Rec (substId t) (substId u) (substId v)
-
-export
-substHomo :
-  (t : Term ctx ty) ->
-  (sub1 : Terms ctx' ctx) ->
-  (sub2 : Terms ctx'' ctx') ->
-  subst (subst t sub1) sub2 = subst t (sub2 . sub1)
-substHomo (Var i) sub1 sub2 =
-  sym $ indexComp sub1 sub2 i
-substHomo (Abs t) sub1 sub2 =
+substWkn (Var i) sub thin =
+  indexRestrict sub thin i
+substWkn (Abs t) sub thin =
   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))
-      ...(substHomo 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)
-      ...(Refl)
-    ~~ subst t (restrict (wknAll sub2 (Drop id)) id . sub1 :< Var Here)
-      ...(cong (subst t . (:< Var Here)) $ compDrop sub1 (Drop id) (wknAll sub2 (Drop id) :< Var Here))
-    ~~ subst t (wknAll sub2 (Drop id) . sub1 :< Var Here)
-      ...(cong (subst t . (:< Var Here) . (. sub1)) $ restrictId (wknAll sub2 (Drop id)))
-    ~~ subst t (wknAll (sub2 . sub1) (Drop id) :< Var Here)
-      ...(cong (subst t . (:< Var Here)) $ wknAllComp sub1 sub2 (Drop id))
-substHomo (App t u) sub1 sub2 =
-  cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2)
-substHomo Zero sub1 sub2 =
+    |~ subst (wkn t (keep thin _)) (lift sub)
+    ~~ subst t (restrict (lift sub) (keep thin _)) ...(substWkn t (lift sub) (keep thin _))
+    ~~ subst t (lift (restrict sub thin))          ...(substCong t (restrictLift sub thin))
+substWkn (App t u) sub thin =
+  cong2 App (substWkn t sub thin) (substWkn u sub thin)
+substWkn Zero sub thin =
   Refl
-substHomo (Suc t) sub1 sub2 =
-  cong Suc (substHomo t sub1 sub2)
-substHomo (Rec t u v) sub1 sub2 =
-  cong3 Rec (substHomo t sub1 sub2) (substHomo u sub1 sub2) (substHomo v sub1 sub2)
+substWkn (Suc t) sub thin =
+  cong Suc (substWkn t sub thin)
+substWkn (Rec t u v) sub thin =
+  cong3 Rec (substWkn t sub thin) (substWkn u sub thin) (substWkn v sub thin)
+
+-- -- substBase : (t : Term ctx ty) -> (thin : ctx `Thins` ctx') -> subst t (Base thin) = wkn t thin
+-- -- substBase (Var i) thin = Refl
+-- -- substBase (Abs t) thin =
+-- --   rewrite identityLeft thin in
+-- --   cong Abs $ Calc $
+-- --     |~ subst t (Base (Drop thin) :< Var Here)
+-- --     ~~ subst t (Base $ Keep thin)             ...(sym $ substCong t Base)
+-- --     ~~ wkn t (Keep thin)                      ...(substBase t (Keep thin))
+-- -- substBase (App t u) thin = cong2 App (substBase t thin) (substBase u thin)
+-- -- substBase Zero thin = Refl
+-- -- substBase (Suc t) thin = cong Suc (substBase t thin)
+-- -- substBase (Rec t u v) thin = cong3 Rec (substBase t thin) (substBase u thin) (substBase v thin)
+
+-- -- -- Substitution Composition
+
+-- -- indexComp :
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (sub2 : Terms ctx'' ctx') ->
+-- --   (i : Elem ty ctx) ->
+-- --   index (sub2 . sub1) i = subst (index sub1 i) sub2
+-- -- indexComp (Base thin) sub2 i = indexRestrict thin sub2 i
+-- -- indexComp (sub1 :< t) sub2 Here = Refl
+-- -- indexComp (sub1 :< t) sub2 (There i) = indexComp sub1 sub2 i
+
+-- -- wknAllComp :
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (sub2 : Terms ctx'' ctx') ->
+-- --   (thin : ctx'' `Thins` ctx''') ->
+-- --   wknAll sub2 thin . sub1 = wknAll (sub2 . sub1) thin
+-- -- wknAllComp (Base thin') sub2 thin = wknAllRestrict thin' sub2 thin
+-- -- wknAllComp (sub1 :< t) sub2 thin =
+-- --   cong2 (:<)
+-- --     (wknAllComp sub1 sub2 thin)
+-- --     (sym $ wknSubst t sub2 thin)
+
+-- -- compDrop :
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (thin : ctx' `Thins` ctx'') ->
+-- --   (sub2 : Terms ctx''' ctx'') ->
+-- --   sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
+-- -- compDrop (Base thin') thin sub2 = restrictHomo sub2 thin thin'
+-- -- compDrop (sub1 :< t) thin sub2 = cong2 (:<) (compDrop sub1 thin sub2) (substWkn t thin sub2)
+
+-- -- export
+-- -- compWknAll :
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (sub2 : Terms ctx''' ctx'') ->
+-- --   (thin : ctx' `Thins` ctx'') ->
+-- --   sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
+-- -- compWknAll (Base thin') sub2 thin = restrictHomo sub2 thin thin'
+-- -- compWknAll (sub1 :< t) sub2 thin = cong2 (:<) (compWknAll sub1 sub2 thin) (substWkn t thin sub2)
+
+-- -- export
+-- -- baseComp :
+-- --   (thin : ctx' `Thins` ctx'') ->
+-- --   (sub : Terms ctx' ctx) ->
+-- --   Base thin . sub = wknAll sub thin
+-- -- baseComp thin (Base thin') = Refl
+-- -- baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin)
+
+-- -- -- Substitution
+
+-- -- 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 identitySquared len in
+-- --   cong Abs $ trans (sym $ substCong t Base) (substId t)
+-- -- substId (App t u) = cong2 App (substId t) (substId u)
+-- -- substId Zero = Refl
+-- -- substId (Suc t) = cong Suc (substId t)
+-- -- substId (Rec t u v) = cong3 Rec (substId t) (substId u) (substId v)
+
+-- -- export
+-- -- substHomo :
+-- --   (t : Term ctx ty) ->
+-- --   (sub1 : Terms ctx' ctx) ->
+-- --   (sub2 : Terms ctx'' ctx') ->
+-- --   subst (subst t sub1) sub2 = subst t (sub2 . sub1)
+-- -- substHomo (Var i) sub1 sub2 =
+-- --   sym $ indexComp sub1 sub2 i
+-- -- substHomo (Abs t) sub1 sub2 =
+-- --   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))
+-- --       ...(substHomo 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)
+-- --       ...(Refl)
+-- --     ~~ subst t (restrict (wknAll sub2 (Drop id)) id . sub1 :< Var Here)
+-- --       ...(cong (subst t . (:< Var Here)) $ compDrop sub1 (Drop id) (wknAll sub2 (Drop id) :< Var Here))
+-- --     ~~ subst t (wknAll sub2 (Drop id) . sub1 :< Var Here)
+-- --       ...(cong (subst t . (:< Var Here) . (. sub1)) $ restrictId (wknAll sub2 (Drop id)))
+-- --     ~~ subst t (wknAll (sub2 . sub1) (Drop id) :< Var Here)
+-- --       ...(cong (subst t . (:< Var Here)) $ wknAllComp sub1 sub2 (Drop id))
+-- -- substHomo (App t u) sub1 sub2 =
+-- --   cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2)
+-- -- substHomo Zero sub1 sub2 =
+-- --   Refl
+-- -- substHomo (Suc t) sub1 sub2 =
+-- --   cong Suc (substHomo t sub1 sub2)
+-- -- substHomo (Rec t u v) sub1 sub2 =
+-- --   cong3 Rec (substHomo t sub1 sub2) (substHomo u sub1 sub2) (substHomo v sub1 sub2)
-- 
cgit v1.2.3