Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe

Martin-Löf type theory 𝐌𝐋𝐓𝐓 was extended by Setzer with the so-called Mahlo universe types. This extension is called 𝐌𝐋𝐌 and was introduced to develop a variant of 𝐌𝐋𝐓𝐓 equipped with an analogue of a large cardinal. Another instance of constructive systems extended with an analogue of a large set was formulated in the context of Aczel's constructive set theory: 𝐂𝐙𝐅. Rathjen, Griffor and Palmgren extended 𝐂𝐙𝐅 with inaccessible sets of all transfinite orders. It is unknown whether this extension of 𝐂𝐙𝐅 is directly interpretable by Mahlo universes. In particular, how to construct the transfinite hierarchy of inaccessible sets using the reflection property of the Mahlo universe in 𝐌𝐋𝐌 is not well understood. We extend 𝐌𝐋𝐌 further by adding the accessibility predicate to it and show that the above extension of 𝐂𝐙𝐅 is directly interpretable in 𝐌𝐋𝐌 using the accessibility predicate.