From fbd0390f32f98dd65567bf64765bd4fbed6008b9 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 2 Apr 2023 10:36:11 +0100
Subject: State that weakening preserves typing.

---
 src/Core/Declarative.idr | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

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

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 9f60d34..ae31870 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -286,3 +286,22 @@ CompWf (KeepWf {thin = thin2, n, prf = prf2} thinWf2) (KeepWf {thin = thin1, thi
   rewrite compKeep thin2 thin1 n in
   rewrite compAssoc thin2 thin1 thin' in
   KeepWf {prf = compPresNotId prf2 prf1} (CompWf thinWf2 thinWf1)
+
+-- Weakening Preservation ------------------------------------------------------
+
+wknPresTypeWf :
+  TypeWf env1 a ->
+  ThinWf thin env2 env1 ->
+  TypeWf env2 (wkn a thin)
+wknPresTypeConv :
+  TypeConv env1 a b ->
+  ThinWf thin env2 env1 ->
+  TypeConv env2 (wkn a thin) (wkn b thin)
+wknPresTermWf :
+  TermWf env1 t a ->
+  ThinWf thin env2 env1 ->
+  TermWf env2 (wkn t thin) (wkn a thin)
+wknPresTermConv :
+  TermConv env1 t u a ->
+  ThinWf thin env2 env1 ->
+  TermConv env2 (wkn t thin) (wkn u thin) (wkn a thin)
-- 
cgit v1.2.3