1 files changed, 20 insertions, 0 deletions
diff --git a/src/Core/Term.idr b/src/Core/Term.idr
new file mode 100644
index 0000000..603d8a9
--- /dev/null
+++ b/src/Core/Term.idr
@@ -0,0 +1,20 @@
+module Core.Term
+
+import Core.Context
+import Core.Var
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Term : Context -> Type where
+  Var : Var sx -> Term sx
+
+  Set : Term sx
+
+  Pi : (n : Name) -> Term sx -> Term (sx :< n) -> Term sx
+  Abs : (n : Name) -> Term (sx :< n) -> Term sx
+  App : Term sx -> Term sx -> Term sx
+
+%name Term t, u, v