We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda.
Altenkirch, T., & Kaposi, A. (2017). Normalisation by evaluation for type theory, in type theory. Logical Methods in Computer Science, 13(4:1), https://doi.org/10.23638/LMCS-13%284%3A1%292017