Prove term weakening respects identities.

1 files changed, 20 insertions, 0 deletions

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index 182e1ea..7e1a91c 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -32,6 +32,26 @@ wkn (Pi n t u) thin = Pi n (wkn t thin) (wkn u $ keep thin n)
 wkn (Abs n t) thin = Abs n (wkn t $ keep thin n)
 wkn (App t u) thin = App (wkn t thin) (wkn u thin)
 
+-- Respects Identity
+
+export
+wknId : (t : Term sx) -> wkn t (id sx) = t
+wknId (Var i) = cong Var (wknId i)
+wknId Set = Refl
+wknId (Pi n t u) =
+  cong2 (Pi n) (wknId t) $
+  Calc $
+  |~ wkn u (keep (id sx) n)
+  ~~ wkn u (id $ sx :< n)   ...(cong (wkn u) $ keepIdIsId sx n)
+  ~~ u                      ...(wknId u)
+wknId (Abs n t) =
+  cong (Abs n) $
+  Calc $
+  |~ wkn t (keep (id sx) n)
+  ~~ wkn t (id $ sx :< n)   ...(cong (wkn t) $ keepIdIsId sx n)
+  ~~ t                      ...(wknId t)
+wknId (App t u) = cong2 App (wknId t) (wknId u)
+
 -- Is Homomorphic
 
 export