[Agda] Normalization by evaluation, plain Agda types and impredicativity.

[flicky frans]

Hello. I am searching for a paper, that describes normalization by
evaluation for roughly this representation of the lambda-calculus:

{-# OPTIONS --type-in-type #-}

mutual
  data Term : Set -> Set where
    ↑ : {A : Set} -> A -> Term A
    _·_ : {A : Set} {B : A -> Set}
        -> Term ((x : A) -> B x) -> (e : Term A) -> Term (B (eval e))
    ⇧ : {A : Set} {B : A -> Set}
      -> ((x : A) -> Term (B x)) -> Term ((x : A) -> B x)

  eval : ∀ {A} -> Term A -> A
  eval (↑ v)   = v
  eval (f · x) = eval f (eval x)
  eval (⇧ f)   = λ x -> eval (f x)

I've searched, but haven't found any NbE algorithm for representation,
that contains dependent meta-language types. I wrote one [1] and want
to study other approaches, if they exist.

Also, there are a lof of `subst`s in normalized terms in my code,
probably because of the postulated functional extensionality axiom. Is
it possible to remove them without searching for another proof of the
`eval∘reify∘reflect` lemma? I could "prove" `fun-ext` from Girard's
paradox, but that's very dirty.

[1] http://lpaste.net/111763