module STLC.Embed {U : Set} (Prim : U → Set) where open import STLC.Embedded as E open import STLC.Typing U as T open import STLC.Bound Type as B open import Data.Fin open import Data.Vec open import Relation.Binary.PropositionalEquality embed-type : T.Type → Set embed-type (el A) = Prim A embed-type (τ₁ ↣ τ₂) = embed-type τ₁ → embed-type τ₂ embed-ctxt : ∀ {n} → T.Ctxt n → E.Ctxt n embed-ctxt [] = [] embed-ctxt (τ ∷ Γ) = embed-type τ ∷ embed-ctxt Γ embed-hom : ∀ {n} x → (Γ : T.Ctxt n) → lookup x (embed-ctxt Γ) ≡ embed-type (lookup x Γ) embed-hom () [] embed-hom zero (y ∷ Γ) = refl embed-hom (suc x) (y ∷ Γ) = embed-hom x Γ embed : ∀ {n} {E : B.Expr n} {Γ : T.Ctxt n} {τ : T.Type} → Γ ⊢ E ∶ τ → E.Expr (embed-ctxt Γ) (embed-type τ) embed {E = var x} {Γ} tVar = subst (E.Expr _) (embed-hom x Γ) (var x) embed {E = lam τ _} (tLam t) = lam {A = embed-type τ} (embed t) embed (t₁ · t₂) = embed t₁ · embed t₂