  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.
