同伦类型论中的累积层次
The cumulative hierarchy in Homotopy Type Theory
摘要：
我们探索了HoTT书第10章中定义的累积层次结构$V$。我们首先展示了如何翻译公式的集合论在HotT，并继续检查哪些公理是满足$V$。特别是，我们表明$V$在HoTT+PR中对ZF $^-$进行建模，而LEM需要获得完整的ZF。最后，我们试图在V中建模建设性的集合论，虽然这是ECST实现的，我们只得到IZF和CZF与LEM。
英文摘要：
We explore the cumulative hierarchy $V$ defined in Chapter 10 of the HoTT book. We begin by showing how to translate formulas of set theory in HoTT, and proceed to examine which axioms are satisfied in $V$. In particular, we show that $V$ models ZF$^-$ in HoTT+PR, while LEM is required to obtain full ZF. Finally, we attempt to model constructive set theories in V, and although this is achieved for ECST, we only obtain IZF and CZF with LEM.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
