Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
Yuta Takahashi
TL;DR
The paper shows that Aczel's constructive set theory with inaccessible sets ${\mathbf{CZF}_{\pi}}$ can be interpreted inside Martin-Löf type theory with Setzer's Mahlo universe ${\mathbf{MLM}}$ by replacing the need for a universe above the Mahlo universe with an accessibility predicate ${\mathrm{Acc}}$. It introduces a higher-order universe operator ${\mathrm{u}^{\mathbb{M}}}$ based on the Mahlo reflection and iterates it along ${\mathrm{Acc}}$ to build a transfinite hierarchy of subuniverses that model inaccessible sets, thereby realizing ${\mathbf{CZF}_{\pi}}$ in a bottom-up fashion. A central technical contribution is the construction of the transfinite hierarchy ${\mathcal{V}^{\alpha , t}_{(a , f)}}$ and the proof that these objects are ${\alpha}$-set-inaccessible, enabling a faithful type-theoretic interpretation. The main results are formalized in Agda, leveraging indexed induction-recursion to simulate the Mahlo universe and to define ${\mathrm{Acc}}$, providing a concrete, mechanized account of the interpretation. The work advances constructive set theory within type theory and suggests future HoTT-oriented refinements and explorations of diagonal fixed points in the transfinite hierarchy.
Abstract
Rathjen proved that Aczel's constructive set theory $\mathbf{CZF}$ extended with inaccessible sets of all transfinite orders can be interpreted in Martin-Löf type theory $\mathbf{MLTT}$ extended with Setzer's Mahlo universe and another universe above it. In this paper we show that this interpretation can be carried out bottom-up without the universe above the Mahlo universe, provided we add an accessibility predicate instead. If we work in Martin-Löf type theory with extensional identity types the accessibility predicate can be defined in terms of $\mathrm{W}$-types. The main part of our interpretation has been formalised in the proof assistant Agda.