1 files changed, 50 insertions, 0 deletions
diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr
new file mode 100644
index 0000000..248c44f
--- /dev/null
+++ b/src/Core/Term/Substitution.idr
@@ -0,0 +1,50 @@
+module Core.Term.Substitution
+
+import Core.Context
+import Core.Var
+import Core.Term
+import Core.Thinning
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Subst : Context -> Context -> Type where
+  Base : sx `Thins` sy -> Subst sx sy
+  (:<) : Subst sx sy -> (sz `Thins` sy, Term sz) -> Subst (sx :< x) sy
+
+%name Subst sub
+
+-- Constructors ----------------------------------------------------------------
+
+public export
+sub1 : Term sx -> Subst (sx :< n) sx
+sub1 t = Base (id sx) :< (id sx, t)
+
+-- Operations ------------------------------------------------------------------
+
+export
+index : Subst sx sy -> Var sx -> Term sy
+doIndex : Subst sx sy -> (sz `Thins` sy, Term sz) -> {0 i : Var (sx :< n)} -> View i -> Term sy
+
+index (Base thin) i = Var $ wkn i thin
+index (sub :< p) i = doIndex sub p (view i)
+
+doIndex sub (thin, t) Here = wkn t thin
+doIndex sub p (There i) = index sub i
+
+public export
+wkn : Subst sx sy -> sy `Thins` sz -> Subst sx sz
+wkn (Base thin') thin = Base (thin . thin')
+wkn (sub :< (thin', t)) thin = wkn sub thin :< (thin . thin', t)
+
+public export
+lift : Subst sx sy -> (0 n : Name) -> Subst (sx :< n) (sy :< n)
+lift sub n = wkn sub (drop (id sy) n) :< (id _, Var here)
+
+public export
+subst : Term sx -> Subst sx sy -> Term sy
+subst (Var i) sub = index sub i
+subst Set sub = Set
+subst (Pi n t u) sub = Pi n (subst t sub) (subst u $ lift sub n)
+subst (Abs n t) sub = Abs n (subst t $ lift sub n)
+subst (App t u) sub = App (subst t sub) (subst u sub)