从类型论到setoids再回到
From type theory to setoids and back
摘要：
在Agda中形式化了一个包含宇宙的马丁-勒夫外延类型理论模型，Agda是一个基于马丁-勒夫内涵类型理论的交互式证明系统。我们认为，这可以理解为对在内涵理论中建立完全外延理论模型这一老问题的解决。类型被解释为setoid，因此模型是setoid模型。我们利用Aczel类型的迭代集解决了解释类型宇宙的问题，并展示了如何将其制成包含必要setoid构造的小setoid的setoid。此外，我们解释了Awodey和Bauer的括号类型。更多的商类型应该是可解释的。
英文摘要：
A model of Martin-Löf extensional type theory with universes is formalized in Agda, an interactive proof system based on Martin-Löf intensional type theory. This may be understood, we claim, as a solution to the old problem of modelling the full extensional theory in the intensional theory. Types are interpreted as setoids, and the model is therefore a setoid model. We solve the problem of intepreting type universes by utilizing Aczel's type of iterative sets, and show how it can be made into a setoid of small setoids containing the necessary setoid constructions. In addition we interpret the bracket types of Awodey and Bauer. Further quotient types should be interpretable.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
