1 files changed, 45 insertions, 0 deletions
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