1 files changed, 54 insertions, 0 deletions
diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr
new file mode 100644
index 0000000..6846d80
--- /dev/null
+++ b/src/Core/Term/Substitution.idr
@@ -0,0 +1,54 @@
+module Core.Term.Substitution
+
+import Core.Term
+import Core.Term.Thinned
+import Core.Thinning
+
+infix 4 =~=
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Subst : Nat -> Nat -> Type where
+  Wkn : m `Thins` n -> Subst m n
+  (:<) : Subst m n -> Thinned n -> Subst (S m) n
+
+namespace Eq
+  public export
+  data (=~=) : Subst m n -> Subst m n -> Type where
+    Refl : sub =~= sub
+    (:<) : sub1 =~= sub2 -> t =~= u -> sub1 :< t =~= sub2 :< u
+
+%name Subst sub
+%name Eq.(=~=) prf
+
+-- Indexing --------------------------------------------------------------------
+
+public export
+index : Subst m n -> Fin m -> Thinned n
+index (Wkn thin) i = Var i `Over` thin
+index (sub :< t) FZ = t
+index (sub :< t) (FS i) = index sub i
+
+-- Weakening -------------------------------------------------------------------
+
+public export
+wkn : Subst k m -> m `Thins` n -> Subst k n
+wkn (Wkn thin') thin = Wkn (thin . thin')
+wkn (sub :< t) thin = wkn sub thin :< wkn t thin
+
+-- Constructors ----------------------------------------------------------------
+
+public export
+lift : Subst m n -> Subst (S m) (S n)
+lift sub = wkn sub (drop $ id n) :< (Var 0 `Over` id (S n))
+
+-- Substitution ----------------------------------------------------------------
+
+public export
+subst : Term m -> Subst m n -> Term n
+subst (Var i) sub = expand $ index sub i
+subst Set sub = Set
+subst (Pi t u) sub = Pi (subst t sub) (subst u $ lift sub)
+subst (Abs t) sub = Abs (subst t $ lift sub)
+subst (App t u) sub = App (subst t sub) (subst u sub)