From 6e8ab4c1135f39d441cdcf54c5a1bc12b7e565be Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 8 Apr 2023 15:45:24 +0100
Subject: Prove conversion is a generic equality.

---
 src/Core/Generic.idr | 45 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)

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

diff --git a/src/Core/Generic.idr b/src/Core/Generic.idr
index 37b6b36..bd11fad 100644
--- a/src/Core/Generic.idr
+++ b/src/Core/Generic.idr
@@ -114,3 +114,48 @@ interface IsGenericEquality (eq : GenericEquality) where
     eq.TermEq env a b f ->
     ---
     eq.NtrlEq {sx} env (App t a) (App u b) (subst g (sub1 a))
+
+-- Judgemental Equality --------------------------------------------------------
+
+Judgemental : GenericEquality
+Judgemental = MkEquality TypeConv TermConv TermConv
+
+IsGenericEquality Judgemental where
+  ntrlImpliesTermEq = id
+  termImpliesTypeEq = LiftConv
+  eqImpliesTermConv = id
+  eqImpliesTypeConv = id
+
+  ntrlSym = SymTerm
+  ntrlTrans = TransTerm
+  termSym = SymTerm
+  termTrans = TransTerm
+  typeSym = SymType
+  typeTrans = TransType
+
+  ntrlConv = ConvTermConv
+  termConv = ConvTermConv
+
+  wknPresNtrlEq = wknPresTermConv
+  wknPresTermEq = wknPresTermConv
+  wknPresTypeEq = wknPresTypeConv
+
+  typeExpansion steps1 steps2 n m conv =
+    TransType (typeRedImpliesTypeConv steps1) $
+    TransType conv $
+    SymType (typeRedImpliesTypeConv steps2)
+  termExpansion steps1 steps2 steps3 n m k conv =
+    ConvTermConv
+      (TransTerm (termRedImpliesTermConv steps2) $
+       TransTerm conv $
+       SymTerm (termRedImpliesTermConv steps3))
+      (SymType $ typeRedImpliesTypeConv steps1)
+
+  typeSet = ReflType . SetType
+  typePi = PiTypeConv
+
+  termPi = PiTermConv
+  termPiEta = PiEta
+
+  ntrlVar = ReflTerm
+  ntrlApp = AppConv
-- 
cgit v1.2.3