From 670ab78c2033198a33f1e24e8ce84a697cab5243 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 7 Apr 2023 17:52:02 +0100
Subject: Prove term weakening respects identities.

---
 src/Core/Term.idr | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

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

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
-- 
cgit v1.2.3