类型论中的类型论求值归一化
Normalisation by Evaluation for Type Theory, in Type Theory
AI总结：
本文在类型论中基于预层范畴和商归纳类型提出依赖类型的求值归一化方法，合并解释与逻辑关系为证明相关谓词，证明定义等式的归一化、完备性、稳定性和可判定性，并在Agda中形式化。
摘要：
我们基于预层范畴为依赖类型发展了求值归一化（NBE）。我们的构造在类型论的元语言中使用商归纳类型表述。我们采用带类型的表示，因此构造中没有前项或实现者，且每个构造都尊重转换关系。简单类型的NBE使用语法与预层解释之间的逻辑关系。在我们的构造中，我们将预层解释与逻辑关系合并为一个证明相关的逻辑谓词。我们证明了定义等式的归一化、完备性、稳定性和可判定性。大部分构造已在Agda中形式化。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
