The cumulative hierarchy in Homotopy Type Theory
Ioannis Eleftheriadis

TL;DR
This paper investigates the cumulative hierarchy in Homotopy Type Theory, translating set theory formulas, analyzing axioms satisfaction, and modeling various constructive set theories within this framework.
Contribution
It demonstrates how to model set theories in HoTT's cumulative hierarchy and clarifies the axioms needed for different set theories.
Findings
V models ZF− in HoTT+PR
LEM is necessary for full ZF
Constructive set theories like ECST, IZF, and CZF are modeled in V
Abstract
We explore the cumulative hierarchy 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 . In particular, we show that 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Topology and Set Theory · Homotopy and Cohomology in Algebraic Topology · Advanced Topics in Algebra
