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

[flicky frans]

2014-09-29 23:57 GMT+04:00, Larrytheliquid <larrytheliquid at gmail.com>:
> Note that changing McBride's ObMC to be indexed over Agda Set's instead of
> a universe is easy and also works well.
>
> I did so when adapting ObMC to a universe hierarchy in accompanying code
> for the paper "Leveling up dependent types":
> https://github.com/larrytheliquid/leveling-up/blob/master/src/TT/OperationalTerms.agda
>
> The code also contains a version closer to yours where the binding
> constructs of Term (Pi, lambda, etc) use Agda functions instead:
> https://github.com/larrytheliquid/leveling-up/blob/master/src/TT/DenotationalTerms.agda

Great paper, thanks. Your representation is quite more complex
however. I'll think about what I can adopt from your development.