Add dependent products.

1 files changed, 32 insertions, 2 deletions

diff --git a/src/Obs/Substitution.idr b/src/Obs/Substitution.idr
index 54df355..340afff 100644
--- a/src/Obs/Substitution.idr
+++ b/src/Obs/Substitution.idr
@@ -5,9 +5,39 @@ import Data.Fin
 %default total
 
 public export
-interface Rename (x : Nat -> Type) where
+interface Rename (0 x : Nat -> Type) where
   rename : forall m, n . x n -> (Fin n -> Fin m) -> x m
 
 public export
-interface Subst (x, y, z : Nat -> Type) where
+interface Rename x => PointedRename x where
+  point : forall n . Fin n -> x n
+
+public export
+interface Subst (0 x, y, z : Nat -> Type) where
   subst : forall m, n . x n -> (Fin n -> y m) -> z m
+
+public export
+Rename x => Subst x Fin x where
+  subst = rename
+
+public export
+Rename Fin where
+  rename i f = f i
+
+public export
+PointedRename Fin where
+  point = id
+
+public export
+add : (0 x : _) -> x n -> (Fin m -> x n) -> Fin (S m) -> x n
+add x v f FZ     = v
+add x v f (FS i) = f i
+
+public export
+lift : PointedRename x => (k : _) -> (Fin m -> x n) -> Fin (k + m) -> x (k + n)
+lift 0     f = f
+lift (S k) f = add x (point FZ) (\i => rename (lift k f i) FS)
+
+public export
+weaken : Rename x => (m : _) -> x n -> x (m + n)
+weaken m t = rename t (shift m)