Prove weakening of type judgements.

This is a huge commit that has many more changes. I should split
this up later.

7 files changed, 505 insertions, 31 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 1292fc9..2afceaa 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -1,6 +1,7 @@
 module Core.Declarative
 
 import Core.Environment
+import Core.Environment.Extension
 import Core.Term
 import Core.Term.Substitution
 import Core.Term.Thinned
@@ -82,7 +83,7 @@ data TermWf where
     TermWf env t (Pi a b) ->
     TermWf env u a ->
     ---
-    TermWf env (App t u) (subst b $ Wkn (id _) :< pure u)
+    TermWf env (App t u) (subst1 b u)
   ConvWf :
     TermWf env t a ->
     TypeConv env a b ->
@@ -107,7 +108,7 @@ data TermConv where
     TermConv env f g (Pi a b) ->
     TermConv env t u a ->
     ---
-    TermConv env (App f t) (App g u) (subst b $ Wkn (id _) :< pure t)
+    TermConv env (App f t) (App g u) (subst1 b t)
   PiTmConv :
     TypeWf env a ->
     TermConv env a c Set ->
@@ -129,10 +130,7 @@ data TermConv where
     TermWf (env :< pure a) t b ->
     TermWf env u a ->
     ---
-    TermConv env
-      (App (Abs t) u)
-      (subst t $ Wkn (id _) :< pure u)
-      (subst g $ Wkn (id _) :< pure u)
+    TermConv env (App (Abs t) u) (subst1 t u) (subst1 b u)
   ConvConv :
     TermConv env t u a ->
     TypeConv env a b ->
