From ff4c5f15f354aa8da7bb5868d913dbbef23832a3 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 18 Dec 2022 16:36:09 +0000 Subject: Add dependent products. --- src/Obs/Substitution.idr | 34 ++++++++++++++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) (limited to 'src/Obs/Substitution.idr') 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) -- cgit v1.2.3