From a38b0b5a6ee30e7dd22bc91765ba5361ed807dda Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 15 Apr 2023 16:35:15 +0100
Subject: Prove substitution respects the quotient.

---
 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 1b050ca..74ef7af 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -27,3 +27,24 @@ wkn Set thin = Set
 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
+wknHomo :
+  (t : Term k) ->
+  (thin1 : k `Thins` m) ->
+  (thin2 : m `Thins` n) ->
+  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
+wknHomo (Var i) thin1 thin2 = cong Var (wknHomo i thin1 thin2)
+wknHomo Set thin1 thin2 = Refl
+wknHomo (Pi t u) thin1 thin2 =
+  cong2 Pi
+    (wknHomo t thin1 thin2)
+    (trans
+      (wknHomo u (keep thin1) (keep thin2))
+      (cong (wkn u) $ compKeep thin2 thin1))
+wknHomo (Abs t) thin1 thin2 =
+  cong Abs
+    (trans
+      (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)
-- 
cgit v1.2.3