The cumulative hierarchy in Homotopy Type Theory

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 $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.