Rathjen proved that Aczel's constructive set theory $\mathbf{CZF}$ extended with inaccessible sets of all transfinite orders can be interpreted in Martin-L\"{o}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\"{o}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.

翻译：Rathjen证明了Aczel的构造集合论$\mathbf{CZF}$通过添加所有超限阶的不可达集合，可以在Martin-Löf类型论$\mathbf{MLTT}$中通过扩展Setzer的马洛宇宙及其上方另一个宇宙进行解释。本文证明，若我们添加可达性谓词而非马洛宇宙上方的宇宙，该解释可自底向上实现。若在具有外延恒等类型的Martin-Löf类型论中工作，可达性谓词可通过$\mathrm{W}$-类型定义。我们解释的主要部分已在证明辅助工具Agda中形式化。