module Exp6b where

data Nat : Set where
  z : Nat
  s : Nat → Nat

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO z #-}
{-# BUILTIN SUC s #-}

_+_ : Nat → Nat → Nat
z   + n = n
s m + n = s (m + n)

data Fin : Nat → Set where
  fz : ∀{n} → Fin (s n)
  fs : ∀{n} → Fin n → Fin (s n)

data Exp : Nat → Set where
  Var : ∀{n} → Fin n → Exp n
  Val : ∀{n} → Nat → Exp n
  Add : ∀{n} → Exp n → Exp n → Exp n
  Let : ∀{n} → Exp n → Exp (s n) → Exp n

data Env : Nat → Set where
  ε : Env z
  _<_ : ∀{n} → Env n → Nat → Env (s n)

lookup : ∀{n} → Fin n → Env n → Nat
lookup fz     (γ < n) = n
lookup (fs i) (γ < n) = lookup i γ

eval : ∀{n} → Exp n → Env n → Nat
eval (Var i)     γ = lookup i γ
eval (Val n)     γ = n
eval (Add e1 e2) γ = eval e1 γ + eval e2 γ
eval (Let e1 e2) γ = eval e2 (γ < eval e1 γ)

Ren : Nat → Nat → Set
Ren m n = Fin m → Fin n

mapRen : ∀{m n} → Ren m n → Exp m → Exp n
mapRen f (Var i)     = Var (f i)
mapRen f (Val n)     = Val n
mapRen f (Add e1 e2) = Add (mapRen f e1) (mapRen f e2)
mapRen f (Let e1 e2) = {!!}

idRen : ∀{n} → Ren n n
idRen i = i

compRen : ∀{m n o} → Ren n o → Ren m n → Ren m o
compRen f g i = f (g i)

data _≅_ {A : Set} : A → A → Set where
  refl : {a : A} → a ≅ a

postulate ext : ∀{A B}{f f' : A → B} → (∀ a → f a ≅ f' a) → f ≅ f'

rid : ∀{m n}(f : Ren m n) → compRen f idRen ≅ f
rid f = ext (λ i → refl)

Sub : Nat → Nat → Set
Sub m n = Fin m → Exp n

extend : ∀{m n} → Sub m n → Exp n → Sub (s m) n
extend f e fz     = e
extend f e (fs i) = f i

sub : ∀{m n} → Sub m n → Exp m → Exp n
sub f (Var i)     = f i
sub f (Val n)     = Val n
sub f (Add e1 e2) = Add (sub f e1) (sub f e2)
sub f (Let e1 e2) = sub (extend f (sub f e1)) e2