Define generic equality.

Judgemental equality is a trivial instance.

3 files changed, 202 insertions, 0 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 987d511..96f9be4 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -10,6 +10,7 @@ modules
   = Core.Declarative
   , Core.Environment
   , Core.Environment.Extension
+  , Core.Generic
   , Core.Reduction
   , Core.Term
   , Core.Term.NormalForm
diff --git a/src/Core/Generic.idr b/src/Core/Generic.idr
new file mode 100644
index 0000000..c2bd1f4
--- /dev/null
+++ b/src/Core/Generic.idr
@@ -0,0 +1,178 @@
+module Core.Generic
+
+import Core.Declarative
+import Core.Environment
+import Core.Reduction
+import Core.Term
+import Core.Term.NormalForm
+import Core.Term.Substitution
+import Core.Term.Thinned
+import Core.Thinning
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+public export
+record Equality where
+  constructor MkEquality
+  TypeEq : forall n. Env n -> Term n -> Term n -> Type
+  TermEq : forall n. Env n -> Term n -> Term n -> Term n -> Type
+  NtrlEq : forall n. Env n -> NeutralTerm n -> NeutralTerm n -> Term n -> Type
+
+public export
+interface IsEq (0 eq : Equality) where
+  -- Subsumption
+  ntrlEqImpliesTermEq :
+    {0 n, m : NeutralTerm k} ->
+    eq.NtrlEq env n m a ->
+    eq.TermEq env n.fst m.fst a
+  termEqImpliesTypeEq : eq.TermEq {n} env a b Set -> eq.TypeEq env a b
+  termEqImpliesConv : eq.TermEq {n} env t u a -> TermConv env t u a
+  typeEqImpliesConv : eq.TypeEq {n} env a b -> TypeConv env a b
+
+  -- Partial Equivalence
+  ntrlSym : eq.NtrlEq {n = k} env n m a -> eq.NtrlEq env m n a
+  ntrlTrans : eq.NtrlEq {n = k} env n1 n2 a -> eq.NtrlEq env n2 n3 a -> eq.NtrlEq env n1 n3 a
+  termSym : eq.TermEq {n} env t u a -> eq.TermEq env u t a
+  termTrans : eq.TermEq {n} env t u a -> eq.TermEq env u v a -> eq.TermEq env t v a
+  typeSym : eq.TypeEq {n} env a b -> eq.TypeEq env b a
+  typeTrans : eq.TypeEq {n} env a b -> eq.TypeEq env b c -> eq.TypeEq env a c
+
+  -- Conversion
+  ntrlConv : eq.NtrlEq {n = k} env n m a -> TypeConv env a b -> eq.NtrlEq env n m b
+  termConv : eq.TermEq {n} env t u a -> TypeConv env a b -> eq.TermEq env t u b
+
+  -- Weakening
+  wknNtrl :
+    eq.NtrlEq {n = j} env1 n m a ->
+    ExtendsWf thin env2 env1 ->
+    eq.NtrlEq {n = k} env2 (wkn n thin) (wkn m thin) (wkn a thin)
+  wknTerm :
+    eq.TermEq {n = m} env1 t u a ->
+    ExtendsWf thin env2 env1 ->
+    eq.TermEq {n} env2 (wkn t thin) (wkn u thin) (wkn a thin)
+  wknType :
+    eq.TypeEq {n = m} env1 a b ->
+    ExtendsWf thin env2 env1 ->
+    eq.TypeEq {n} env2 (wkn a thin) (wkn b thin)
+
+  -- Weak Head Expansion
+  expandTerm :
+    TermReduce env t t' a ->
+    TermReduce env u u' a ->
+    Whnf t' ->
+    Whnf u' ->
+    eq.TermEq {n} env t' u' a ->
+    eq.TermEq env t u a
+  expandType :
+    TypeReduce env a a' ->
+    TypeReduce env b b' ->
+    Whnf a' ->
+    Whnf b' ->
+    eq.TypeEq {n} env a' b' ->
+    eq.TypeEq env a b
+
+  -- Neutral Congruence
+  ntrlVar :
+    TermWf env (Var i) a ->
+    ---
+    eq.NtrlEq {n} env (Element (Var i) Var) (Element (Var i) Var) a
+  ntrlApp :
+    {0 n, m : NeutralTerm k} ->
+    eq.NtrlEq env n m (Pi a b) ->
+    eq.TermEq env t u a ->
+    ---
+    eq.NtrlEq env
+      (Element (App n.fst t) (App n.snd))
+      (Element (App m.fst u) (App m.snd))
+      (subst1 b t)
+
+  -- Term Congurence
+  termPi :
+    TypeWf env a ->
+    eq.TermEq env a c Set ->
+    eq.TermEq (env :< pure a) b d Set ->
+    ---
+    eq.TermEq {n} env (Pi a b) (Pi c d) Set
+  termPiEta :
+    TypeWf env a ->
+    TermWf env t (Pi a b) ->
+    TermWf env u (Pi a b) ->
+    eq.TermEq (env :< pure a)
+      (App (wkn t $ drop $ id _) (Var FZ))
+      (App (wkn u $ drop $ id _) (Var FZ))
+      b ->
+    ---
+    eq.TermEq {n} env t u (Pi a b)
+
+  -- Type Congruence
+  typeSet :
+    EnvWf env ->
+    ---
+    eq.TypeEq {n} env Set Set
+  typePi :
+    TypeWf env a ->
+    eq.TypeEq env a c ->
+    eq.TypeEq (env :< pure a) b d ->
+    ---
+    eq.TypeEq {n} env (Pi a b) (Pi c d)
+
+-- Instance 1 ------------------------------------------------------------------
+
+public export
+Judgemental : Equality
+Judgemental = MkEquality TypeConv TermConv (\env, n, m, a => TermConv env n.fst m.fst a)
+
+judgeWknNtrl :
+  (Judgemental .NtrlEq) {n = j} env1 n m a ->
+  ExtendsWf thin env2 env1 ->
+  (Judgemental .NtrlEq) {n = k} env2 (wkn n thin) (wkn m thin) (wkn a thin)
+judgeWknNtrl {n = Element t n, m = Element u m} = weakenTermConv
+
+export
+IsEq Judgemental where
+  -- Subsumption
+  ntrlEqImpliesTermEq = id
+  termEqImpliesTypeEq = LiftConv
+  termEqImpliesConv = id
+  typeEqImpliesConv = id
+
+  -- Partial Equivalence
+  ntrlSym = SymTm
+  ntrlTrans = TransTm
+  termSym = SymTm
+  termTrans = TransTm
+  typeSym = SymTy
+  typeTrans = TransTy
+
+  -- Conversion
+  ntrlConv = ConvConv
+  termConv = ConvConv
+
+  -- Weakening
+  wknNtrl = judgeWknNtrl
+  wknTerm = weakenTermConv
+  wknType = weakenTypeConv
+
+  -- Weak Head Expansion
+  expandTerm = \steps1, steps2, n, m, eq =>
+    TransTm (termRedImpliesConv steps1) $
+    TransTm eq $
+    SymTm (termRedImpliesConv steps2)
+  expandType = \steps1, steps2, n, m, eq =>
+    TransTy (typeRedImpliesConv steps1) $
+    TransTy eq $
+    SymTy (typeRedImpliesConv steps2)
+
+  -- Neutral Congruence
+  ntrlVar = ReflTm
+  ntrlApp = AppConv
+
+  -- Term Congurence
+  termPi = PiTmConv
+  termPiEta = PiEta
+
+  -- Type Congruence
+  typeSet = ReflTy . SetTyWf
+  typePi = PiConv
diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr
index 9984bee..2cd16a1 100644
--- a/src/Core/Term/NormalForm.idr
+++ b/src/Core/Term/NormalForm.idr
@@ -1,6 +1,9 @@
 module Core.Term.NormalForm
 
 import Core.Term
+import Core.Thinning
+
+import public Data.DPair
 
 -- Definition ------------------------------------------------------------------
 
@@ -20,3 +23,23 @@ data Whnf : Term n -> Type where
 
 %name Neutral n, m
 %name Whnf n, m
+
+public export
+NeutralTerm : Nat -> Type
+NeutralTerm n = Subset (Term n) Neutral
+
+-- Inversion -------------------------------------------------------------------
+
+invertNtrlApp : Neutral (App t u) -> Neutral t
+invertNtrlApp (App n) = n
+
+-- Weakening -------------------------------------------------------------------
+
+export
+wknPresNtrl : Neutral t -> (thin : m `Thins` n) -> Neutral (wkn t thin)
+wknPresNtrl Var thin = Var
+wknPresNtrl (App n) thin = App (wknPresNtrl n thin)
+
+public export
+wkn : NeutralTerm m -> m `Thins` n -> NeutralTerm n
+wkn (Element t n) thin = Element (wkn t thin) (wknPresNtrl n thin)