[Agda] Normalization by Evaluation

[Brandon Moore]

> One way to do the proof can be found in section 2.5 of

> 
> http://www.cse.chalmers.se/~peterd/papers/Glueing.pdf 
> 
> The key idea is to define a family of predicates "Gl_A" by induction 
> on types A, which carves out the good values in the semantics.

Dear Peter

Thanks for the reference. I see it's enough for the predicate to
assert things about the quotation of the semantic value,
rather than relating the quotation to any particular input value.
The point about initial algebras seems to be key.

Brandon