From 87eea439d8d8390c768498c2224268200373f629 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 16 Apr 2023 18:31:20 +0100
Subject: Prove weakening of type judgements.

This is a huge commit that has many more changes. I should split
this up later.
---
 src/Core/Term.idr | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

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

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
@@ -28,6 +30,14 @@ wkn (Pi t u) thin = Pi (wkn t thin) (wkn u $ keep thin)
 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) ->
@@ -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))
-- 
cgit v1.2.3