Define declarative typing rules.

3 files changed, 142 insertions, 1 deletions

diff --git a/obs.ipkg b/obs.ipkg
index f806c52..1dd3f73 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -7,7 +7,8 @@ depends = contrib
 options = "--total"
 
 modules
-  = Core.Environment
+  = Core.Declarative
+  , Core.Environment
   , Core.Term
   , Core.Term.Substitution
   , Core.Term.Thinned
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
new file mode 100644
index 0000000..6a2c8bd
--- /dev/null
+++ b/src/Core/Declarative.idr
@@ -0,0 +1,135 @@
+module Core.Declarative
+
+import Core.Environment
+import Core.Term
+import Core.Term.Substitution
+import Core.Term.Thinned
+import Core.Thinning
+
+-- Definition ------------------------------------------------------------------
+
+data EnvWf : Env n -> Type
+data TypeWf : Env n -> Term n -> Type
+data TypeConv : Env n -> Term n -> Term n -> Type
+data TermWf : Env n -> Term n -> Term n -> Type
+data TermConv : Env n -> Term n -> Term n -> Term n -> Type
+
+data EnvWf where
+  Lin : EnvWf [<]
+  (:<) : EnvWf env -> TypeWf env (expand a) -> EnvWf (env :< a)
+
+data TypeWf where
+  SetTyWf :
+    EnvWf env ->
+    ---
+    TypeWf env Set
+  PiTyWf :
+    TypeWf env a ->
+    TypeWf (env :< pure a) b ->
+    ---
+    TypeWf env (Pi a b)
+  LiftWf :
+    TermWf env a Set ->
+    ---
+    TypeWf env a
+
+data TypeConv where
+  ReflTy :
+    TypeWf env a ->
+    ---
+    TypeConv env a a
+  SymTy :
+    TypeConv env a b ->
+    ---
+    TypeConv env b a
+  TransTy :
+    TypeConv env a b ->
+    TypeConv env b c ->
+    ---
+    TypeConv env a c
+  PiConv :
+    TypeWf env a ->
+    TypeConv env a c ->
+    TypeConv (env :< pure a) b d ->
+    ---
+    TypeConv env (Pi a b) (Pi c d)
+  LiftConv :
+    TermConv env a b Set ->
+    ---
+    TypeConv env a b
+
+data TermWf where
+  PiTmWf :
+    TermWf env a Set ->
+    TermWf (env :< pure a) b Set ->
+    ---
+    TermWf env (Pi a b) Set
+  VarWf :
+    EnvWf env ->
+    ---
+    TermWf env (Var i) (expand $ index env i)
+  AbsWf :
+    TypeWf env a ->
+    TermWf (env :< pure a) t b ->
+    ---
+    TermWf env (Abs t) (Pi a b)
+  AppWf :
+    TermWf env t (Pi a b) ->
+    TermWf env u a ->
+    ---
+    TermWf env (App t u) (subst b $ Wkn (id _) :< pure u)
+  ConvWf :
+    TermWf env t a ->
+    TypeConv env a b ->
+    ---
+    TermWf env t b
+
+data TermConv where
+  ReflTm :
+    TermWf env t a ->
+    ---
+    TermConv env t t a
+  SymTm :
+    TermConv env t u a ->
+    ---
+    TermConv env u t a
+  TransTm :
+    TermConv env t u a ->
+    TermConv env u v a ->
+    ---
+    TermConv env t v a
+  AppConv :
+    TermConv env f g (Pi a b) ->
+    TermConv env t u a ->
+    ---
+    TermConv env (App f t) (App g u) (subst b $ Wkn (id _) :< pure t)
+  PiTmConv :
+    TypeWf env a ->
+    TermConv env a c Set ->
+    TermConv (env :< pure a) b d Set ->
+    ---
+    TermConv env (Pi a b) (Pi c d) Set
+  PiEta :
+    TypeWf env a ->
+    TermWf env t (Pi a b) ->
+    TermWf env u (Pi a b) ->
+    TermConv (env :< pure a)
+      (App (wkn t $ drop $ id _) (Var FZ))
+      (App (wkn u $ drop $ id _) (Var FZ))
+      b ->
+    ---
+    TermConv env t u (Pi a b)
+  PiBeta :
+    TypeWf env a ->
+    TermWf (env :< pure a) t b ->
+    TermWf env u a ->
+    ---
+    TermConv env
+      (App (Abs t) u)
+      (subst t $ Wkn (id _) :< pure u)
+      (subst g $ Wkn (id _) :< pure u)
+  ConvConv :
+    TermConv env t u a ->
+    TypeConv env a b ->
+    ---
+    TermConv env t u b
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr
index 824439a..3ed4779 100644
--- a/src/Core/Term/Thinned.idr
+++ b/src/Core/Term/Thinned.idr
@@ -22,6 +22,11 @@ record Thinned (n : Nat) where
 
 %inline
 public export
+pure : Term n -> Thinned n
+pure = (`Over` id n)
+
+%inline
+public export
 expand : Thinned n -> Term n
 expand (term `Over` thin) = wkn term thin