Prove typing respects environment quotient.

1 files changed, 95 insertions, 0 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 6a2c8bd..12096ac 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -133,3 +133,98 @@ data TermConv where
     TypeConv env a b ->
     ---
     TermConv env t u b
+
+%name EnvWf envWf
+%name TypeWf tyWf
+%name TypeConv tyConv
+%name TermWf tmWf
+%name TermConv tmConv
+
+-- Respects Environment Quotient -----------------------------------------------
+
+export
+envWfRespEq : EnvWf env1 -> env1 =~= env2 -> EnvWf env2
+export
+typeWfRespEq : TypeWf env1 a -> env1 =~= env2 -> TypeWf env2 a
+export
+typeConvRespEq : TypeConv env1 a b -> env1 =~= env2 -> TypeConv env2 a b
+export
+termWfRespEq : TermWf env1 t a -> env1 =~= env2 -> TermWf env2 t a
+export
+termConvRespEq : TermConv env1 t u a -> env1 =~= env2 -> TermConv env2 t u a
+
+envWfRespEq envWf Refl = envWf
+envWfRespEq (envWf :< tyWf) (prf :< prf') =
+  envWfRespEq envWf prf :<
+  rewrite sym prf' in typeWfRespEq tyWf prf
+
+typeWfRespEq (SetTyWf envWf) prf = SetTyWf (envWfRespEq envWf prf)
+typeWfRespEq (PiTyWf tyWf tyWf1) prf =
+  PiTyWf
+    (typeWfRespEq tyWf prf)
+    (typeWfRespEq tyWf1 $ prf :< Refl)
+typeWfRespEq (LiftWf tmWf) prf = LiftWf (termWfRespEq tmWf prf)
+
+typeConvRespEq (ReflTy tyWf) prf = ReflTy (typeWfRespEq tyWf prf)
+typeConvRespEq (SymTy tyConv) prf = SymTy (typeConvRespEq tyConv prf)
+typeConvRespEq (TransTy tyConv tyConv1) prf =
+  TransTy
+    (typeConvRespEq tyConv prf)
+    (typeConvRespEq tyConv1 prf)
+typeConvRespEq (PiConv tyWf tyConv tyConv1) prf =
+  PiConv
+    (typeWfRespEq tyWf prf)
+    (typeConvRespEq tyConv prf)
+    (typeConvRespEq tyConv1 $ prf :< Refl)
+typeConvRespEq (LiftConv tmConv) prf = LiftConv (termConvRespEq tmConv prf)
+
+termWfRespEq (PiTmWf tmWf tmWf1) prf =
+  PiTmWf
+    (termWfRespEq tmWf prf)
+    (termWfRespEq tmWf1 $ prf :< Refl)
+termWfRespEq (VarWf {i} envWf) prf =
+  rewrite indexCong prf i in
+  VarWf (envWfRespEq envWf prf)
+termWfRespEq (AbsWf tyWf tmWf) prf =
+  AbsWf
+    (typeWfRespEq tyWf prf)
+    (termWfRespEq tmWf $ prf :< Refl)
+termWfRespEq (AppWf tmWf tmWf1) prf =
+  AppWf
+    (termWfRespEq tmWf prf)
+    (termWfRespEq tmWf1 prf)
+termWfRespEq (ConvWf tmWf tyConv) prf =
+  ConvWf
+    (termWfRespEq tmWf prf)
+    (typeConvRespEq tyConv prf)
+
+termConvRespEq (ReflTm tmWf) prf = ReflTm (termWfRespEq tmWf prf)
+termConvRespEq (SymTm tmConv) prf = SymTm (termConvRespEq tmConv prf)
+termConvRespEq (TransTm tmConv tmConv1) prf =
+  TransTm
+    (termConvRespEq tmConv prf)
+    (termConvRespEq tmConv1 prf)
+termConvRespEq (AppConv tmConv tmConv1) prf =
+  AppConv
+    (termConvRespEq tmConv prf)
+    (termConvRespEq tmConv1 prf)
+termConvRespEq (PiTmConv tyWf tmConv tmConv1) prf =
+  PiTmConv
+    (typeWfRespEq tyWf prf)
+    (termConvRespEq tmConv prf)
+    (termConvRespEq tmConv1 $ prf :< Refl)
+termConvRespEq (PiEta tyWf tmWf tmWf1 tmConv) prf =
+  PiEta
+    (typeWfRespEq tyWf prf)
+    (termWfRespEq tmWf prf)
+    (termWfRespEq tmWf1 prf)
+    (termConvRespEq tmConv $ prf :< Refl)
+termConvRespEq (PiBeta tyWf tmWf tmWf1) prf =
+  PiBeta
+    (typeWfRespEq tyWf prf)
+    (termWfRespEq tmWf $ prf :< Refl)
+    (termWfRespEq tmWf1 prf)
+termConvRespEq (ConvConv tmConv tyConv) prf =
+  ConvConv
+    (termConvRespEq tmConv prf)
+    (typeConvRespEq tyConv prf)