Define generic equality.

2 files changed, 117 insertions, 0 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 73ffaf9..af236ce 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -11,6 +11,7 @@ modules
   , Core.Declarative
   , Core.Declarative.Substitution
   , Core.Environment
+  , Core.Generic
   , Core.Name
   , Core.Reduction
   , Core.Term
diff --git a/src/Core/Generic.idr b/src/Core/Generic.idr
new file mode 100644
index 0000000..37b6b36
--- /dev/null
+++ b/src/Core/Generic.idr
@@ -0,0 +1,116 @@
+module Core.Generic
+
+import Core.Context
+import Core.Declarative
+import Core.Environment
+import Core.Reduction
+import Core.Term
+import Core.Term.NormalForm
+import Core.Term.Substitution
+import Core.Thinning
+import Core.Var
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+record GenericEquality where
+  constructor MkEquality
+  TypeEq : forall sx. Env sx -> Term sx -> Term sx -> Type
+  TermEq : forall sx. Env sx -> Term sx -> Term sx -> Term sx -> Type
+  NtrlEq : forall sx. Env sx -> Term sx -> Term sx -> Term sx -> Type
+
+interface IsGenericEquality (eq : GenericEquality) where
+  -- Subsumption
+  ntrlImpliesTermEq : eq.NtrlEq {sx} env t u a -> eq.TermEq env t u a
+  termImpliesTypeEq : eq.TermEq {sx} env a b Set -> eq.TypeEq env a b
+  eqImpliesTermConv : eq.TermEq {sx} env t u a -> TermConv env t u a
+  eqImpliesTypeConv : eq.TypeEq {sx} env a b -> TypeConv env a b
+
+  -- Partial Equivalence
+  ntrlSym : eq.NtrlEq {sx} env t u a -> eq.NtrlEq env u t a
+  ntrlTrans : eq.NtrlEq {sx} env t u a -> eq.NtrlEq env u v a -> eq.NtrlEq env t v a
+  termSym : eq.TermEq {sx} env t u a -> eq.TermEq env u t a
+  termTrans : eq.TermEq {sx} env t u a -> eq.TermEq env u v a -> eq.TermEq env t v a
+  typeSym : eq.TypeEq {sx} env a b -> eq.TypeEq env b a
+  typeTrans : eq.TypeEq {sx} env a b -> eq.TypeEq env b c -> eq.TypeEq env a c
+
+  -- Conversion
+  ntrlConv : eq.NtrlEq {sx} env t u a -> TypeConv env a b -> eq.NtrlEq env t u b
+  termConv : eq.TermEq {sx} env t u a -> TypeConv env a b -> eq.TermEq env t u b
+
+  -- Weakening
+  wknPresNtrlEq :
+    eq.NtrlEq {sx} env1 t u a ->
+    EnvWf env2 ->
+    IsExtension thin env2 env1 ->
+    eq.NtrlEq {sx = sy} env2 (wkn t thin) (wkn u thin) (wkn a thin)
+  wknPresTermEq :
+    eq.TermEq {sx} env1 t u a ->
+    EnvWf env2 ->
+    IsExtension thin env2 env1 ->
+    eq.TermEq {sx = sy} env2 (wkn t thin) (wkn u thin) (wkn a thin)
+  wknPresTypeEq :
+    eq.TypeEq {sx} env1 a b ->
+    EnvWf env2 ->
+    IsExtension thin env2 env1 ->
+    eq.TypeEq {sx = sy} env2 (wkn a thin) (wkn b thin)
+
+  -- Weak Head Expansion
+  typeExpansion :
+    TypeRed env a a' ->
+    TypeRed env b b' ->
+    Whnf a' ->
+    Whnf b' ->
+    eq.TypeEq {sx} env a' b' ->
+    eq.TypeEq env a b
+  termExpansion :
+    TypeRed env a b ->
+    TermRed env t t' b ->
+    TermRed env u u' b ->
+    Whnf b ->
+    Whnf t' ->
+    Whnf u' ->
+    eq.TermEq {sx} env t' u' b ->
+    eq.TermEq env t u a
+
+  -- Type Constructor Congruence
+  typeSet :
+    EnvWf env ->
+    ---
+    eq.TypeEq {sx} env Set Set
+  typePi :
+    TypeWf env f ->
+    eq.TypeEq env f h ->
+    eq.TypeEq (env :< f) g e ->
+    ---
+    eq.TypeEq {sx} env (Pi n f g) (Pi n h e)
+
+  -- Term Constructor Congruence and η
+  termPi :
+    TypeWf env f ->
+    eq.TermEq env f h Set ->
+    eq.TermEq (env :< f) g e Set ->
+    ---
+    eq.TermEq {sx} env (Pi n f g) (Pi n h e) Set
+  termPiEta :
+    TypeWf env f ->
+    TermWf env t (Pi n f g) ->
+    TermWf env u (Pi n f g) ->
+    eq.TermEq (env :< f)
+      (App (wkn t (wkn1 _ n)) (Var Var.here))
+      (App (wkn u (wkn1 _ n)) (Var Var.here))
+      g ->
+    ---
+    eq.TermEq {sx} env t u (Pi n f g)
+
+  -- Neutral Congruence
+  ntrlVar :
+    TermWf env (Var i) a ->
+    ---
+    eq.NtrlEq {sx} env (Var i) (Var i) a
+  ntrlApp :
+    eq.NtrlEq env t u (Pi n f g) ->
+    eq.TermEq env a b f ->
+    ---
+    eq.NtrlEq {sx} env (App t a) (App u b) (subst g (sub1 a))