Normalisation by Evaluation for Type Theory, in Type Theory

We develop normalisation by evaluation (NBE) for dependent types based onpresheaf categories. Our construction is formulated in the metalanguage of typetheory using quotient inductive types. We use a typed presentation hence thereare no preterms or realizers in our construction, and every constructionrespects the conversion relation. NBE for simple types uses a logical relationbetween the syntax and the presheaf interpretation. In our construction, wemerge the presheaf interpretation and the logical relation into aproof-relevant logical predicate. We prove normalisation, completeness,stability and decidability of definitional equality. Most of the constructionswere formalized in Agda