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