module Obs.Substitution

import Data.Fin

%default total

public export
interface Rename (0 x : Nat -> Type) where
  rename : forall m, n . x n -> (Fin n -> Fin m) -> x m

public export
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)