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

[flicky frans]

Thanks for the answers.

> Here is a (historical) reference describing your technique for System F-omega, albeit before the time of Agda...

It's similar, but not exactly the same. Their representation is
predicative (kinds are inferred by a compiler) and `Term' is not an
inductive-recursive type.

> I don't know how relevant it is to this thread but there's also the
> style from McBride's "Outrageous but Meaningful Coincidences:
> Dependent type-safe syntax and evaluation".

This is related, but again, there is an encoded universe with a
decoding function instead of plain Agda types.
Do you know, is there some accompanying paper for your [1]?