@@ -269,3 +267,133 @@ termConvImpliesEnvWf (PiTmConv tyWf tmConv tmConv1) = termConvImpliesEnvWf tmCon
 termConvImpliesEnvWf (PiEta tyWf tmWf tmWf1 tmConv) = termWfImpliesEnvWf tmWf
 termConvImpliesEnvWf (PiBeta tyWf tmWf tmWf1) = typeWfImpliesEnvWf tyWf
 termConvImpliesEnvWf (ConvConv tmConv tyConv) = termConvImpliesEnvWf tmConv
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+record ExtendsWf (0 thin : m `Thins` n) (0 env2 : Env n) (0 env1 : Env m) where
+  constructor MkExtWf
+  ext : Extends thin env2 env1
+  wf : EnvWf env2
+
+%name ExtendsWf extWf
+
+wknPiEta :
+  (t : Term m) ->
+  (thin : m `Thins` n) ->
+  wkn (App (wkn t (wkn1 m)) (Var 0)) (keep thin) =
+  App (wkn (wkn t thin) (wkn1 n)) (Var 0)
+wknPiEta t thin = cong2 App (sym $ wkn1Comm t thin) (cong Var $ wknKeepFZ thin)
+
+export
+weakenTypeWf :
+  TypeWf env1 a ->
+  ExtendsWf thin env2 env1 ->
+  TypeWf env2 (wkn a thin)
+export
+weakenTypeConv :
+  TypeConv env1 a b ->
+  ExtendsWf thin env2 env1 ->
+  TypeConv env2 (wkn a thin) (wkn b thin)
+export
+weakenTermWf :
+  TermWf env1 t a ->
+  ExtendsWf thin env2 env1 ->
+  TermWf env2 (wkn t thin) (wkn a thin)
+export
+weakenTermConv :
+  TermConv env1 t u a ->
+  ExtendsWf thin env2 env1 ->
+  TermConv env2 (wkn t thin) (wkn u thin) (wkn a thin)
+
+weakenTypeWf (SetTyWf envWf) extWf = SetTyWf extWf.wf
+weakenTypeWf (PiTyWf {a} tyWf tyWf1) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  PiTyWf tyWf
+    (typeWfRespEq
+      (weakenTypeWf tyWf1 $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTypeWf (LiftWf tmWf) extWf = LiftWf (weakenTermWf tmWf extWf)
+
+weakenTypeConv (ReflTy tyWf) extWf = ReflTy (weakenTypeWf tyWf extWf)
+weakenTypeConv (SymTy tyConv) extWf = SymTy (weakenTypeConv tyConv extWf)
+weakenTypeConv (TransTy tyConv tyConv1) extWf =
+  TransTy
+    (weakenTypeConv tyConv extWf)
+    (weakenTypeConv tyConv1 extWf)
+weakenTypeConv (PiConv {a} tyWf tyConv tyConv1) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  PiConv tyWf
+    (weakenTypeConv tyConv extWf)
+    (typeConvRespEq
+      (weakenTypeConv tyConv1 $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTypeConv (LiftConv tmConv) extWf = LiftConv (weakenTermConv tmConv extWf)
+
+weakenTermWf (PiTmWf {a} tmWf tmWf1) extWf =
+  let tmWf = weakenTermWf tmWf extWf in
+  PiTmWf tmWf
+    (termWfRespEq
+      (weakenTermWf tmWf1 $ MkExtWf (Keep' extWf.ext) (extWf.wf :< LiftWf tmWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTermWf (VarWf {i} envWf) extWf =
+  rewrite sym $ expandHomo (index env1 i) thin in
+  rewrite sym $ indexHomo extWf.ext i in
+  VarWf extWf.wf
+weakenTermWf (AbsWf {a} tyWf tmWf) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  AbsWf tyWf
+    (termWfRespEq
+      (weakenTermWf tmWf $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTermWf (AppWf {b, u} tmWf tmWf1) extWf =
+  rewrite wknSubst1 b u thin in
+  AppWf
+    (weakenTermWf tmWf extWf)
+    (weakenTermWf tmWf1 extWf)
+weakenTermWf (ConvWf tmWf tyConv) extWf =
+  ConvWf
+    (weakenTermWf tmWf extWf)
+    (weakenTypeConv tyConv extWf)
+
+weakenTermConv (ReflTm tmWf) extWf = ReflTm (weakenTermWf tmWf extWf)
+weakenTermConv (SymTm tmConv) extWf = SymTm (weakenTermConv tmConv extWf)
+weakenTermConv (TransTm tmConv tmConv1) extWf =
+  TransTm
+    (weakenTermConv tmConv extWf)
+    (weakenTermConv tmConv1 extWf)
+weakenTermConv (AppConv {b, t} tmConv tmConv1) extWf =
+  rewrite wknSubst1 b t thin in
+  AppConv
+    (weakenTermConv tmConv extWf)
+    (weakenTermConv tmConv1 extWf)
+weakenTermConv (PiTmConv {a} tyWf tmConv tmConv1) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  PiTmConv tyWf
+    (weakenTermConv tmConv extWf)
+    (termConvRespEq
+      (weakenTermConv tmConv1 $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTermConv (PiEta {a, t, u} tyWf tmWf tmWf1 tmConv) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  PiEta tyWf
+    (weakenTermWf tmWf extWf)
+    (weakenTermWf tmWf1 extWf)
+    (termConvRespEq
+      (rewrite sym $ wknPiEta t thin in
+       rewrite sym $ wknPiEta u thin in
+       weakenTermConv tmConv $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+weakenTermConv (PiBeta {a, b, t, u} tyWf tmWf tmWf1) extWf =
+  let tyWf = weakenTypeWf tyWf extWf in
+  rewrite wknSubst1 t u thin in
+  rewrite wknSubst1 b u thin in
+  PiBeta tyWf
+    (termWfRespEq
+      (weakenTermWf tmWf $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf))
+      (Refl :< sym (wknId $ wkn a thin)))
+    (weakenTermWf tmWf1 extWf)
+weakenTermConv (ConvConv tmConv tyConv) extWf =
+  ConvConv
+    (weakenTermConv tmConv extWf)
+    (weakenTypeConv tyConv extWf)
diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr
index f13cde3..cdf58b7 100644
--- a/src/Core/Environment.idr
+++ b/src/Core/Environment.idr
@@ -26,8 +26,8 @@ namespace Eq
 
 public export
 index : Env n -> Fin n -> Thinned n
-index (env :< t) FZ = wkn t (drop $ id _)
-index (env :< t) (FS i) = wkn (index env i) (drop $ id _)
+index (env :< t) FZ = wkn t (wkn1 _)
+index (env :< t) (FS i) = wkn (index env i) (wkn1 _)
 
 export
 indexCong :
@@ -36,5 +36,5 @@ indexCong :
   (i : Fin n) ->
   index env1 i =~= index env2 i
 indexCong Refl i = Refl
-indexCong (prf :< prf') FZ = wknCong prf' (drop $ id _)
-indexCong (prf :< prf') (FS i) = wknCong (indexCong prf i) (drop $ id _)
+indexCong (prf :< prf') FZ = wknCong prf' (wkn1 _)
+indexCong (prf :< prf') (FS i) = wknCong (indexCong prf i) (wkn1 _)
diff --git a/src/Core/Environment/Extension.idr b/src/Core/Environment/Extension.idr
index 9914697..9520809 100644
--- a/src/Core/Environment/Extension.idr
+++ b/src/Core/Environment/Extension.idr
@@ -1,22 +1,31 @@
 module Core.Environment.Extension
 
 import Core.Environment
+import Core.Term
 import Core.Term.Thinned
 import Core.Thinning
 
+import Syntax.PreorderReasoning
+
 -- Definition ------------------------------------------------------------------
 
 public export
 data Extends : m `Thins` n -> Env n -> Env m -> Type where
   Id : Extends (id n) env env
-  Drop : Extends thin env1 env2 -> Extends (drop thin) (env1 :< a) env2
-  Keep : Extends thin env1 env2 -> Extends (keep thin) (env1 :< wkn a thin) (env2 :< a)
+  Drop : Extends thin env2 env1 -> Extends (drop thin) (env2 :< a) env1
+  Keep : Extends thin env2 env1 -> Extends (keep thin) (env2 :< wkn a thin) (env1 :< a)
 
 %name Extends ext
 
+-- Smart Constructor -----------------------------------------------------------
+
+export
+Keep' : Extends thin env1 env2 -> Extends (keep thin) (env1 :< (a `Over` thin)) (env2 :< pure a)
+Keep' ext = rewrite sym $ cong (a `Over`) $ compRightId thin in Keep ext
+
 -- Composition -----------------------------------------------------------------
 
-public export
+export
 (.) : Extends thin2 env3 env2 -> Extends thin1 env2 env1 -> Extends (thin2 . thin1) env3 env1
 Id . ext1 =
   rewrite compLeftId thin1 in
@@ -34,3 +43,30 @@ Keep {thin = thin2} ext2 . Keep {thin = thin1, a} ext1 =
   rewrite compKeep thin2 thin1 in
   rewrite wknHomo a thin1 thin2 in
   Keep (ext2 . ext1)
+
+-- Indexing --------------------------------------------------------------------
+
+export
+indexHomo :
+  Extends thin env2 env1 ->
+  (i : Fin m) ->
+  index env2 (wkn i thin) = wkn (index env1 i) thin
+indexHomo Id i = Calc $
+  |~ index env1 (wkn i $ id m)
+  ~~ index env1 i              ...(cong (index env1) $ wknId i)
+  ~~ wkn (index env1 i) (id m) ...(sym $ wknId (index env1 i))
+indexHomo (Drop {thin, env2, env1, a} ext) i = Calc $
+  |~ index (env2 :< a) (wkn i $ drop thin)
+  ~~ wkn (index env2 (wkn i thin)) (wkn1 _) ...(cong (index $ env2 :< a) $ wknDrop i thin)
+  ~~ wkn (wkn (index env1 i) thin) (wkn1 _) ...(cong (flip wkn (wkn1 _)) $ indexHomo ext i)
+  ~~ wkn (index env1 i) (wkn1 _ . thin)     ...(wknHomo (index env1 i) thin (wkn1 _))
+  ~~ wkn (index env1 i) (drop thin)         ...(cong (wkn (index env1 i)) $ compLeftWkn1 thin)
+indexHomo (Keep {thin, env2, env1, a} ext) FZ = Calc $
+  |~ index (env2 :< wkn a thin) (wkn FZ $ keep thin)
+  ~~ wkn (wkn a thin) (wkn1 _)                       ...(cong (index $ env2 :< wkn a thin) $ wknKeepFZ thin)
+  ~~ wkn (wkn a (wkn1 _)) (keep thin)                ...(wkn1Comm a thin)
+indexHomo (Keep {thin, env2, env1, a} ext) (FS i) = Calc $
+  |~ index (env2 :< wkn a thin) (wkn (FS i) $ keep thin)
+  ~~ wkn (index env2 $ wkn i thin) (wkn1 _)              ...(cong (index $ env2 :< wkn a thin) $ wknKeepFS i thin)
+  ~~ wkn (wkn (index env1 i) thin) (wkn1 _)              ...(cong (flip wkn (wkn1 _)) $ indexHomo ext i)
+  ~~ wkn (wkn (index env1 i) (wkn1 _)) (keep thin)       ...(wkn1Comm (index env1 i) thin)
diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index 74ef7af..a3ddac5 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -4,6 +4,8 @@ import Core.Thinning
 
 import public Data.Fin
 
+import Syntax.PreorderReasoning
+
 -- Definition ------------------------------------------------------------------
 
 public export
@@ -29,6 +31,14 @@ wkn (Abs t) thin = Abs (wkn t $ keep thin)
 wkn (App t u) thin = App (wkn t thin) (wkn u thin)
 
 export
+wknId : (t : Term n) -> wkn t (id n) = t
+wknId (Var i) = cong Var (wknId i)
+wknId Set = Refl
+wknId (Pi t u) = cong2 Pi (wknId t) (trans (cong (wkn u) $ keepIdIsId n) (wknId u))
+wknId (Abs t) = cong Abs (trans (cong (wkn t) $ keepIdIsId n) (wknId t))
+wknId (App t u) = cong2 App (wknId t) (wknId u)
+
+export
 wknHomo :
   (t : Term k) ->
   (thin1 : k `Thins` m) ->
@@ -48,3 +58,14 @@ wknHomo (Abs t) thin1 thin2 =
       (wknHomo t (keep thin1) (keep thin2))
       (cong (wkn t) $ compKeep thin2 thin1))
 wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
+
+export
+wkn1Comm :
+  (t : Term m) ->
+  (thin : m `Thins` n) ->
+  wkn (wkn t thin) (wkn1 n) = wkn (wkn t $ wkn1 m) (keep thin)
+wkn1Comm t thin = Calc $
+  |~ wkn (wkn t thin) (wkn1 n)
+  ~~ wkn t (wkn1 n . thin)            ...(wknHomo t thin (wkn1 n))
+  ~~ wkn t (keep thin . wkn1 m)       ...(sym $ cong (wkn t) $ wkn1Comm thin)
+  ~~ wkn (wkn t $ wkn1 m) (keep thin) ...(sym $ wknHomo t (wkn1 m) (keep thin))
diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr
index abeb487..c14c652 100644
--- a/src/Core/Term/Substitution.idr
+++ b/src/Core/Term/Substitution.idr
@@ -4,6 +4,8 @@ import Core.Term
 import Core.Term.Thinned
 import Core.Thinning
 
+import Syntax.PreorderReasoning
+
 infix 4 =~=
 
 -- Definition ------------------------------------------------------------------
@@ -22,6 +24,81 @@ namespace Eq
 %name Subst sub
 %name Eq.(=~=) prf
 
+-- Weakening -------------------------------------------------------------------
+
+public export
+wkn : Subst k m -> m `Thins` n -> Subst k n
+wkn (Wkn thin') thin = Wkn (thin . thin')
+wkn (sub :< t) thin = wkn sub thin :< wkn t thin
+
+export
+wknCong :
+  {0 sub1, sub2 : Subst k m} ->
+  sub1 =~= sub2 ->
+  (thin : m `Thins` n) ->
+  wkn sub1 thin =~= wkn sub2 thin
+wknCong Refl thin = Refl
+wknCong (prf :< prf') thin = wknCong prf thin :< wknCong prf' thin
+
+export
+wknHomo :
+  (sub : Subst j k) ->
+  (thin1 : k `Thins` m) ->
+  (thin2 : m `Thins` n) ->
+  wkn (wkn sub thin1) thin2 = wkn sub (thin2 . thin1)
+wknHomo (Wkn thin) thin1 thin2 = cong Wkn (compAssoc thin2 thin1 thin)
+wknHomo (sub :< t) thin1 thin2 = cong2 (:<) (wknHomo sub thin1 thin2) (wknHomo t thin1 thin2)
+
+-- Composition -----------------------------------------------------------------
+
+export
+(.) : Subst m n -> k `Thins` m -> Subst k n
+comp : Subst m n -> Thinned n -> {0 thin : k `Thins` S m} -> View thin -> Subst k n
+
+Wkn thin1 . thin = Wkn (thin1 . thin)
+(sub :< t) . thin = comp sub t (view thin)
+
+comp sub t (Id (S m)) = sub :< t
+comp sub t (Drop thin) = sub . thin
+comp sub t (Keep thin) = (sub . thin) :< t
+
+export
+compId : (sub : Subst m n) -> sub . id m = sub
+compId (Wkn thin) = cong Wkn (compRightId thin)
+compId (sub :< t) = viewId m (\v => comp sub t v = sub :< t) Refl
+
+export
+compKeep :
+  (sub : Subst m n) ->
+  (t : Thinned n) ->
+  (thin : k `Thins` m) ->
+  (sub :< t) . keep thin = (sub . thin) :< t
+compKeep sub t thin =
+  viewKeep thin (\v => comp sub t v = (sub . thin) :< t)
+    (\Refl, Refl => sym $ cong (:< t) $ compId sub)
+    Refl
+
+export
+wknComp :
+  (sub : Subst k m) ->
+  (thin1 : j `Thins` k) ->
+  (thin2 : m `Thins` n) ->
+  wkn (sub . thin1) thin2 = wkn sub thin2 . thin1
+wknComp' :
+  (sub : Subst k m) ->
+  (t : Thinned m) ->
+  {0 thin1 : j `Thins` S k} ->
+  (v : View thin1) ->
+  (thin2 : m `Thins` n) ->
+  wkn (comp sub t v) thin2 = comp (wkn sub thin2) (wkn t thin2) v
+
+wknComp (Wkn thin) thin1 thin2 = cong Wkn (compAssoc thin2 thin thin1)
+wknComp (sub :< t) thin1 thin2 = wknComp' sub t (view thin1) thin2
+
+wknComp' sub t (Id (S k)) thin2 = Refl
+wknComp' sub t (Drop thin1) thin2 = wknComp sub thin1 thin2
+wknComp' sub t (Keep thin1) thin2 = cong (:< wkn t thin2) (wknComp sub thin1 thin2)
+
 -- Indexing --------------------------------------------------------------------
 
 public export
@@ -40,27 +117,79 @@ indexCong Refl i = Refl
 indexCong (prf :< prf') FZ = prf'
 indexCong (prf :< prf') (FS i) = indexCong prf i
 
--- Weakening -------------------------------------------------------------------
-
-public export
-wkn : Subst k m -> m `Thins` n -> Subst k n
-wkn (Wkn thin') thin = Wkn (thin . thin')
-wkn (sub :< t) thin = wkn sub thin :< wkn t thin
-
 export
-wknCong :
-  {0 sub1, sub2 : Subst k m} ->
-  sub1 =~= sub2 ->
+indexHomo :
+  (sub : Subst k m) ->
   (thin : m `Thins` n) ->
-  wkn sub1 thin =~= wkn sub2 thin
-wknCong Refl thin = Refl
-wknCong (prf :< prf') thin = wknCong prf thin :< wknCong prf' thin
+  (i : Fin k) ->
+  index (wkn sub thin) i = wkn (index sub i) thin
+indexHomo (Wkn thin') thin i = Refl
+indexHomo (sub :< t) thin FZ = Refl
+indexHomo (sub :< t) thin (FS i) = indexHomo sub thin i
+
+export
+indexComp :
+  (sub : Subst m n) ->
+  (thin : k `Thins` m) ->
+  (i : Fin k) ->
+  index (sub . thin) i =~= index sub (wkn i thin)
+indexComp' :
+  (sub : Subst m n) ->
+  (t : Thinned n) ->
+  {0 thin : k `Thins` S m} ->
+  (v : View thin) ->
+  (i : Fin k) ->
+  index (comp sub t v) i =~= index (sub :< t) (wkn i thin)
+
+indexComp (Wkn thin1) thin i = sym $ cong Var $ wknHomo i thin thin1
+indexComp (sub :< t) thin i = indexComp' sub t (view thin) i
+
+indexComp' sub t (Id (S m)) i = rewrite wknId i in Refl
+indexComp' sub t (Drop thin) i = rewrite wknDrop i thin in indexComp sub thin i
+indexComp' sub t (Keep thin) FZ = rewrite wknKeepFZ thin in Refl
+indexComp' sub t (Keep thin) (FS i) = rewrite wknKeepFS i thin in indexComp sub thin i
 
 -- Constructors ----------------------------------------------------------------
 
 public export
+Refl' : {0 sub1, sub2 : Subst m n} -> sub1 = sub2 -> sub1 =~= sub2
+Refl' Refl = Refl
+
+public export
 lift : Subst m n -> Subst (S m) (S n)
-lift sub = wkn sub (drop $ id n) :< (Var 0 `Over` id (S n))
+lift sub = wkn sub (wkn1 n) :< pure (Var 0)
+
+export
+wknLift :
+  (sub : Subst k m) ->
+  (thin : m `Thins` n) ->
+  wkn (lift sub) (keep thin) =~= lift (wkn sub thin)
+wknLift sub thin =
+  let
+    eq1 : wkn (wkn sub (wkn1 m)) (keep thin) =~= wkn (wkn sub thin) (wkn1 n)
+    eq1 = Refl' $ Calc $
+      |~ wkn (wkn sub (wkn1 m)) (keep thin)
+      ~~ wkn sub (keep thin . wkn1 m)       ...(wknHomo sub (wkn1 m) (keep thin))
+      ~~ wkn sub (wkn1 n . thin)            ...(cong (wkn sub) $ wkn1Comm thin)
+      ~~ wkn (wkn sub thin) (wkn1 n)        ...(sym $ wknHomo sub thin (wkn1 n))
+    eq2 : (Var (wkn 0 (keep thin . id (S m))) = Var (wkn FZ (id $ S n)))
+    eq2 = cong Var $ Calc $
+      |~ wkn 0 (keep thin . id (S m))
+      ~~ wkn 0 (keep thin)            ...(cong (wkn 0) $ compRightId (keep thin))
+      ~~ 0                            ...(wknKeepFZ thin)
+      ~~ wkn 0 (id $ S n)             ...(sym $ wknId 0)
+  in
+  eq1 :< eq2
+
+export
+compLift :
+  (sub : Subst m n) ->
+  (thin : k `Thins` m) ->
+  lift sub . keep thin = lift (sub . thin)
+compLift sub thin = Calc $
+  |~ lift sub . keep thin
+  ~~ (wkn sub (wkn1 n) . thin) :< pure (Var 0) ...(compKeep (wkn sub (wkn1 n)) (pure $ Var 0) thin)
+  ~~ lift (sub . thin)                         ...(sym $ cong (:< pure (Var 0)) $ wknComp sub thin (wkn1 n))
 
 -- Substitution ----------------------------------------------------------------
 
@@ -72,6 +201,10 @@ subst (Pi t u) sub = Pi (subst t sub) (subst u $ lift sub)
 subst (Abs t) sub = Abs (subst t $ lift sub)
 subst (App t u) sub = App (subst t sub) (subst u sub)
 
+public export
+subst1 : Term (S n) -> Term n -> Term n
+subst1 t u = subst t (Wkn (id n) :< pure u)
+
 export
 substCong :
   (t : Term m) ->
@@ -83,6 +216,62 @@ substCong Set prf = Refl
 substCong (Pi t u) prf =
   cong2 Pi
     (substCong t prf)
-    (substCong u $ wknCong prf (drop $ id n) :< Refl)
-substCong (Abs t) prf = cong Abs (substCong t $ wknCong prf (drop $ id n) :< Refl)
+    (substCong u $ wknCong prf (wkn1 n) :< Refl)
+substCong (Abs t) prf = cong Abs (substCong t $ wknCong prf (wkn1 n) :< Refl)
 substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf)
+
+-- Interaction with Weakening
+
+export
+wknSubst :
+  (t : Term k) ->
+  (sub : Subst k m) ->
+  (thin : m `Thins` n) ->
+  wkn (subst t sub) thin = subst t (wkn sub thin)
+wknSubst (Var i) sub thin = sym $ Calc $
+  |~ expand (index (wkn sub thin) i)
+  ~~ expand (wkn (index sub i) thin) ...(cong expand $ indexHomo sub thin i)
+  ~~ wkn (expand (index sub i)) thin ...(expandHomo (index sub i) thin)
+wknSubst Set sub thin = Refl
+wknSubst (Pi t u) sub thin = cong2 Pi (wknSubst t sub thin) $ Calc $
+  |~ wkn (subst u $ lift sub) (keep thin)
+  ~~ subst u (wkn (lift sub) (keep thin)) ...(wknSubst u (lift sub) (keep thin))
+  ~~ subst u (lift $ wkn sub thin)        ...(substCong u $ wknLift sub thin)
+wknSubst (Abs t) sub thin = cong Abs $ Calc $
+  |~ wkn (subst t $ lift sub) (keep thin)
+  ~~ subst t (wkn (lift sub) (keep thin)) ...(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)
+
+export
+substWkn :
+  (t : Term k) ->
+  (thin : k `Thins` m) ->
+  (sub : Subst m n) ->
+  subst (wkn t thin) sub = subst t (sub . thin)
+
+substWkn (Var i) thin sub = sym (indexComp sub thin i)
+substWkn Set thin sub = Refl
+substWkn (Pi t u) thin sub = cong2 Pi (substWkn t thin sub) $ Calc $
+  |~ subst (wkn u (keep thin)) (lift sub)
+  ~~ subst u (lift sub . keep thin)       ...(substWkn u (keep thin) (lift sub))
+  ~~ subst u (lift (sub . thin))          ...(cong (subst u) $ compLift sub thin)
+substWkn (Abs t) thin sub = cong Abs $ Calc $
+  |~ subst (wkn t (keep thin)) (lift sub)
+  ~~ subst t (lift sub . keep thin)       ...(substWkn t (keep thin) (lift sub))
+  ~~ subst t (lift (sub . thin))          ...(cong (subst t) $ compLift sub thin)
+substWkn (App t u) thin sub = cong2 App (substWkn t thin sub) (substWkn u thin sub)
+
+export
+wknSubst1 :
+  (t : Term (S m)) ->
+  (u : Term m) ->
+  (thin : m `Thins` n) ->
+  wkn (subst1 t u) thin = subst1 (wkn t $ keep thin) (wkn u thin)
+wknSubst1 t u thin = Calc $
+  |~ wkn (subst t (Wkn (id m) :< pure u)) thin
+  ~~ subst t (Wkn (thin . id m) :< (u `Over` thin . id m))        ...(wknSubst t (Wkn (id m) :< pure u) thin)
+  ~~ subst t (Wkn thin :< (u `Over` thin))                        ...(cong (\thin => subst t (Wkn thin :< (u `Over` thin))) $ compRightId thin)
+  ~~ subst t (Wkn (id n . thin) :< pure (wkn u thin))             ...(sym $ substCong t (Refl' (cong Wkn $ compLeftId thin) :< wknId (wkn u thin)))
+  ~~ subst t ((Wkn (id n) :< pure (wkn u thin)) . keep thin)      ...(sym $ cong (subst t) $ compKeep (Wkn $ id n) (pure $ wkn u thin) thin)
+  ~~ subst (wkn t $ keep thin) (Wkn (id n) :< pure (wkn u thin))  ...(sym $ substWkn t (keep thin) (Wkn (id n) :< pure (wkn u thin)))
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr
index 3a06612..6a6c0ff 100644
--- a/src/Core/Term/Thinned.idr
+++ b/src/Core/Term/Thinned.idr
@@ -49,9 +49,33 @@ wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $
   ~~ wkn u (thin . thin2)   ...(wknHomo u thin2 thin)
 
 export
+wknId : (t : Thinned n) -> wkn t (id n) = t
+wknId (t `Over` thin) = cong (t `Over`) (compLeftId thin)
+
+export
 wknHomo :
   (t : Thinned k) ->
   (thin1 : k `Thins` m) ->
   (thin2 : m `Thins` n) ->
   wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
 wknHomo (t `Over` thin) thin1 thin2 = cong (t `Over`) (compAssoc thin2 thin1 thin)
+
+export
+wkn1Comm :
+  (t : Thinned m) ->
+  (thin : m `Thins` n) ->
+  wkn (wkn t thin) (wkn1 n) = wkn (wkn t $ wkn1 m) (keep thin)
+wkn1Comm (t `Over` thin') thin = cong (t `Over`) $ Calc $
+  |~ wkn1 n . (thin . thin')
+  ~~ drop (thin . thin')          ...(compLeftWkn1 (thin . thin'))
+  ~~ keep thin . drop thin'       ...(sym $ compRightDrop thin thin')
+  ~~ keep thin . (wkn1 m . thin') ...(sym $ cong (keep thin .) $ compLeftWkn1 thin')
+
+-- Interaction with Expansion
+
+export
+expandHomo :
+  (t : Thinned m) ->
+  (thin : m `Thins` n) ->
+  expand (wkn t thin) = wkn (expand t) thin
+expandHomo (t `Over` thin') thin = sym (wknHomo t thin' thin)
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index 51947e0..d56ada8 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -33,6 +33,16 @@ keep : m `Thins` n -> S m `Thins` S n
 keep IsId = IsId
 keep (IsThinner thin) = IsThinner (IsKeep thin)
 
+public export
+wkn1 : (0 n : Nat) -> n `Thins` S n
+wkn1 n = drop (id n)
+
+-- Properties
+
+export
+keepIdIsId : (0 n : Nat) -> keep (id n) = id (S n)
+keepIdIsId n = Refl
+
 -- Non-Identity ----------------------------------------------------------------
 
 export
@@ -49,6 +59,8 @@ data View : m `Thins` n -> Type where
   Drop : (thin : m `Thins` n) -> View (drop thin)
   Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
 
+%name Thinning.View view
+
 export
 view : (thin : m `Thins` n) -> View thin
 view IsId = Id m
@@ -56,6 +68,38 @@ view (IsThinner IsBase) = Drop (id _)
 view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
 view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
 
+-- Eliminators
+
+export
+viewId :
+  (0 n : Nat) ->
+  (0 p : View (id n) -> Type) ->
+  p (Id n) ->
+  p (view $ id n)
+viewId n p x = x
+
+export
+viewDrop :
+  (thin : m `Thins` n) ->
+  (0 p : View (drop thin) -> Type) ->
+  p (Drop thin) ->
+  p (view $ drop thin)
+viewDrop IsId p x = x
+viewDrop (IsThinner thin) p x = x
+
+export
+viewKeep :
+  forall m, n.
+  (thin : m `Thins` n) ->
+  (0 p : View (keep thin) -> Type) ->
+  ((eq1 : m = n) ->
+   (eq2 : thin = (rewrite eq1 in id n)) ->
+   p (rewrite eq2 in rewrite eq1 in Id (S n))) ->
+  ({auto 0 prf : IsNotId thin} -> p (Keep thin)) ->
+  p (view $ keep thin)
+viewKeep IsId p id keep = id Refl Refl
+viewKeep (IsThinner thin) p id keep = keep
+
 -- Composition -----------------------------------------------------------------
 
 comp : Thinner m n -> Thinner k m -> Thinner k n
@@ -119,7 +163,6 @@ compLeftDrop IsId (IsThinner thin1) = Refl
 compLeftDrop (IsThinner thin2) IsId = Refl
 compLeftDrop (IsThinner thin2) (IsThinner thin1) = Refl
 
-
 export
 compRightDrop :
   (thin2 : m `Thins` n) ->
@@ -138,6 +181,18 @@ compKeep IsId thin2 = Refl
 compKeep (IsThinner thin1) IsId = Refl
 compKeep (IsThinner thin1) (IsThinner thin2) = Refl
 
+export
+compLeftWkn1 : (thin : m `Thins` n) -> wkn1 n . thin = drop thin
+compLeftWkn1 thin = trans (compLeftDrop (id n) thin) (cong drop $ compLeftId thin)
+
+export
+compRightWkn1 : (thin : m `Thins` n) -> keep thin . wkn1 m = drop thin
+compRightWkn1 thin = trans (compRightDrop thin (id m)) (cong drop $ compRightId thin)
+
+export
+wkn1Comm : (thin : m `Thins` n) -> keep thin . wkn1 m = wkn1 n . thin
+wkn1Comm thin = trans (compRightWkn1 thin) (sym $ compLeftWkn1 thin)
+
 -- Weakening -------------------------------------------------------------------
 
 wkn' : Fin m -> Thinner m n -> Fin n
@@ -151,7 +206,11 @@ wkn : Fin m -> m `Thins` n -> Fin n
 wkn i IsId = i
 wkn i (IsThinner thin) = wkn' i thin
 
--- Properties
+-- Categorical
+
+export
+wknId : (i : Fin n) -> wkn i (id n) = i
+wknId i = Refl
 
 wkn'Homo :
   (i : Fin k) ->
@@ -174,3 +233,20 @@ wknHomo :
 wknHomo i IsId thin2 = sym $ cong (wkn i) $ compRightId thin2
 wknHomo i (IsThinner thin1) IsId = Refl
 wknHomo i (IsThinner thin1) (IsThinner thin2) = wkn'Homo i thin2 thin1
+
+-- Specific Cases
+
+export
+wknDrop : (i : Fin m) -> (thin : m `Thins` n) -> wkn i (drop thin) = FS (wkn i thin)
+wknDrop i IsId = Refl
+wknDrop i (IsThinner thin) = Refl
+
+export
+wknKeepFZ : (thin : m `Thins` n) -> wkn 0 (keep thin) = 0
+wknKeepFZ IsId = Refl
+wknKeepFZ (IsThinner thin) = Refl
+
+export
+wknKeepFS : (i : Fin m) -> (thin : m `Thins` n) -> wkn (FS i) (keep thin) = FS (wkn i thin)
+wknKeepFS i IsId = Refl
+wknKeepFS i (IsThinner thin) = Refl