AI 中文总结
该研究在内涵类型论中给出显示集合oid新概念，用于为带宇宙的外延类型论在安全Agda中提供语义，通过特定方式定义其语法，虽因IRU表达手段有限使语义给出复杂，但得到了ETU一致性的证明。
AI 中文摘要
我们在内涵类型论中给出了显示集合oid（集合oid族）的新概念。它用于在安全的Agda中为带宇宙的外延类型论（ETU）提供语义，Agda是对内涵类型论进行机器可检查的形式化，通过归纳递归定义（IRU）封闭宇宙进行扩充。ETU的语法在IRU中以传统的外部形式定义，使用其项的良好作用域局部无名表示。由于IRU提供的表达手段非常有限，用显示集合oid给出其语义很复杂。作为推论，我们在IRU中得到了ETU一致性的证明。
英文摘要
We show that a certain notion of displayed setoid (family of setoids) in intensional type theory can be used to give a semantics for extensional type theory with universes (ETU). Safe Agda serves as a machine-checkable formalization of intentional type theory augmented with a universe closed under inductive-recursive definitions (IRU). The syntax of ETU is defined in IRU in a traditional extrinsic form, using a well-scoped locally nameless representation of its terms. Giving the semantics of ETU in terms of displayed setoids is complicated by the very limited means of expression afforded by IRU. As a corollary we obtain a proof within IRU of the consistency of ETU.
Comments33 pages
