Martin-L\"{o}f type theory $\mathbf{MLTT}$ was extended by Setzer with the so-called Mahlo universe types. This extension is called $\mathbf{MLM}$ and was introduced to develop a variant of $\mathbf{MLTT}$ 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: $\mathbf{CZF}$. Rathjen, Griffor and Palmgren extended $\mathbf{CZF}$ with inaccessible sets of all transfinite orders. It is unknown whether this extension of $\mathbf{CZF}$ 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 $\mathbf{MLM}$ is not well understood. We extend $\mathbf{MLM}$ further by adding the accessibility predicate to it and show that the above extension of $\mathbf{CZF}$ is directly interpretable in $\mathbf{MLM}$ using the accessibility predicate.

翻译：马丁-洛夫类型论 $\mathbf{MLTT}$ 经Setzer扩展后引入了所谓马拉若宇宙类型。该扩展称为$\mathbf{MLM}$，旨在构建一个配备大基数类似物的$\mathbf{MLTT}$变体。在Aczel构造性集合论$\mathbf{CZF}$背景下，同样存在一个扩展了大集合类似物的构造系统实例。Rathjen、Griffor和Palmgren将$\mathbf{CZF}$扩展至包含所有超穷阶的不可达集。目前尚不清楚$\mathbf{CZF}$的这一扩展是否可直接通过马拉若宇宙进行解释。特别是，如何利用$\mathbf{MLM}$中马拉若宇宙的反射性质来构造不可达集的超穷层次结构尚未得到充分理解。我们通过向$\mathbf{MLM}$添加可达性谓词对其进一步扩展，并证明利用该可达性谓词，上述$\mathbf{CZF}$的扩展可直接在$\mathbf{MLM}$中得到解释。