The cumulative hierarchy in Homotopy Type Theory
Logic
2021-08-17 v1
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.
Keywords
Cite
@article{arxiv.2108.06348,
title = {The cumulative hierarchy in Homotopy Type Theory},
author = {Ioannis Eleftheriadis},
journal= {arXiv preprint arXiv:2108.06348},
year = {2021}
}
Comments
Appeared in the proceedings of the ESSLLI 2021 student session