Martin-L\"{o}f type theory $\mathbf{MLTT}$ was extended by Setzer with the so-called Mahlo universe types. The extension of $\mathbf{MLTT}$ with one Mahlo universe 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. While Rathjen proved that this extended system of $\mathbf{CZF}$ is interpretable in an extension of $\mathbf{MLM}$ with one usual universe type above the Mahlo universe, it is unknown whether it can be interpreted by the Mahlo universe without a universe type above it. We extend $\mathbf{MLM}$ not by a universe type but by the accessibility predicate, and show that $\mathbf{CZF}$ with inaccessible sets can be interpreted in $\mathbf{MLM}$ with the accessibility predicate. Our interpretation of this extension of $\mathbf{CZF}$ is the same as that of Rathjen, Griffor and Palmgren formulated by $\mathbf{MLTT}$ with second-order universe operators, except that we construct the inaccessible sets by using the Mahlo universe and the accessibility predicate. We formalised the main part of our interpretation in the proof assistant Agda.

翻译：马丁-洛夫类型论 $\mathbf{MLTT}$ 曾被 Setzer 通过引入所谓的马洛宇宙类型进行扩展。这种带有一个马洛宇宙的 $\mathbf{MLTT}$ 扩展被称为 $\mathbf{MLM}$，其引入旨在发展一种配备了大基数类似物的 $\mathbf{MLTT}$ 变体。另一个在构造性系统中扩展了大集合类似物的实例是在 Aczel 的构造集合论 $\mathbf{CZF}$ 的背景下提出的。Rathjen、Griffor 和 Palmgren 将 $\mathbf{CZF}$ 扩展至包含所有超限阶的不可达集合。虽然 Rathjen 证明了 $\mathbf{CZF}$ 的这一扩展系统可在 $\mathbf{MLM}$ 的扩展（即在马洛宇宙之上增加一个常规宇宙类型）中得到解释，但尚不清楚它是否能在没有上层宇宙类型的马洛宇宙中得到解释。我们并非通过增加宇宙类型，而是通过可及性谓词来扩展 $\mathbf{MLM}$，并证明带有不可达集合的 $\mathbf{CZF}$ 可在配备可及性谓词的 $\mathbf{MLM}$ 中得到解释。我们对 $\mathbf{CZF}$ 这一扩展的解释与 Rathjen、Griffor 和 Palmgren 通过带二阶宇宙算子的 $\mathbf{MLTT}$ 所表述的解释相同，区别在于我们利用马洛宇宙和可及性谓词来构造不可达集合。我们已在证明辅助工具 Agda 中将我们解释的主要部分进行了形式化。