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

Yuta Takahashi0000-0002-5214-7077  Ochanomizu University, 2-1-1 Otsuka,
Bunkyo-ku, Tokyo 112-8610, Japan<EMAIL_ADDRESS>
###### Abstract.

Martin-Lö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.

###### Key words and phrases:

Martin-Löf type theory, constructive set theory, Mahlo universe types

This work is supported by JSPS KAKENHI Grant Number JP21K12822.

##  1\. Introduction

### Background and Aim

Martin-Löf type theory $\mathbf{MLTT}$ was extended by Setzer [21, 23] with
the so-called Mahlo universe types to provide a variant of $\mathbf{MLTT}$
equipped with an analogue of a large cardinal. Specifically, a Mahlo universe
$\mathbb{M}$ has a reflection property similar to that of weakly Mahlo
cardinals [11]: for any function $f$ of type
$\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}x\to\mathbb{M})\to\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}x\to\mathbb{M})$,
where $\mathrm{T}_{\mathbb{M}}$ is the decoding function for $\mathbb{M}$, the
universe $\mathbb{M}$ has the subuniverse which is closed under $f$ and
denoted by $\mathrm{U}_{f}$ (see, e.g., [6]). The resulting system,
$\mathbf{MLM}$, is thus an instance of a constructive system extended with an
analogue of a large set. Setzer’s purpose of introducing $\mathbf{MLM}$ is to
obtain an extension of $\mathbf{MLTT}$ whose proof-theoretic ordinal is
slightly greater than that of Kripke-Platek set theory with one recursively
Mahlo ordinal, where the proof-theoretic ordinals of a system enable
measurement of the proof-theoretic strength. The proof-theoretic ordinal of
$\mathbf{MLM}$ was determined by the results of [21, 23].

Another instance of constructive systems extended with an analogue of a large
set was developed in the context of Aczel’s constructive set theory:
$\mathbf{CZF}$ [1, 2, 3]. Rathjen, Griffor and Palmgren [17] introduced the
system $\mathbf{CZF}_{\pi}$, which is an extension of $\mathbf{CZF}$ with the
inaccessible sets of all transfinite orders [11]. The main purpose of
introducing $\mathbf{CZF}_{\pi}$ is a proof-theoretic one, as in the case of
Mahlo universes. Rathjen, Griffor and Palmgren also introduced an extension of
$\mathbf{MLTT}$ and determined a lower bound of its proof-theoretic ordinal by
verifying that $\mathbf{CZF}_{\pi}$ is interpretable in this extension. The
proof-theoretic ordinal of this extended system is equal to or greater than
that of $\mathbf{CZF}_{\pi}$, implying that the extended system has at least
the same proof-theoretic strength as $\mathbf{CZF}_{\pi}$.

In summary, $\mathbf{MLM}$ and $\mathbf{CZF}_{\pi}$ have been introduced as
instances of constructive systems equipped with an analogue of a large set.
According to [17, 9], the proof-theoretic ordinal of $\mathbf{CZF}_{\pi}$ is
smaller than that of $\mathbf{MLM}$; therefore, it can be conjectured that
$\mathbf{CZF}_{\pi}$ is interpretable in $\mathbf{MLM}$. Later, Rathjen [16]
introduced the notion of a Mahlo set into $\mathbf{CZF}$ and verified that
$\mathbf{CZF}$ with the axiom asserting the existence of one Mahlo set is
interpretable in $\mathbf{MLM}$. Moreover, he also showed that
$\mathbf{CZF}_{\pi}$ is interpretable in $\mathbf{CZF}$ with one Mahlo set.
Thus, it follows that one can embed $\mathbf{CZF}_{\pi}$ into $\mathbf{MLM}$
by combining these two interpretations.

However, it is unknown whether $\mathbf{CZF}_{\pi}$ is interpretable in
$\mathbf{MLM}$ directly. In particular, how to construct the transfinite
hierarchy of inaccessible sets using the reflection property of $\mathbb{M}$
is not well understood. Answering this question contributes to the
investigation of the interpretation between $\mathbf{MLTT}$ and $\mathbf{CZF}$
rather than ordinal analysis because the proof-theoretic ordinals of
$\mathbf{MLM}$ and $\mathbf{CZF}_{\pi}$ have already been determined.
Therefore, we examine the interpretations between the two constructive
frameworks, $\mathbf{MLTT}$ and $\mathbf{CZF}$, rather than the exact proof-
theoretic strength of the systems in these frameworks. This justifies our
strategy for tackling the question: below, we add the accessibility predicate
$\mathrm{Acc}$ to $\mathbf{MLM}$, which is an example of inductive predicates
being definable in proof assistants, such as Coq and Agda. The addition of
$\mathrm{Acc}$ to $\mathbf{MLM}$ enables the perspicuous development of a
transfinite iteration of a higher-order universe operator defined in
$\mathbf{MLM}$.

In this paper, we show that $\mathbf{CZF}_{\pi}$ is directly interpretable in
$\mathbf{MLM}$ with the accessibility predicate $\mathrm{Acc}$. We first
define a higher-order universe operator using the reflection property of
$\mathbb{M}$ in $\mathbf{MLM}$. Next, the transfinite hierarchy of Aczel’s
iterative sets is constructed by iterating this universe operator along the
accessibility given by $\mathrm{Acc}$. Finally, we verify that these sets are
indeed type-theoretic counterparts of inaccessible sets.

### Related Work

The interpretation of $\mathbf{CZF}$ in $\mathbf{MLTT}$ was first discussed in
[1]. Here Aczel set out $\mathbf{CZF}$ and interpreted it in the fragment
$\mathbf{ML_{1}V}$ of $\mathbf{MLTT}$, which has dependent function types
(i.e., $\Pi$-types), dependent pair types (i.e., $\Sigma$-types), disjoint
union types, the empty type, the unit type, the natural number type, the
universe type and an instance of $\mathrm{W}$-types. Iterative sets in
$\mathbf{CZF}$ were interpreted by this instance of $\mathrm{W}$-types. Later,
the set-theoretic axiom of dependent choice was interpreted in the extension
of $\mathbf{ML_{1}V}$ by extensional identity types ([2]). Moreover, the
regular extension axiom ($\mathbf{REA}$), which states that any set is a
subset of a regular set, was interpreted by further adding $\mathrm{W}$-types
([3]).

Griffor and Rathjen [9] showed that $\mathbf{CZF}$ and $\mathbf{ML_{1}V}$ have
the same proof-theoretic strength and there is a fragment of $\mathbf{MLTT}$
with the same proof-theoretic strength as $\mathbf{CZF}+\mathbf{REA}$. Setzer
[20, 19] determined the proof-theoretic strength of the standard formulation
of $\mathbf{MLTT}$, i.e., the system obtained from $\mathbf{ML_{1}V}$ by
adding intensional identity types and $\mathrm{W}$-types. He computed the
proof-theoretic ordinal of the standard system, without appealing to Aczel’s
interpretation of $\mathbf{CZF}$ in $\mathbf{MLTT}$.

As aforementioned, Rathjen, Griffor and Palmgren [17] introduced the extension
$\mathbf{CZF}_{\pi}$ of $\mathbf{CZF}$ by the axiom asserting the existence of
inaccessible sets of all transfinite orders. The type system in which
$\mathbf{CZF}_{\pi}$ was interpreted is $\mathbf{MLQ}$, which is an extension
of $\mathbf{MLTT}$ by the inductive type $\mathrm{Q}$ and universe type
$\mathrm{M}$: $\mathrm{Q}$ is an inductive type of codes for operators which
provides universes closed under universe operators constructed previously, and
$\mathrm{M}$ is a universe closed under the operators whose codes belong to
$\mathrm{Q}$. Our higher-order universe operator is inspired by the one
defined with the types $\mathrm{Q}$ and $\mathrm{M}$, and our interpretation
of $\mathbf{CZF}_{\pi}$ is the same as that of [17], except for the
interpretation of inaccessible sets. Rathjen [15] introduced the fragment
$\mathbf{MLF}$ of $\mathbf{MLQ}$ and showed that two weaker variants of
$\mathbf{CZF}_{\pi}$ have the same proof-theoretic strength as $\mathbf{MLF}$.

The relationship between $\mathbf{MLM}$ and $\mathbf{CZF}$ has already been
examined by Rathjen [16], as shown above. He introduced the notion of a Mahlo
set into $\mathbf{CZF}$ and verified that $\mathbf{CZF}$ with the axiom
asserting the existence of one Mahlo set is interpretable in $\mathbf{MLM}$.
He also showed that $\mathbf{CZF}_{\pi}$ is interpretable in $\mathbf{CZF}$
with one Mahlo set, but the direct interpretation of $\mathbf{CZF}_{\pi}$ in
$\mathbf{MLM}$ was not discussed.

### Contributions

Our contributions are summarised as follows:

  1. (1)

The principal contribution of this paper is the construction of inaccessible
sets of transfinite orders in $\mathbf{MLM}$ with the accessibility predicate
$\mathrm{Acc}$. To describe this interpretation, we use both the reflection
property of $\mathbb{M}$ and accessibility predicate $\mathrm{Acc}$. We define
a higher-order universe operator with the reflection property of $\mathbb{M}$
and iterate this operator along the accessibility given by $\mathrm{Acc}$.

  2. (2)

A secondary contribution is the use of the accessibility predicate
$\mathrm{Acc}$. As aforementioned, the iteration of the higher-order universe
operator continues along the accessibility given by $\mathrm{Acc}$, which
clarifies which recursion principle is used to define the type-theoretic
interpretation of inaccessible sets.

### Organisation of the Paper

In Section 2, we describe the system $\mathbf{MLM}$ and define a higher-order
universe operator using the reflection property of the Mahlo universe
$\mathbb{M}$. Section 3 first provides a brief introduction to
$\mathbf{CZF}_{\pi}$ and then shows that $\mathbf{CZF}_{\pi}$ is directly
interpretable in $\mathbf{MLM}$ with the accessibility predicate
$\mathrm{Acc}$. Specifically, we iterate the application of our higher-order
operator along the accessibility given by $\mathrm{Acc}$ to construct the
hierarchy of inaccessible sets in $\mathbf{MLM}$.

##  2\. A Higher-Order Universe Operator by the Mahlo Universe in
$\mathbf{MLM}$

In this section, we first present the system $\mathbf{MLM}$ of Martin-Löf type
theory with one Mahlo universe (Section 2.1). Next, we formulate a higher-
order universe operator using the reflection property of the Mahlo universe
(Section 2.2). This operator will be used to construct the transfinite
hierarchy of inaccessible sets.

###  2.1. Martin-Löf Type Theory with One Mahlo Universe

We follow Setzer’s work [21, 23, 22] in defining the rules of universes in the
system $\mathbf{MLM}$ of Martin-Löf type theory with one Mahlo universe, while
we follow [10, 20] in defining the inference rules other than those of
universes. The system $\mathbf{MLM}$ is an intensional $\mathbf{MLTT}$ (i.e.,
an $\mathbf{MLTT}$ with the intensional identity types) formulated in the
polymorphic way. See [13, 7] for the distinction between intensional
$\mathbf{MLTT}$’s and extensional ones; see [13] for the distinction between
the polymorphic formulation and the monomorphic one.

In this paper, syntactic variables are used possibly with suffixes. Let an
infinite set of variables be given. Variables are denoted by $x,y,z,v,w$, and
numerals $0,1,\ldots$ are denoted by $n,m,k$. Pre-terms $a,b,c,\ldots$ and
pre-types $A,B,C,\ldots$ are defined by simultaneous induction in Table 1. The
intuitive meanings of pre-terms and pre-types will be explained by the
inference rules of $\mathbf{MLM}$.

$\displaystyle a,b,c,d,f,g,h,l::=$ $\displaystyle\>x\mid 0\mid
m_{n}\mid\lambda
x.a\mid\mathsf{app}(a,b)\mid(a,b)\mid\mathsf{E}_{\Sigma}(a,b)\mid$
$\displaystyle\>\mathsf{i}(a)\mid\mathsf{j}(a)\mid\mathsf{E}_{+}(a,b,c)\mid\mathsf{suc}(a)\mid\mathsf{E}_{\mathrm{N}}(a,b,c)\mid$
$\displaystyle\>\mathsf{E}_{n}(a_{0},\ldots,a_{n})\mid\mathsf{sup}(a,b)\mid\mathsf{E}_{\mathrm{W}}(a,b)\mid\mathsf{refl}(a)\mid\mathsf{E}_{\mathrm{Id}}(a,b)\mid$
$\displaystyle\>\widehat{\mathrm{N}}_{\mathbb{M}}\mid\widehat{\mathrm{N}_{n}}_{\mathbb{M}}\mid\widehat{\Pi}_{\mathbb{M}}(a,b)\mid\widehat{\Sigma}_{\mathbb{M}}(a,b)\mid
a\widehat{+}_{\mathbb{M}}b\mid\widehat{\mathrm{W}}_{\mathbb{M}}(a,b)\mid$
$\displaystyle\>\widehat{\mathrm{Id}}_{\mathbb{M}}(a,b,c)\mid\widehat{\mathrm{U}}_{f}\mid\widehat{\mathrm{T}}_{f}(a)\mid\mathsf{res}^{0}_{f}(a,b)\mid\mathsf{res}^{1}_{f}(a,b,c)$
$\displaystyle\>\widehat{\mathrm{N}}_{f}\mid\widehat{\mathrm{N}_{n}}_{f}\mid\widehat{\Pi}_{f}(a,b)\mid\widehat{\Sigma}_{f}(a,b)\mid
a\widehat{+}_{f}b\mid\widehat{\mathrm{W}}_{f}(a,b)\mid\widehat{\mathrm{Id}}_{f}(a,b,c)$
$\displaystyle A,B,C,D::=$
$\displaystyle\>\mathrm{N}\mid\mathrm{N}_{n}\mid\mathbb{M}\mid\mathrm{U}_{f}\mid\Pi_{(x:A)}B\mid\Sigma_{(x:A)}B\mid
A+B\mid$
$\displaystyle\>\mathrm{W}_{(x:A)}B\mid\mathrm{Id}(A,a,b)\mid\mathrm{T}_{\mathbb{M}}(a)$
Table 1. Pre-Terms and Pre-Types

The pre-terms of the form $\mathsf{app}(a,b)$ are abbreviated as $a\>b$. When
a variable $x$ is not free in $B$, we write $\Pi_{(x:A)}B$ as $A\to B$, and
$\Sigma_{(x:A)}B$ as $A\times B$. The occurrences of $x$ are bound in the
expressions of the form $\Pi_{(x:A)}B,\Sigma_{(x:A)}B,\mathrm{W}_{(x:A)}B$ or
$\lambda x.a$. Consecutive applications $k_{1}(k_{2}(\cdots k_{n}(a)\cdots))$
of $\mathsf{i},\mathsf{j}$ with
$k_{1},k_{2},\ldots,k_{n}\in\\{\mathsf{i},\mathsf{j}\\}$ are abbreviated as
$k_{1}k_{2}\cdots k_{n}a$. Any two $\alpha$-equivalent expressions are
identified. In addition, we adopt Barendregt’s variable condition: no variable
occurs both as a free one and as a bound one in an expression, and all bound
variables in an expression are distinct. We denote by
$e[e_{1}/x_{1},\ldots,e_{n}/x_{n}]$ the expression obtained by substituting
$e_{1},\ldots,e_{n}$ for $x_{1},\ldots,x_{n}$ in $e$ consecutively. We always
assume that no bound variable in $e$ occurs freely in any of
$e_{1},\ldots,e_{n}$, by applying the $\alpha$-conversion if necessary.

Judgements are expressions which have one of the following forms:

  * •

$\vdash\Gamma\;\mathrm{ctxt}$, which means that $\Gamma$ is a valid context,

  * •

$\Gamma\vdash A\;\mathrm{type}$, which means that $A$ is a type in a context
$\Gamma$,

  * •

$\Gamma\vdash a:A$, which means that $a$ is a term of type $A$ in a context
$\Gamma$,

  * •

$\vdash\Gamma=\Delta\;\mathrm{ctxt}$, which means that $\Gamma$ and $\Delta$
are definitionally equal contexts,

  * •

$\Gamma\vdash A=B$, which means that $A$ and $B$ are definitionally equal
types in a context $\Gamma$,

  * •

$\Gamma\vdash a=b:A$, which means that $a$ and $b$ are definitionally equal
terms of type $A$ in a context $\Gamma$.

According to the propositions-as-types conception, $\Gamma\vdash a:A$ means
that $a$ is a proof of the proposition $A$ in the context $\Gamma$. One can
consider two definitionally equal expressions to be two expressions whose
results of computation are equal. We denote by $\theta$ an expression of one
of the following forms:

$A\;\mathrm{type},\qquad a:A,\qquad A=B,\qquad a=b:A.$

The system $\mathbf{MLM}$ is a formal system to derive judgements of the forms
above by means of inference rules. Its inference rules are classified as
follows.

  * •

General rules: those of contexts, assumptions, substitutions and the
definitional equality,

  * •

Rules for standard types: those of $\Pi$-types, $\Sigma$-types, $+$-types,
$\mathrm{N}$-type, $\mathrm{N}_{n}$-types, $\mathrm{W}$-types and
$\mathrm{Id}$-types,

  * •

Rules for universe types: those of Mahlo universe types and non-Mahlo universe
types.

Each collection of rules for standard types includes the formation rule, the
introduction rules, the elimination rules and the equality rules. The
formation rule explains how to form the types, and the introduction rules
enable the construction of canonical elements of the types. On the other hand,
the elimination rules provide executable elements of the types, and the
equality rules specify how to execute (or compute) these elements in an
equational way. For detailed explanations of the above rules except those of
Mahlo universes, see e.g. [12, 13, 10, 7]. Below we denote the Mahlo universe
in $\mathbf{MLM}$ by $\mathbb{M}$, while it is denoted by $\mathrm{V}$ in [21,
23, 22]. [Inference Rules and Judgements in $\mathbf{MLM}$] Judgements in
$\mathbf{MLM}$ are those which are derivable by the following inference rules
of $\mathbf{MLM}$:

Rules for Contexts:

let $x$ be fresh for $\Gamma$, and $y$ be fresh for $\Delta$.

$\vdash\emptyset\;\mathrm{ctxt}\qquad\vdash\Gamma,x:A\;\mathrm{ctxt}\Gamma\vdash
A\;\mathrm{type}\qquad\vdash\Gamma,x:A=\Delta,y:B\;\mathrm{ctxt}\lx@proof@logical@and\vdash\Gamma=\Delta\;\mathrm{ctxt}\Gamma\vdash
A=B\qquad\Delta\vdash A\;\mathrm{type}\lx@proof@logical@and\Gamma\vdash
A\;\mathrm{type}\vdash\Gamma=\Delta\;\mathrm{ctxt}$
$\vdash\Gamma=\Gamma\;\mathrm{ctxt}\vdash\Gamma\;\mathrm{ctxt}\qquad\vdash\Delta=\Gamma\;\mathrm{ctxt}\vdash\Gamma=\Delta\;\mathrm{ctxt}\qquad\vdash\Gamma=\Theta\;\mathrm{ctxt}\lx@proof@logical@and\vdash\Gamma=\Delta\;\mathrm{ctxt}\vdash\Delta=\Theta\;\mathrm{ctxt}$

Rule for Assumptions:

$\Gamma,x:A,\Delta\vdash x:A\vdash\Gamma,x:A,\Delta\;\mathrm{ctxt}$

Rules for Substitutions:

$\Gamma,\Delta[a/x]\vdash\theta[a/x]\lx@proof@logical@and\Gamma\vdash
a:A\Gamma,x:A,\Delta\vdash\theta\qquad\Gamma,\Delta[a/x]\vdash
B[a/x]=B[b/x]\lx@proof@logical@and\Gamma\vdash a=b:A\Gamma,x:A,\Delta\vdash
B\;\mathrm{type}$ $\Gamma,\Delta[a/x]\vdash
c[a/x]=c[b/x]:B[a/x]\lx@proof@logical@and\Gamma\vdash
a=b:A\Gamma,x:A,\Delta\vdash c:B$

Hereafter, we list the premises of an inference rule in the vertical way.

Rules for Definitional Equality:

$\Gamma\vdash a=a:A\Gamma\vdash a:A\qquad\Gamma\vdash b=a:A\Gamma\vdash
a=b:A\qquad\Gamma\vdash a=c:A\Gamma\vdash b=c:A\Gamma\vdash a=b:A$
$\Gamma\vdash A=A\Gamma\vdash A\;\mathrm{type}\qquad\Gamma\vdash
B=A\Gamma\vdash A=B\qquad\Gamma\vdash A=C\Gamma\vdash B=C\Gamma\vdash
A=B\qquad\Delta\vdash a:B\Gamma\vdash
A=B\vdash\Gamma=\Delta\;\mathrm{ctxt}\Gamma\vdash a:A$

Rules for $\Pi$-Types:

we have the formation rule $\Pi\mathsf{fm}$, the introduction rule
$\Pi\mathsf{in}$, the elimination rule $\Pi\mathsf{el}$ and the equality rule
$\Pi\mathsf{eq}$ for $\Pi$-types.

$\Gamma\vdash\Pi_{(x:A)}B\;\mathrm{type}\Gamma,x:A\vdash
B\;\mathrm{type}\Gamma\vdash A\;\mathrm{type}\qquad\Gamma\vdash\lambda
x.b:\Pi_{(x:A)}B\Gamma,x:A\vdash b:B$ $\Gamma\vdash b\>a:B[a/x]\Gamma\vdash
a:A\Gamma\vdash b:\Pi_{(x:A)}B\Gamma,x:A\vdash
B\;\mathrm{type}\qquad\Gamma\vdash(\lambda x.b)a=b[a/x]:B[a/x]\Gamma\vdash
a:A\Gamma,x:A\vdash b:B$

Moreover, we have a congruence rule for each of
$\Pi\mathsf{fm},\Pi\mathsf{in},\Pi\mathsf{el}$ as follows.

$\Gamma\vdash\Pi_{(x:A_{1})}B_{1}=\Pi_{(x:A_{2})}B_{2}\Gamma,x:A_{1}\vdash
B_{1}=B_{2}\Gamma\vdash A_{1}=A_{2}\qquad\Gamma\vdash\lambda x.b_{1}=\lambda
x.b_{2}:\Pi_{(x:A)}B\Gamma,x:A\vdash b_{1}=b_{2}:B$ $\Gamma\vdash
b_{1}a_{1}=b_{2}a_{2}:B[a_{1}/x]\Gamma\vdash a_{1}=a_{2}:A\Gamma\vdash
b_{1}=b_{2}:\Pi_{(x:A)}B\Gamma,x:A\vdash B\;\mathrm{type}$

As in the case of $\Pi$-types, for any
$\ast\in\\{\Sigma,+,\mathrm{N}_{n},\mathrm{N},\mathrm{W},\mathrm{Id}\\}$, we
use the labels $\ast\mathsf{fm},\ast\mathsf{in},\ast\mathsf{el}$ and
$\ast\mathsf{eq}$ possibly with suffixes to denote $\ast$-formation rules,
$\ast$-introduction rules, $\ast$-elimination rules and $\ast$-equality rules,
respectively. Hereafter, we omit to write down congruence rules: we assume
that congruence rules are formulated for the $\ast$-formation,
$\ast$-introduction and $\ast$-elimination rules except
$\mathrm{N}\mathsf{fm},\mathrm{N}_{n}\mathsf{fm},\mathrm{N}\mathsf{in}_{0},\mathrm{N}_{n}\mathsf{in}$.

Rules for $\Sigma$-Types:

we have the following rules.

$\Gamma\vdash\Sigma_{(x:A)}B\;\mathrm{type}\Gamma,x:A\vdash
B\;\mathrm{type}\Gamma\vdash
A\;\mathrm{type}\quad\Gamma\vdash(a,b):\Sigma_{(x:A)}B\Gamma\vdash
b:B[a/x]\Gamma\vdash a:A\Gamma,x:A\vdash
B\;\mathrm{type}\quad\Gamma\vdash\mathsf{E}_{\Sigma}(b,c):C[b/z]\Gamma\vdash
b:\Sigma_{(x:A)}B\Gamma\vdash
c:\Pi_{(x:A)}\Pi_{(y:B)}C[(x,y)/z]\Gamma,z:\Sigma_{(x:A)}B\vdash
C\;\mathrm{type}$
$\Gamma\vdash\mathsf{E}_{\Sigma}((a,b),c)=c\>a\>b:C[(a,b)/z]\Gamma\vdash
c:\Pi_{(x:A)}\Pi_{(y:B)}C[(x,y)/z]\Gamma,z:\Sigma_{(x:A)}B\vdash
C\;\mathrm{type}\Gamma\vdash b:B[a/x]\Gamma\vdash a:A\Gamma,x:A\vdash
B\;\mathrm{type}$

It is straightforward to define the left projection $\mathsf{p}_{1}$ and the
right projection $\mathsf{p}_{2}$ satisfying the following:

$\Gamma\vdash\mathsf{p}_{1}c:A\Gamma\vdash c:\Sigma_{(x:A)}B\Gamma,x:A\vdash
B\;\mathrm{type}\qquad\Gamma\vdash\mathsf{p}_{1}(a,b)=a:A\Gamma\vdash
b:B[a/x]\Gamma\vdash a:A\Gamma,x:A\vdash B\;\mathrm{type}$
$\Gamma\vdash\mathsf{p}_{2}c:B[\mathsf{p}_{1}(c)/x]\Gamma\vdash
c:\Sigma_{(x:A)}B\Gamma,x:A\vdash
B\;\mathrm{type}\qquad\Gamma\vdash\mathsf{p}_{2}(a,b)=b:B[\mathsf{p}_{1}(a,b)/x]\Gamma\vdash
b:B[a/x]\Gamma\vdash a:A\Gamma,x:A\vdash B\;\mathrm{type}$

Rules for $+$-Types:

a sum type $A+B$ corresponds to a disjoint sum of $A$ and $B$.

$\Gamma\vdash A+B\;\mathrm{type}\Gamma\vdash B\;\mathrm{type}\Gamma\vdash
A\;\mathrm{type}\qquad\Gamma\vdash\mathsf{i}(a):A+B\Gamma\vdash
B\;\mathrm{type}\Gamma\vdash
a:A\qquad\Gamma\vdash\mathsf{j}(b):A+B\Gamma\vdash b:B\Gamma\vdash
A\;\mathrm{type}$
$\Gamma\vdash\mathsf{E}_{+}(d,c_{1},c_{2}):C[d/x]\Gamma\vdash
d:A+B\Gamma\vdash c_{2}:\Pi_{(z:B)}C[\mathsf{j}(z)/x]\Gamma\vdash
c_{1}:\Pi_{(y:A)}C[\mathsf{i}(y)/x]\Gamma,x:A+B\vdash C\;\mathrm{type}$
$\Gamma\vdash\mathsf{E}_{+}(\mathsf{i}(a),c_{1},c_{2})=c_{1}\>a:C[\mathsf{i}(a)/x]\Gamma\vdash
a:A\Gamma\vdash c_{2}:\Pi_{(z:B)}C[\mathsf{j}(z)/x]\Gamma\vdash
c_{1}:\Pi_{(y:A)}C[\mathsf{i}(y)/x]\Gamma,x:A+B\vdash
C\;\mathrm{type}\qquad\Gamma\vdash\mathsf{E}_{+}(\mathsf{j}(b),c_{1},c_{2})=c_{2}\>b:C[\mathsf{j}(b)/x]\Gamma\vdash
b:B\Gamma\vdash c_{2}:\Pi_{(z:B)}C[\mathsf{j}(z)/x]\Gamma\vdash
c_{1}:\Pi_{(y:A)}C[\mathsf{i}(y)/x]\Gamma,x:A+B\vdash C\;\mathrm{type}$

Rules for $\mathrm{N}$-Type:

the $\mathrm{N}$-type is the type of natural numbers. Its elimination rule is
the induction principle on $\mathrm{N}$.

$\Gamma\vdash\mathrm{N}\;\mathrm{type}\vdash\Gamma\;\mathrm{ctxt}\qquad\Gamma\vdash
0:\mathrm{N}\vdash\Gamma\;\mathrm{ctxt}\qquad\Gamma\vdash\mathsf{suc}(a):\mathrm{N}\Gamma\vdash
a:\mathrm{N}$ $\Gamma\vdash\mathsf{E}_{\mathrm{N}}(a,b,c):C[a/x]\Gamma\vdash
c:\Pi_{(x:\mathrm{N})}(C\to C[\mathsf{suc}(x)/x])\Gamma\vdash
b:C[0/x]\Gamma\vdash a:\mathrm{N}\Gamma,x:\mathrm{N}\vdash
C\;\mathrm{type}\qquad\Gamma\vdash\mathsf{E}_{\mathrm{N}}(0,b,c)=b:C[0/x]\Gamma\vdash
c:\Pi_{(x:\mathrm{N})}(C\to C[\mathsf{suc}(x)/x])\Gamma\vdash
b:C[0/x]\Gamma,x:\mathrm{N}\vdash C\;\mathrm{type}$
$\Gamma\vdash\mathsf{E}_{\mathrm{N}}(\mathsf{suc}(a),b,c)=c\>a\>(\mathsf{E}_{\mathrm{N}}(a,b,c)):C[\mathsf{suc}(a)/x]\Gamma\vdash
c:\Pi_{(x:\mathrm{N})}(C\to C[\mathsf{suc}(x)/x])\Gamma\vdash
b:C[0/x]\Gamma\vdash a:\mathrm{N}\Gamma,x:\mathrm{N}\vdash C\;\mathrm{type}$

Rules for $\mathrm{N}_{n}$-Type:

the $\mathrm{N}_{n}$-type is the type of finite set with $n$ members.

$\Gamma\vdash\mathrm{N}_{n}\;\mathrm{type}\vdash\Gamma\;\mathrm{ctxt}\qquad\Gamma\vdash
m_{n}:\mathrm{N}_{n}\vdash\Gamma\;\mathrm{ctxt}$
$\Gamma\vdash\mathsf{E}_{n}(a,b_{0},\ldots,b_{n-1}):C[a/x]\Gamma\vdash
b_{n-1}:C[(n-1)_{n}/x]\Gamma\vdash b_{0}:C[0_{n}/x]\Gamma\vdash
a:\mathrm{N}_{n}\Gamma,x:\mathrm{N}_{n}\vdash
C\;\mathrm{type}\quad\Gamma\vdash\mathsf{E}_{n}(m_{n},b_{0},\ldots,b_{n-1})=b_{m}:C[m_{n}/x]\Gamma\vdash
b_{n-1}:C[(n-1)_{n}/x]\Gamma\vdash
b_{0}:C[0_{n}/x]\Gamma,x:\mathrm{N}_{n}\vdash C\;\mathrm{type}$

Rules for $\mathrm{W}$-Types:

a $\mathrm{W}$-type $\mathrm{W}_{(x:A)}B$ corresponds to the type of well
founded trees such that each of their branchings is indexed by $B[a/x]$ for
some $a:A$. Its elimination rule is the induction principle on a well-founded
tree.

$\Gamma\vdash\mathrm{W}_{(x:A)}B\;\mathrm{type}\Gamma,x:A\vdash
B\;\mathrm{type}\Gamma\vdash
A\;\mathrm{type}\qquad\Gamma\vdash\mathsf{sup}(a,b):\mathrm{W}_{(x:A)}B\Gamma\vdash
b:B[a/x]\to\mathrm{W}_{(x:A)}B\Gamma\vdash a:A\Gamma,x:A\vdash
B\;\mathrm{type}$
$\Gamma\vdash\mathsf{E}_{\mathrm{W}}(a,b):C[a/y^{\prime}]\Gamma\vdash
b:\Pi_{(y:A)}\Pi_{(z:B[y/x]\to\mathrm{W}_{(x:A)}B)}(\Pi_{(v:B[y/x])}C[z\>v/y^{\prime}]\to
C[\mathsf{sup}(y,z)/y^{\prime}])\Gamma\vdash
a:\mathrm{W}_{(x:A)}B\Gamma,y^{\prime}:\mathrm{W}_{(x:A)}B\vdash
C\;\mathrm{type}\Gamma,x:A\vdash B\;\mathrm{type}$
$\Gamma\vdash\mathsf{E}_{\mathrm{W}}(\mathsf{sup}(a,b),c)=c\>a\>b\>(\lambda
v.\mathsf{E}_{\mathrm{W}}(\mathsf{app}(b,v),c)):C[\mathsf{sup}(a,b)/y^{\prime}]\Gamma\vdash
c:\Pi_{(y:A)}\Pi_{(z:B[y/x]\to\mathrm{W}_{(x:A)}B)}(\Pi_{(v:B[y/x])}C[z\>v/y^{\prime}]\to
C[\mathsf{sup}(y,z)/y^{\prime}])\Gamma\vdash
b:B[a/x]\to\mathrm{W}_{(x:A)}B\Gamma\vdash
a:A\Gamma,y^{\prime}:\mathrm{W}_{(x:A)}B\vdash
C\;\mathrm{type}\Gamma,x:A\vdash B\;\mathrm{type}$

Rules for $\mathrm{Id}$-Types:

an $\mathrm{Id}$-type $\mathrm{Id}(A,a_{1},a_{2})$ corresponds to an identity
statement which says that $a_{1}$ and $a_{2}$ are equal elements of $A$.

$\Gamma\vdash\mathrm{Id}(A,a_{1},a_{2})\;\mathrm{type}\Gamma\vdash
a_{2}:A\Gamma\vdash a_{1}:A\Gamma\vdash
A\;\mathrm{type}\qquad\Gamma\vdash\mathsf{refl}(a):\mathrm{Id}(A,a,a)\Gamma\vdash
a:A$ $\Gamma\vdash\mathsf{E}_{\mathrm{Id}}(d,c):C[a/x,b/y,d/z]\Gamma\vdash
d:\mathrm{Id}(A,a,b)\Gamma\vdash b:A\Gamma\vdash a:A\Gamma\vdash
c:\Pi_{(v:A)}C[v/x,v/y,\mathsf{refl}(v)/z]\Gamma,x:A,y:A,z:\mathrm{Id}(A,x,y)\vdash
C\;\mathrm{type}$
$\Gamma\vdash\mathsf{E}_{\mathrm{Id}}(\mathsf{refl}(a),c)=c\>a:C[a/x,a/y,\mathsf{refl}(a)/z]\Gamma\vdash
a:A\Gamma\vdash
c:\Pi_{(v:A)}C[v/x,v/y,\mathsf{refl}(v)/z]\Gamma,x:A,y:A,z:\mathrm{Id}(A,x,y)\vdash
C\;\mathrm{type}$

Rules for Mahlo Universe $(\mathbb{M},\mathrm{T}_{\mathbb{M}})$:

we have the rules $\mathbb{M}\mathsf{fm}$, $\mathbb{M}\mathsf{in}$ and
$\mathrm{T}_{\mathbb{M}}\mathsf{fm}$ with the inference rules which define the
decoding function $\mathrm{T}_{\mathbb{M}}$ recursively. Congruence rules are
defined for the $\mathrm{T}_{\mathbb{M}}$-formation rule
$\mathrm{T}_{\mathbb{M}}\mathsf{fm}$ and all $\mathbb{M}$-introduction rules
$\mathbb{M}\mathsf{in}$ except $\mathbb{M}\mathsf{in}_{\mathrm{N}}$ and
$\mathbb{M}\mathsf{in}_{\mathrm{N}_{n}}$, though we omit to write down them.

$\Gamma\vdash\mathbb{M}\;\mathrm{type}\vdash\Gamma\;\mathrm{ctxt}\qquad\Gamma\vdash\mathrm{T}_{\mathbb{M}}(a)\;\mathrm{type}\Gamma\vdash
a:\mathbb{M}\qquad\Gamma\vdash\widehat{\mathrm{N}}_{\mathbb{M}}:\mathbb{M}\vdash\Gamma\;\mathrm{ctxt}\qquad\Gamma\vdash\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{N}}_{\mathbb{M}})=\mathrm{N}\vdash\Gamma\;\mathrm{ctxt}$
$\Gamma\vdash\widehat{\mathrm{N}_{n}}_{\mathbb{M}}:\mathbb{M}\vdash\Gamma\;\mathrm{ctxt}\qquad\Gamma\vdash\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{N}_{n}}_{\mathbb{M}})=\mathrm{N}_{n}\vdash\Gamma\;\mathrm{ctxt}$
$\Gamma\vdash\widehat{\Pi}_{\mathbb{M}}(a,b):\mathbb{M}\Gamma\vdash
b:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}\Gamma\vdash
a:\mathbb{M}\qquad\Gamma\vdash\mathrm{T}_{\mathbb{M}}(\widehat{\Pi}_{\mathbb{M}}(a,b))=\Pi_{(x:\mathrm{T}_{\mathbb{M}}(a))}\mathrm{T}_{\mathbb{M}}(b\>x)\Gamma\vdash
b:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}\Gamma\vdash a:\mathbb{M}$
$\Gamma\vdash\widehat{\Sigma}_{\mathbb{M}}(a,b):\mathbb{M}\Gamma\vdash
b:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}\Gamma\vdash
a:\mathbb{M}\qquad\Gamma\vdash\mathrm{T}_{\mathbb{M}}(\widehat{\Sigma}_{\mathbb{M}}(a,b))=\Sigma_{(x:\mathrm{T}_{\mathbb{M}}(a))}\mathrm{T}_{\mathbb{M}}(b\>x)\Gamma\vdash
b:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}\Gamma\vdash a:\mathbb{M}$
$\Gamma\vdash a\widehat{+}_{\mathbb{M}}b:\mathbb{M}\Gamma\vdash
b:\mathbb{M}\Gamma\vdash
a:\mathbb{M}\qquad\Gamma\vdash\mathrm{T}_{\mathbb{M}}(a\widehat{+}_{\mathbb{M}}b)=\mathrm{T}_{\mathbb{M}}(a)+\mathrm{T}_{\mathbb{M}}(b)\Gamma\vdash
b:\mathbb{M}\Gamma\vdash a:\mathbb{M}$
$\Gamma\vdash\widehat{\mathrm{W}}_{\mathbb{M}}(a,b):\mathbb{M}\Gamma\vdash
b:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}\Gamma\vdash
a:\mathbb{M}\qquad\Gamma\vdash\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{W}}_{\mathbb{M}}(a,b))=\mathrm{W}_{(x:\mathrm{T}_{\mathbb{M}}(a))}\mathrm{T}_{\mathbb{M}}(b\>x)\Gamma\vdash
b:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}\Gamma\vdash a:\mathbb{M}$
$\Gamma\vdash\widehat{\mathrm{Id}}_{\mathbb{M}}(a,b,c):\mathbb{M}\Gamma\vdash
c:\mathrm{T}_{\mathbb{M}}(a)\Gamma\vdash
b:\mathrm{T}_{\mathbb{M}}(a)\Gamma\vdash
a:\mathbb{M}\qquad\Gamma\vdash\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{Id}}_{\mathbb{M}}(a,b,c))=\mathrm{Id}(\mathrm{T}_{\mathbb{M}}(a),b,c)\Gamma\vdash
c:\mathrm{T}_{\mathbb{M}}(a)\Gamma\vdash
b:\mathrm{T}_{\mathbb{M}}(a)\Gamma\vdash a:\mathbb{M}$

The rules concerning the codes of non-Mahlo universes are as follows:

$\Gamma\vdash\widehat{\mathrm{U}}_{f}:\mathbb{M}\Gamma\vdash
f:\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})\to\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})$
$\Gamma\vdash\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{U}}_{f})=\mathrm{U}_{f}\Gamma\vdash
f:\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})\to\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})$
$\Gamma\vdash\widehat{\mathrm{T}}_{f}(a):\mathbb{M}\Gamma\vdash
a:\mathrm{U}_{f}\Gamma\vdash
f:\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})\to\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})$

Rules for Non-Mahlo Universes $(\mathrm{U}_{f},\widehat{\mathrm{T}}_{f})$:

below we define the $\mathrm{U}_{f}$-formation rule
$\mathrm{U}_{f}\mathsf{fm}$, the $\mathrm{U}_{f}$-introduction rules
$\mathrm{U}_{f}\mathsf{in}$ and the inference rules which define the decoding
function $\widehat{\mathrm{T}}_{f}$ recursively. Congruence rules are defined
as in the case of the Mahlo Universe rules.

We denote the assumption $\Gamma\vdash
f:\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})\to\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})$
by $(\ast)$, and put
$\mathrm{T}_{f}(a):=\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{T}}_{f}(a))$.

$\Gamma\vdash\mathrm{U}_{f}\;\mathrm{type}(\ast)\qquad\Gamma\vdash\widehat{\mathrm{N}}_{f}:\mathrm{U}_{f}(\ast)\qquad\Gamma\vdash\widehat{\mathrm{T}}_{f}(\widehat{\mathrm{N}}_{f})=\widehat{\mathrm{N}}_{\mathbb{M}}:\mathbb{M}(\ast)$
$\Gamma\vdash\widehat{\Pi}_{f}(a,b):\mathrm{U}_{f}\Gamma\vdash
b:\mathrm{T}_{f}(a)\to\mathrm{U}_{f}\Gamma\vdash
a:\mathrm{U}_{f}(\ast)\qquad\Gamma\vdash\widehat{\mathrm{T}}_{f}(\widehat{\Pi}_{f}(a,b))=\widehat{\Pi}_{\mathbb{M}}(\widehat{\mathrm{T}}_{f}(a),\lambda
x.\widehat{\mathrm{T}}_{f}(b\>x)):\mathbb{M}\Gamma\vdash
b:\mathrm{T}_{f}(a)\to\mathrm{U}_{f}\Gamma\vdash a:\mathrm{U}_{f}(\ast)$
$\Gamma\vdash\widehat{\mathrm{Id}}_{f}(a,b,c):\mathrm{U}_{f}\Gamma\vdash
c:\mathrm{T}_{f}(a)\Gamma\vdash b:\mathrm{T}_{f}(a)\Gamma\vdash
a:\mathrm{U}_{f}(\ast)\qquad\Gamma\vdash\widehat{\mathrm{T}}_{f}(\widehat{\mathrm{Id}}_{f}(a,b,c))=\widehat{\mathrm{Id}}_{\mathbb{M}}(\widehat{\mathrm{T}}_{f}(a),b,c):\mathbb{M}\Gamma\vdash
c:\mathrm{T}_{f}(a)\Gamma\vdash b:\mathrm{T}_{f}(a)\Gamma\vdash
a:\mathrm{U}_{f}(\ast)$

Similarly, we define the introduction and decoding function rules for
$\widehat{\mathrm{N}_{n}}_{f},\widehat{\Sigma}_{f},\widehat{+}_{f},\widehat{\mathrm{W}}_{f}$,
but we omit to write down them.

The following rules are the rules for the restriction of $f$ to
$\mathrm{U}_{f}$:

$\Gamma\vdash\mathsf{res}^{0}_{f}(a,b):\mathrm{U}_{f}\Gamma\vdash
b:\mathrm{T}_{f}(a)\to\mathrm{U}_{f}\Gamma\vdash
a:\mathrm{U}_{f}(\ast)\quad\scalebox{0.9}{
$\Gamma\vdash\widehat{\mathrm{T}}_{f}(\mathsf{res}^{0}_{f}(a,b))=\mathsf{p}_{1}(f\>(\widehat{\mathrm{T}}_{f}(a),\lambda
x.\widehat{\mathrm{T}}_{f}(b\>x))):\mathbb{M}\Gamma\vdash
b:\mathrm{T}_{f}(a)\to\mathrm{U}_{f}\Gamma\vdash a:\mathrm{U}_{f}(\ast)$ }$
$\Gamma\vdash\mathsf{res}^{1}_{f}(a,b,c):\mathrm{U}_{f}\Gamma\vdash
c:\mathrm{T}_{f}(\mathsf{res}^{0}_{f}(a,b))\Gamma\vdash
b:\mathrm{T}_{f}(a)\to\mathrm{U}_{f}\Gamma\vdash
a:\mathrm{U}_{f}(\ast)\quad\scalebox{0.9}{
$\Gamma\vdash\widehat{\mathrm{T}}_{f}(\mathsf{res}^{1}_{f}(a,b,c))=\mathsf{p}_{2}(f\>(\widehat{\mathrm{T}}_{f}(a),\lambda
x.\widehat{\mathrm{T}}_{f}(b\>x)))\>c:\mathbb{M}\Gamma\vdash
c:\mathrm{T}_{f}(\mathsf{res}^{0}_{f}(a,b))\Gamma\vdash
b:\mathrm{T}_{f}(a)\to\mathrm{U}_{f}\Gamma\vdash a:\mathrm{U}_{f}(\ast)$ }$

Note that, in the definition above, we defined subuniverses of the Mahlo
Universe $\mathbb{M}$ as recursive subuniverses in the sense of [23, 22]: the
decoding function $\widehat{\mathrm{T}}_{f}$ for the subuniverse
$\mathrm{U}_{f}$ was defined recursively.

As we have seen in Section 1, the Mahlo universe $\mathbb{M}$ reflects
functions on families of small types in $\mathbb{M}$. The system
$\mathbf{MLM}$ expresses this feature as follows. First of all, the
$\mathbb{M}\mathsf{in}_{\mathrm{U}}$ rule above states that there is a
subuniverse $\mathrm{U}_{f}$ of $\mathbb{M}$ closed under
$f:\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})\to\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})$
with its code $\widehat{\mathrm{U}}_{f}:\mathbb{M}$. The closure under $f$ is
then expressed by $\mathsf{res}^{0}_{f}$ and $\mathsf{res}^{1}_{f}$, which
provide the restriction of $f$ to $\mathrm{U}_{f}$: we have
$\mathsf{res}^{0}_{f}(a,b):\mathrm{U}_{f}$ and
$\mathsf{res}^{1}_{f}(a,b,c):\mathrm{U}_{f}$ for any $a:\mathrm{U}_{f}$,
$b:\mathrm{T}_{f}(a)\to\mathrm{U}_{f}$ and
$c:\mathrm{T}_{f}(\mathsf{res}^{0}_{f}(a,b))$. The following computation rules
given by the corresponding inference rules of $\mathbf{MLM}$ show that
$\mathsf{res}^{0}_{f}$ and $\mathsf{res}^{1}_{f}$ actually provide the
restriction of $f$ to $\mathrm{U}_{f}$ via the “injection”
$\widehat{\mathrm{T}}_{f}$ from $\mathrm{U}_{f}$ to $\mathbb{M}$.

$\displaystyle\widehat{\mathrm{T}}_{f}(\mathsf{res}^{0}_{f}(a,b))$
$\displaystyle=\mathsf{p}_{1}(f\>(\widehat{\mathrm{T}}_{f}(a),\lambda
x.\widehat{\mathrm{T}}_{f}(b\>x))):\mathbb{M}$
$\displaystyle\widehat{\mathrm{T}}_{f}(\mathsf{res}^{1}_{f}(a,b,c))$
$\displaystyle=\mathsf{p}_{2}(f\>(\widehat{\mathrm{T}}_{f}(a),\lambda
x.\widehat{\mathrm{T}}_{f}(b\>x)))\>c:\mathbb{M}$

That is, $\widehat{\mathrm{T}}_{f}$ maps $\mathsf{res}^{0}_{f}(a,b)$ to the
left projection of $f\>(\widehat{\mathrm{T}}_{f}(a),\lambda
x.\widehat{\mathrm{T}}_{f}(b\>x))$, and $\mathsf{res}^{1}_{f}(a,b,c)$ to the
right projection of $f\>(\widehat{\mathrm{T}}_{f}(a),\lambda
x.\widehat{\mathrm{T}}_{f}(b\>x))$ applied to $c$.

We work informally in $\mathbf{MLM}$ to improve readability. For any context
$\Gamma$, put $\mathrm{Var}(\Gamma):=\\{x\mid\text{$x:A$ belongs to $\Gamma$
for some type $A$}\\}$. The $\Sigma$-type
$\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M})$ is
abbreviated as $\mathrm{Fam}(\mathbb{M})$. The type constructor $+$ for sum
types is treated as left associative, i.e.,
$A_{1}+A_{2}+\cdots+A_{n}:=(\cdots(A_{1}+A_{2})+\cdots+A_{n})$. Below we write
$\mathrm{Id}(A,a,b)$ as $a=_{A}b$. [Universes above Families of Small Types]
The Mahlo universe $\mathbb{M}$ provides universes above families of small
types as follows. Let $a_{0}:\mathbb{M}$ and
$b_{0}:\mathrm{T}_{\mathbb{M}}(a_{0})\to\mathbb{M}$ be given, and assume that
neither $a_{0}$ nor $b_{0}$ has any free occurrence of a variable $x$.
Defining $f_{0}:\mathrm{Fam}(\mathbb{M})\to\mathrm{Fam}(\mathbb{M})$ as
$f_{0}:=\lambda x.(a_{0},b_{0})$, we have the universe $\mathrm{U}_{f_{0}}$
with the decoding function $\widehat{\mathrm{T}}_{f_{0}}$. The universe
$\mathrm{U}_{f_{0}}$ can be considered as a universe above $(a_{0},b_{0})$, as
the following equations show:

$\displaystyle\widehat{\mathrm{T}}_{f_{0}}(\mathsf{res}^{0}_{f_{0}}(\widehat{\mathrm{N}_{0}}_{f_{0}},\lambda
v.\mathsf{E}_{0}(v)))$
$\displaystyle=\mathsf{p}_{1}\Bigl{(}f_{0}\>(\widehat{\mathrm{T}}_{f_{0}}(\widehat{\mathrm{N}_{0}}_{f_{0}}),\lambda
v.\widehat{\mathrm{T}}_{f_{0}}(\mathsf{E}_{0}(v)))\Bigr{)}=\mathsf{p}_{1}((a_{0},b_{0}))=a_{0}$
$\displaystyle\widehat{\mathrm{T}}_{f_{0}}(\mathsf{res}^{1}_{f_{0}}(\widehat{\mathrm{N}_{0}}_{f_{0}},\lambda
v.\mathsf{E}_{0}(v),c))$
$\displaystyle=\mathsf{p}_{2}\Bigl{(}f_{0}\>(\widehat{\mathrm{T}}_{f_{0}}(\widehat{\mathrm{N}_{0}}_{f_{0}}),\lambda
v.\widehat{\mathrm{T}}_{f_{0}}(\mathsf{E}_{0}(v)))\Bigr{)}\>c=\mathsf{p}_{2}((a_{0},b_{0}))\>c=b_{0}\>c$

That is, $\mathsf{res}^{0}_{f_{0}}(\widehat{\mathrm{N}_{0}}_{f_{0}},\lambda
v.\mathsf{E}_{0}(v))$ is a code for $a_{0}$ in $\mathrm{U}_{f_{0}}$, and
$\mathsf{res}^{1}_{f_{0}}(\widehat{\mathrm{N}_{0}}_{f_{0}},\lambda
v.\mathsf{E}_{0}(v),c)$ is a code for $b_{0}\>c$ in $\mathrm{U}_{f_{0}}$,
where $\widehat{\mathrm{N}_{0}}_{f_{0}}$ and $\lambda v.\mathsf{E}_{0}(v)$ are
dummy arguments.

[Super Universe] A super universe, which is a universe closed under a universe
operator, can be defined by reflecting a function with a parameter. Put
$f_{1}:\mathrm{Fam}(\mathbb{M})\to\mathrm{Fam}(\mathbb{M})$ as $f_{1}:=\lambda
z.y$, where the free variable (or the parameter) $y$ is of type
$\mathrm{Fam}(\mathbb{M})$. We have
$(\widehat{\mathrm{U}}_{f_{1}},\widehat{\mathrm{T}}_{f_{1}}):\mathrm{Fam}(\mathbb{M})$
by reflecting $f_{1}$. Then, we define $g:=\lambda
y.(\widehat{\mathrm{U}}_{f_{1}},\widehat{\mathrm{T}}_{f_{1}})$, and obtain the
universe $\mathrm{U}_{g}$ by reflecting $g$. Note that
$g:\mathrm{Fam}(\mathbb{M})\to\mathrm{Fam}(\mathbb{M})$ is a universe operator
because it takes a family of small types in $\mathbb{M}$ and returns a
universe above this family. The universe $\mathrm{U}_{g}$ is thus a super
universe, because $\mathsf{res}^{0}_{g}$ and $\mathsf{res}^{1}_{g}$ show that
$\mathrm{U}_{g}$ is actually closed under $g$ as the equations below show: for
any $a:\mathrm{U}_{g}$ and $b:\mathrm{T}_{g}(a)\to\mathrm{U}_{g}$,

$\displaystyle\widehat{\mathrm{T}}_{g}(\mathsf{res}^{0}_{g}(a,b))$
$\displaystyle=\mathsf{p}_{1}\Bigl{(}g\>(\widehat{\mathrm{T}}_{g}(a),\lambda
v.\widehat{\mathrm{T}}_{g}(b\>v))\Bigr{)}$
$\displaystyle=\mathsf{p}_{1}(\widehat{\mathrm{U}}_{\lambda
z.(\widehat{\mathrm{T}}_{g}(a),\lambda
v.\widehat{\mathrm{T}}_{g}(b\>v))},\widehat{\mathrm{T}}_{\lambda
z.(\widehat{\mathrm{T}}_{g}(a),\lambda v.\widehat{\mathrm{T}}_{g}(b\>v))})$
$\displaystyle=\widehat{\mathrm{U}}_{\lambda
z.(\widehat{\mathrm{T}}_{g}(a),\lambda v.\widehat{\mathrm{T}}_{g}(b\>v))}$
$\displaystyle\widehat{\mathrm{T}}_{g}(\mathsf{res}^{1}_{g}(a,b,c))$
$\displaystyle=\mathsf{p}_{2}\Bigl{(}g\>(\widehat{\mathrm{T}}_{g}(a),\lambda
v.\widehat{\mathrm{T}}_{g}(b\>v))\Bigr{)}\>c$
$\displaystyle=\mathsf{p}_{2}(\widehat{\mathrm{U}}_{\lambda
z.(\widehat{\mathrm{T}}_{g}(a),\lambda
v.\widehat{\mathrm{T}}_{g}(b\>v))},\widehat{\mathrm{T}}_{\lambda
z.(\widehat{\mathrm{T}}_{g}(a),\lambda v.\widehat{\mathrm{T}}_{g}(b\>v))})\>c$
$\displaystyle=\widehat{\mathrm{T}}_{\lambda
z.(\widehat{\mathrm{T}}_{g}(a),\lambda v.\widehat{\mathrm{T}}_{g}(b\>v))}\>c$

That is, $\mathsf{res}^{0}_{g}(a,b)$ is a code of the universe above the
family $(a,b)$, and $\mathsf{res}^{1}_{g}(a,b)$ is a code of its decoding
function. Notice that $\mathrm{U}_{g}$ also has a code
$\mathsf{res}^{0}_{g}(\mathsf{res}^{0}_{g}(a,b),\mathsf{res}^{1}_{g}(a,b))$ of
the universe above the family
$(\mathsf{res}^{0}_{g}(a,b),\mathsf{res}^{1}_{g}(a,b))$, and so on.

###  2.2. Construction of A Higher-Order Universe Operator

Following [14], we define the type $\mathrm{O}$ of first-order operators and
the type $\mathrm{Fam}(\mathrm{O})$ of families of first-order operators as

$\mathrm{O}:=\mathrm{Fam}(\mathbb{M})\to\mathrm{Fam}(\mathbb{M}),\qquad\qquad\mathrm{Fam}(\mathrm{O}):=\Sigma_{(x:\mathbb{M})}(\mathrm{T}_{\mathbb{M}}(x)\to\mathrm{O}).$

For instance, let $f$ be of type $\mathrm{N}_{3}\to\mathrm{O}$. Then,
$(\widehat{\mathrm{N}_{3}}_{\mathbb{M}},f):\mathrm{Fam}(\mathrm{O})$ is a
family of first-order operators which consists of the operators
$f\;0_{3},f\;1_{3},f\;2_{3}:\mathrm{O}$.

We define the higher-order operator
$\mathrm{u}^{\mathbb{M}}:\mathrm{Fam}(\mathrm{O})\to\mathrm{O}$ by using the
reflection property of $\mathbb{M}$. Typically, this operator takes a family
of universe operators as an input, and returns a universe operator which
provides a universe closed under all of the operators in this family. So an
output of $\mathrm{u}^{\mathbb{M}}$ can be its input again, and this process
will be iterated transfinitely to construct the type-theoretic counterparts of
inaccessible sets. [Operator $\mathrm{u}^{\mathbb{M}}$] The higher-order
operator $\mathrm{u}^{\mathbb{M}}:\mathrm{Fam}(\mathrm{O})\to\mathrm{O}$ is
defined as follows. Let $(z,v):\mathrm{Fam}(\mathrm{O})$ and
$(x,y):\mathrm{Fam}(\mathbb{M})$ be given. Then, by using $+\mathsf{el}$
repeatedly, one can define

$h^{\mathbb{M}}:\Pi_{(w:\mathrm{Fam}(\mathbb{M}))}\Bigl{(}\mathrm{N}_{1}+\mathrm{T}_{\mathbb{M}}(x)+\mathrm{T}_{\mathbb{M}}(z)+\Sigma_{(w^{\prime}:\mathrm{T}_{\mathbb{M}}(z))}\mathrm{T}_{\mathbb{M}}(\mathsf{p}_{1}(v\>w^{\prime}\>w))\to\mathbb{M}\Bigr{)}$

such that

  * •

$h^{\mathbb{M}}\>w\>(\mathsf{i}\mathsf{i}\mathsf{i}\>x_{1})=x$ with
$x_{1}:\mathrm{N}_{1}$,

  * •

$h^{\mathbb{M}}\>w\>(\mathsf{i}\mathsf{i}\mathsf{j}\>x_{2})=y\>x_{2}$ with
$x_{2}:\mathrm{T}_{\mathbb{M}}(x)$,

  * •

$h^{\mathbb{M}}\>w\>(\mathsf{i}\mathsf{j}\>y_{1})=\mathsf{p}_{1}(v\>y_{1}\>w)$
with $y_{1}:\mathrm{T}_{\mathbb{M}}(z)$,

  * •

$h^{\mathbb{M}}\>w\>(\mathsf{j}(y_{1},z_{1}))=\mathsf{p}_{2}(v\>y_{1}\>w)\>z_{1}$
with $y_{1}:\mathrm{T}_{\mathbb{M}}(z)$ and
$z_{1}:\mathrm{T}_{\mathbb{M}}(\mathsf{p}_{1}(v\>y_{1}\>w))$.

Next, put $f^{\mathbb{M}}[z,v,x,y]:\mathrm{O}$ as

$f^{\mathbb{M}}[z,v,x,y]:=\lambda
w.(\widehat{\mathrm{N}_{1}}_{\mathbb{M}}\>\widehat{+}_{\mathbb{M}}\>x\>\widehat{+}_{\mathbb{M}}\>z\>\widehat{+}_{\mathbb{M}}\>\widehat{\Sigma}_{\mathbb{M}}(z,\lambda
w^{\prime}.\mathsf{p}_{1}(v\>w^{\prime}\>w)),\>h^{\mathbb{M}}\>w).$

Then, we define
$\mathrm{u}^{\mathbb{M}}\>(z,v)\>(x,y):=(\widehat{\mathrm{U}}_{f^{\mathbb{M}}[z,v,x,y]},\widehat{\mathrm{T}}_{f^{\mathbb{M}}[z,v,x,y]})$.
By applying $\Sigma\mathsf{el}$ twice, we have
$\mathrm{u}^{\mathbb{M}}:\mathrm{Fam}(\mathrm{O})\to\mathrm{O}$.

Roughly speaking, $h^{\mathbb{M}}\;w$ in the definition above is a family of
small types in $\mathbb{M}$ whose index set is

$\mathrm{N}_{1}+\mathrm{T}_{\mathbb{M}}(x)+\mathrm{T}_{\mathbb{M}}(z)+\Sigma_{(w^{\prime}:\mathrm{T}_{\mathbb{M}}(z))}\mathrm{T}_{\mathbb{M}}(\mathsf{p}_{1}(v\>w^{\prime}\>w)).$

That is,

  * •

$h^{\mathbb{M}}\>w\>(\mathsf{i}\mathsf{i}\mathsf{i}\>x_{1})$ is the small type
$x:\mathbb{M}$, where $x_{1}$ is of type $\mathrm{N}_{1}$,

  * •

$h^{\mathbb{M}}\>w\>(\mathsf{i}\mathsf{i}\mathsf{j}\>x_{2})$ is the small type
$y\>x_{2}:\mathbb{M}$ given by the family
$y:\mathrm{T}_{\mathbb{M}}(x)\to\mathbb{M}$ of small types and the index
$x_{2}:\mathrm{T}_{\mathbb{M}}(x)$,

  * •

$h^{\mathbb{M}}\>w\>(\mathsf{i}\mathsf{j}\>y_{1})$ is the small type
$\mathsf{p}_{1}(v\>y_{1}\>w):\mathbb{M}$ given by the family
$v:\mathrm{T}_{\mathbb{M}}(z)\to\mathrm{O}$ of first-order operators, the
index $y_{1}:\mathrm{T}_{\mathbb{M}}(z)$ and $w:\mathrm{Fam}(\mathbb{M})$,

  * •

$h^{\mathbb{M}}\>w\>(\mathsf{j}(y_{1},z_{1}))$ is the small type
$\mathsf{p}_{2}(v\>y_{1}\>w)\>z_{1}:\mathbb{M}$ given by the family
$v:\mathrm{T}_{\mathbb{M}}(z)\to\mathrm{O}$ of first-order operators, the
index $y_{1}:\mathrm{T}_{\mathbb{M}}(z)$, $w:\mathrm{Fam}(\mathbb{M})$ and
$z_{1}:\mathrm{T}_{\mathbb{M}}(\mathsf{p}_{1}(v\>y_{1}\>w))$.

In particular, the two small types
$h^{\mathbb{M}}\>w\>(\mathsf{i}\mathsf{j}\>y_{1})$ and
$h^{\mathbb{M}}\>w\>(\mathsf{j}(y_{1},z_{1}))$ are the outputs of the first-
order operator $v\>y_{1}$ from the family
$v:\mathrm{T}_{\mathbb{M}}(z)\to\mathrm{O}$.

For comparison, we show that a super universe can be defined by using the
operator $\mathrm{u}^{\mathbb{M}}$. [Super Universe and Universes above
Families of Small Types] Take $g$ as defined in Example 1, and let
$(a,b):\mathrm{Fam}(\mathbb{M})$ be the case. Using the operator
$\mathrm{u}^{\mathbb{M}}$, we have the subuniverse of $\mathbb{M}$ and its
decoding function

$\mathrm{u}^{\mathbb{M}}\>(\widehat{\mathrm{N}_{1}}_{\mathbb{M}},\lambda
x.\mathsf{E}_{1}(x,g))\>(a,b)=(\widehat{\mathrm{U}}_{g^{\ast}},\widehat{\mathrm{T}}_{g^{\ast}}),$

where we abbreviate
$f^{\mathbb{M}}[\widehat{\mathrm{N}_{1}}_{\mathbb{M}},\lambda
x.\mathsf{E}_{1}(x,g),a,b]$ as $g^{*}$. This subuniverse has the codes for $a$
and $b\>c$ with $c:\mathrm{T}_{\mathbb{M}}(a)$, as shown below.

$\displaystyle\widehat{\mathrm{T}}_{g^{*}}(\mathsf{res}^{1}_{g^{*}}(\widehat{\mathrm{N}_{0}}_{g^{*}},\lambda
x.\mathsf{E}_{0}(x),\mathsf{i}\mathsf{i}\mathsf{i}\>0_{1}))$
$\displaystyle=h^{\mathbb{M}}\>(\widehat{\mathrm{N}_{0}}_{\mathbb{M}},\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(\mathsf{E}_{0}(x)))\>(\mathsf{i}\mathsf{i}\mathsf{i}\>0_{1})=a$
$\displaystyle\widehat{\mathrm{T}}_{g^{*}}(\mathsf{res}^{1}_{g^{*}}(\widehat{\mathrm{N}_{0}}_{g^{*}},\lambda
x.\mathsf{E}_{0}(x),\mathsf{i}\mathsf{i}\mathsf{j}\>c))$
$\displaystyle=h^{\mathbb{M}}\>(\widehat{\mathrm{N}_{0}}_{\mathbb{M}},\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(\mathsf{E}_{0}(x)))\>(\mathsf{i}\mathsf{i}\mathsf{j}\>c)=b\>c$

Moreover, the subuniverse
$\mathrm{u}^{\mathbb{M}}\>(\widehat{\mathrm{N}_{1}}_{\mathbb{M}},\lambda
x.\mathsf{E}_{1}(x,g))\>(a,b)$ is closed under the universe operator $g$. Let
$a^{\prime}:\mathrm{U}_{g^{*}}$ and
$b^{\prime}:\mathrm{T}_{g^{*}}(a^{\prime})\to\mathrm{U}_{g^{*}}$ be given. We
then have

$\displaystyle\widehat{\mathrm{T}}_{g^{*}}(\mathsf{res}^{1}_{g^{*}}(a^{\prime},b^{\prime},\mathsf{i}\mathsf{j}\>0_{1}))$
$\displaystyle=h^{\mathbb{M}}\>(\widehat{\mathrm{T}}_{g^{*}}(a^{\prime}),\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x))\>(\mathsf{i}\mathsf{j}\>0_{1})$
$\displaystyle=\mathsf{p}_{1}\Bigl{(}(\lambda
y.\mathsf{E}_{1}(y,g))\>0_{1}\>(\widehat{\mathrm{T}}_{g^{*}}(a^{\prime}),\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x))\Bigr{)}$
$\displaystyle=\mathsf{p}_{1}\Bigl{(}g\>(\widehat{\mathrm{T}}_{g^{*}}(a^{\prime}),\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x))\Bigr{)}=\widehat{\mathrm{U}}_{\lambda
z.(\widehat{\mathrm{T}}_{g^{*}}(a^{\prime}),\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x))}$
$\displaystyle\widehat{\mathrm{T}}_{g^{*}}(\mathsf{res}^{1}_{g^{*}}(a^{\prime},b^{\prime},\mathsf{j}(0_{1},c)))$
$\displaystyle=h^{\mathbb{M}}\>(\widehat{\mathrm{T}}_{g^{*}}(a^{\prime}),\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x))\>(\mathsf{j}(0_{1},c))$
$\displaystyle=\mathsf{p}_{2}\Bigl{(}(\lambda
y.\mathsf{E}_{1}(y,g))\>0_{1}\>(\widehat{\mathrm{T}}_{g^{*}}(a^{\prime}),\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x))\Bigr{)}\>c$
$\displaystyle=\mathsf{p}_{2}\Bigl{(}g\>(\widehat{\mathrm{T}}_{g^{*}}(a^{\prime}),\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x))\Bigr{)}\>c=\widehat{\mathrm{T}}_{\lambda
z.(\widehat{\mathrm{T}}_{g^{*}}(a^{\prime}),\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x))}(c)$

Thus,
$\mathsf{res}^{1}_{g^{*}}(a^{\prime},b^{\prime},\mathsf{i}\mathsf{j}\>0_{1})$
and $\lambda
w^{\prime}.\mathsf{res}^{1}_{g^{*}}(a^{\prime},b^{\prime},\mathsf{j}(0_{1},w^{\prime}))$
provide the codes in $\mathrm{U}_{g^{*}}$ for the universe obtained by
applying the universe operator $g$ to
$\widehat{\mathrm{T}}_{g^{*}}(a^{\prime})$ and $\lambda
x.\widehat{\mathrm{T}}_{g^{*}}(b^{\prime}\>x)$. This construction can be
iterated as

$\mathsf{res}^{1}_{g^{*}}(\mathsf{res}^{1}_{g^{*}}(a^{\prime},b^{\prime},\mathsf{i}\mathsf{j}\>0_{1}),\lambda
w^{\prime}.\mathsf{res}^{1}_{g^{*}}(a^{\prime},b^{\prime},\mathsf{j}(0_{1},w^{\prime})),\mathsf{i}\mathsf{j}\>0_{1}),$

and so on.

Note that $g^{*}$ is a first-order super-universe operator. So one can
construct a universe closed under this super-universe operator by replacing
$g$ with $g^{*}$ in the argument above, and this process can be iterated.

##  3\. Inaccessible Sets in the Mahlo Universe of $\mathbf{MLM}$

Below we first recall Aczel’s constructive set theory $\mathbf{CZF}$ and then
present Rathjen-Griffor-Palmgren’s extension of $\mathbf{CZF}_{\pi}$ by
inaccessible sets of all transfinite orders (Section 3.1). Next, we prove our
main theorem that inaccessible sets of $\mathbf{CZF}_{\pi}$ are directly
interpretable in $\mathbf{MLM}$ with the accessibility predicate
$\mathrm{Acc}$ (Section 3.2).

###  3.1. $\mathbf{CZF}$ with Inaccessible Sets of All Transfinite Orders

The language of $\mathbf{CZF}$ is a usual first-order language with the
equality $=$ and the membership relation $\in$ except that the restricted
quantifiers $\forall x\in y$ and $\exists x\in y$ are primitive symbols. The
symbol $\in$ is the only non-logical symbol in this language. The underlying
logic of $\mathbf{CZF}$ is intuitionistic logic with equality, and the
following set-theoretic axioms are postulated (cf. [4]).

Pairing:

$\forall a\forall b\exists c\forall x(x\in c\leftrightarrow x=a\lor x=b)$

Union:

$\forall a\exists b\forall x(x\in b\leftrightarrow\exists y\in a(x\in y))$

Infinity:

$\exists a(\exists x(x\in a)\land\forall x\in a\exists y\in a(x\in y))$

Extensionality:

$\forall a\forall b(\forall x(x\in a\leftrightarrow x\in b)\to a=b)$

Set Induction:

For any formula $\varphi[x]$,

$\forall a(\forall x\in a\varphi[x]\to\varphi[a])\to\forall a\varphi[a].$

Restricted Separation:

For any restricted formula $\varphi[x]$,

$\forall a\exists b\forall x(x\in b\leftrightarrow x\in a\land\varphi[x]),$

where a formula is restricted if all of its quantifiers are restricted.

Subset Collection:

For any formula $\psi[x,y,u]$,

$\displaystyle\forall a\forall b\exists c\forall u$ $\displaystyle(\forall
x\in a\exists y\in b\psi[x,y,u]\to\exists z\in c(\forall x\in a\exists y\in
z\psi[x,y,u]\land\forall y\in z\exists x\in a\psi[x,y,u])).$

Strong Collection:

For any formula $\psi[x,y]$,

$\forall a(\forall x\in a\exists y\psi[x,y]\to\exists b(\forall x\in a\exists
y\in b\psi[x,y]\land\forall y\in b\exists x\in a\psi[x,y])).$

Informally, one may suppose that the range of bound variables in
$\mathbf{CZF}$ forms a collection of objects. We call these objects Aczel’s
iterative sets or sets shortly.

To state the axiom that there are inaccessible sets of all transfinite orders,
we need to define the notion of regular set. For any set $a$, $a$ is
transitive if $\forall x\in a\forall y\in x(y\in a)$ holds. [Regular Sets] A
set $a$ is regular if the following conditions are satisfied:

  1. (1)

$a$ is inhabited, i.e., $\exists y(y\in a)$,

  2. (2)

$a$ is transitive,

  3. (3)

$\forall b\in a\forall R(R\subseteq b\times a\land\forall x\in b\exists
y(\langle x,y\rangle\in R)\to$

$\exists c\in a(\forall x\in b\exists y\in c(\langle x,y\rangle\in
R)\land\forall y\in c\exists x\in b(\langle x,y\rangle\in R))$.

The notion of inaccessible set is captured by set-inaccessibility. A set $a$
is set-inaccessible if the following conditions are satisfied:

  1. (1)

$a$ is regular,

  2. (2)

$\forall x\in a\exists y\in a(x\subseteq y\land y\text{ is regular})$,

  3. (3)

$a$ is a model of $\mathbf{CZF}$, i.e., the structure $\langle
a,\in\upharpoonright(a\times a)\rangle$ is a model of $\mathbf{CZF}$.

As in classical Zermelo-Fraenkel set theory, one can talk about classes in
$\mathbf{CZF}$. A class $A$ is said to be unbounded in a class $B$ if $\forall
x\in B\exists y\in A(x\in y\land y\in B)$ holds. Let $\mathsf{TC}(a)$ be the
transitive closure of a set $a$ with the following property (see [4,
Proposition 4.2]):

$\mathsf{TC}(a)=a\cup\bigcup\\{\mathsf{TC}(x)\mid x\in a\\}.$

Inaccessible sets of transfinite orders are defined along the hierarchy of
Aczel’s iterative sets. Let $a$ and $b$ be sets, then $b$ is $a$-set-
inaccessible if $b$ is set-inaccessible and there is a family
$(x_{c})_{c\in\mathsf{TC}(a)}$ of sets such that for any $c\in\mathsf{TC}(a)$,

  * •

$x_{c}$ is unbounded in $b$,

  * •

$x_{c}$ consists of sets which are set-inaccessible,

  * •

for any $y\in x_{c}$ and any $d\in\mathsf{TC}(c)$, $x_{d}$ is unbounded in
$y$.

Note that $x_{d}$ in the third condition is well-defined because for any sets
$a,c$ and $y$, if $c\in\mathsf{TC}(a)$ and $y\in\mathsf{TC}(c)$ hold then
$y\in\mathsf{TC}(a)$ holds. Informally speaking, a set $a$ represents a
transfinite “order” in the hierarchy of iterative sets, so $a$-set-
inaccessibles can be considered as inaccessible sets of order $a$. The first
lemma below immediately follows from the definition of $a$-set-
inaccessibility, and the second lemma follows from the first (see [17, Lemma
2.11]).

######  Lemma 1 ($\mathbf{CZF}$).

For any sets $a,b$ and $c$, if $a$ is $b$-set-inaccessible and
$c\in\mathsf{TC}(b)$ holds, then $a$ is $c$-set-inaccessible.

######  Lemma 2 ($\mathbf{CZF}$).

Let $a$ be set-inaccessible. Then, $a$ is $b$-set-inaccessible if and only if
for all $c\in b$, the class of $c$-set-inaccessibles is unbounded in $a$.

The system $\mathbf{CZF}_{\pi}$ is obtained by adding the following axiom to
$\mathbf{CZF}$.

Pi-Numbers:

$\forall x\forall a\exists b(x\in b\land b\text{ is $a$-set-inaccessible}).$

That is, $\mathbf{CZF}_{\pi}$ is the extension of $\mathbf{CZF}$ by the axiom
that for any sets $x$ and $a$, where $a$ represents a transfinite “order” in
the hierarchy of iterative sets, there is a set $b$ which has $x$ as its
element and is $a$-set-inaccessible.

###  3.2. Construction of Inaccessible Sets in Mahlo Universe

To show that $\mathbf{CZF}_{\pi}$ is interpretable in $\mathbf{MLM}$ with the
accessibility predicate $\mathrm{Acc}$, we recall Aczel’s interpretation of
$\mathbf{CZF}$ in $\mathbf{MLTT}$.

First of all, we define the type-theoretic counterpart of Aczel’s iterative
sets. Let a $\mathrm{W}$-type $\mathrm{W}_{(x:A)}B$ be given. It is
straightforward to define the functions $\mathsf{index}:\mathrm{W}_{(x:A)}B\to
A$ and
$\mathsf{pred}:\Pi_{(y:\mathrm{W}_{(x:A)}B)}B[\mathsf{index}\;y/x]\to\mathrm{W}_{(x:A)}B$
satisfying

$\mathsf{index}\;\mathsf{sup}(a,b)=a,\qquad\mathsf{pred}\;\mathsf{sup}(a,b)=b.$

The $\mathrm{W}$-type $\mathbb{V}$, which is the type of iterative sets in
Aczel’s interpretation of $\mathbf{CZF}$, is defined as

$\mathbb{V}:=\mathrm{W}_{(x:\mathbb{M})}\mathrm{T}_{\mathbb{M}}(x).$

We call terms of type $\mathbb{V}$ in some contexts sets, and denote them by
lowercase Greek letters such as $\alpha,\beta,\gamma$ possibly with suffixes.
For any $\alpha:\mathbb{V}$, we write
$\mathrm{T}_{\mathbb{M}}(\mathsf{index}\;\alpha)$ as $\overline{\alpha}$,
following [17]. Moreover, we adopt the abbreviations below: for any term $F$
such that $\Gamma,\beta:\mathbb{V}\vdash F\;\mathrm{type}$ holds for some
context $\Gamma$,

$\forall\beta\in\alpha
F:=\Pi_{(x:\overline{\alpha})}F[\mathsf{pred}\>\alpha\>x/\beta],\qquad\exists\beta\in\alpha
F:=\Sigma_{(x:\overline{\alpha})}F[\mathsf{pred}\>\alpha\>x/\beta].$

Note that the elimination rule for
$\mathbb{V}=\mathrm{W}_{(x:\mathbb{M})}\mathrm{T}_{\mathbb{M}}(x)$ provides
the transfinite induction principle on $\alpha:\mathbb{V}$. That is, we have a
term

$\mathrm{TI}_{F}:\Pi_{(\alpha:\mathbb{V})}(\forall\gamma\in\alpha
F[\gamma/\beta]\to
F[\alpha/\beta])\to\Pi_{(\alpha:\mathbb{V})}F[\alpha/\beta],$

where $\Gamma,\beta:\mathbb{V}\vdash F\;\mathrm{type}$ holds for some context
$\Gamma$.

Next, we define the interpretation of the equality $a=b$ and the membership
relation $a\in b$ in $\mathbf{CZF}$ as an equivalence relation $\doteq$ and a
binary relation $\in$ on $\mathbb{V}$, respectively. The relation $\doteq$ on
$\mathbb{V}$ is defined by applying the elimination rule for
$\mathrm{W}$-types twice:

$\mathsf{sup}(a,f)\doteq\mathsf{sup}(b,g):=(\Pi_{(x:\mathrm{T}_{\mathbb{M}}(a))}\Sigma_{(y:\mathrm{T}_{\mathbb{M}}(b))}f\;x\doteq
g\;y)\times(\Pi_{(y:\mathrm{T}_{\mathbb{M}}(b))}\Sigma_{(x:\mathrm{T}_{\mathbb{M}}(a))}f\;x\doteq
g\;y).$

For any $\alpha,\beta:\mathbb{V}$, we define $\alpha\in\beta$ as
$\alpha\in\beta:=\exists\gamma\in\beta(\alpha\doteq\gamma)$.

We interpret all formulas of $\mathbf{CZF}$ in $\mathbf{MLTT}$ by using these
relations $\doteq$ and $\in$ on $\mathbb{V}$. The formulas $x=y$ and $x\in y$
in the language of $\mathbf{CZF}$ are interpreted as the relations $x\doteq y$
and $x\in y$ on $\mathbb{V}$, respectively. Compound formulas of
$\mathbf{CZF}$ are interpreted as follows:

$\displaystyle(\varphi\land\psi)^{\ast}$
$\displaystyle:=\varphi^{\ast}\times\psi^{\ast}$
$\displaystyle(\varphi\lor\psi)^{\ast}$
$\displaystyle:=\varphi^{\ast}+\psi^{\ast}$
$\displaystyle(\varphi\to\psi)^{\ast}$
$\displaystyle:=\varphi^{\ast}\to\psi^{\ast}$ $\displaystyle\bot^{\ast}$
$\displaystyle:=\mathrm{N}_{0}$ $\displaystyle(\forall x\in y\varphi)^{\ast}$
$\displaystyle:=\forall x\in y\varphi^{\ast}$ $\displaystyle(\exists x\in
y\varphi)^{\ast}$ $\displaystyle:=\exists x\in y\varphi^{\ast}$
$\displaystyle(\forall x\varphi)^{\ast}$
$\displaystyle:=\Pi_{(\alpha:\mathbb{V})}\varphi^{\ast}$
$\displaystyle(\exists x\varphi)^{\ast}$
$\displaystyle:=\Sigma_{(\alpha:\mathbb{V})}\varphi^{\ast}$

It is then straightforward to show by induction on the length of a given
$\mathbf{CZF}$-formula $\varphi$ that if a list $x_{1},\ldots,x_{n}$ of
variables contains all free variables in $\varphi$ then the judgement
$x_{1}:\mathbb{V},\ldots,x_{n}:\mathbb{V}\vdash\varphi^{\ast}\;\mathrm{type}$
is derivable in $\mathbf{MLTT}$. Moreover, as suggested in [2, Remarks 3.5],
the following useful lemma is provable by induction on the length of a given
$\mathbf{CZF}$-formula.

######  Lemma 3.

Let $\varphi[x_{1},\ldots,x_{n},x]$ be an arbitrary formula of $\mathbf{CZF}$
such that $x_{1},\ldots,x_{n}$ and $x$ contain all free variable occurring in
$\varphi$. Then, the statement

$\Pi_{(x_{1}:\mathbb{V})}\cdots\Pi_{(x_{n}:\mathbb{V})}\Pi_{(y:\mathbb{V})}\Pi_{(z:\mathbb{V})}(y\doteq
z\to\varphi^{\ast}[x_{1},\ldots,x_{n},y]\to\varphi^{\ast}[x_{1},\ldots,x_{n},z])$

is derivable in $\mathbf{MLTT}$.

In $\mathbf{MLTT}$, one is able to define the corresponding operators to the
set-theoretic axioms of $\mathbf{CZF}$ (see [1, 2]). For instance, the union
operator and the binary union operator for elements of $\mathbb{V}$ can be
defined: let $A\leftrightarrow B$ be an abbreviation of $(A\to B)\times(B\to
A)$, then the type-theoretic axiom of choice in $\mathbf{MLTT}$ provides the
two terms $\bigcup:\mathbb{V}\to\mathbb{V}$ and
$\cup:\mathbb{V}\to\mathbb{V}\to\mathbb{V}$ satisfying

$\displaystyle\Pi_{(\alpha:\mathbb{V})}\Pi_{(\gamma:\mathbb{V})}(\gamma\in\bigcup\alpha\leftrightarrow\exists\delta\in\alpha(\gamma\in\delta)),$
$\displaystyle\Pi_{(\alpha_{1}:\mathbb{V})}\Pi_{(\alpha_{2}:\mathbb{V})}\Pi_{(\gamma:\mathbb{V})}(\gamma\in\alpha_{1}\cup\alpha_{2}\leftrightarrow(\gamma\in\alpha_{1})+(\gamma\in\alpha_{2})).$

The term $\bigcup$ enables to interpret the axiom Union in $\mathbf{MLTT}$,
that is, one can show that the interpretation of the axiom Union is derivable
in $\mathbf{MLTT}$. In a similar manner, one can verify that all axioms of
$\mathbf{CZF}$ are interpretable in $\mathbf{MLTT}$ (see [1, 2] for details).

For our purpose, the axiom Pi-Numbers remains to be interpreted in
$\mathbf{MLM}$. Below we first define the transitive closure function
$\mathsf{tc}$ on $\mathbb{V}$ to provide an interpretation of the set-
theoretic transitive closure. Next, we define the accessibility predicate
$\mathrm{Acc}$ on $\mathbb{V}$ and construct the type-theoretic counterparts
$\mathbf{V}^{\alpha,t}_{(a,f)}$ of inaccessible sets by iterating the higher-
order universe operator $\mathrm{u}^{\mathbb{M}}$ along the accessibility
given by $\mathrm{Acc}$. Finally, it is shown that inaccessible sets of all
transfinite orders in $\mathbf{CZF}$ are indeed interpreted by these
counterparts.

Following [17], we define the transitive closure function on $\mathbb{V}$ as
follows. [Transitive Closure] The transitive closure function
$\mathsf{tc}:\mathbb{V}\to\mathbb{V}$ is defined as

$\mathsf{tc}(\mathsf{sup}(a,f)):=\mathsf{sup}(a,f)\cup(\bigcup\mathsf{sup}(a,\lambda
x.\mathsf{tc}(f\;x))).$

We put $\alpha_{\mathsf{tc}}:=\mathsf{tc}(\alpha)$ as in [17]. Note that, by
definition, $\overline{\mathsf{sup}(a,f)_{\mathsf{tc}}}$ is definitionally
equal to
$\mathrm{T}_{\mathbb{M}}(a)+\Sigma_{(z:\mathrm{T}_{\mathbb{M}}(a))}\overline{(f\;z)_{\mathsf{tc}}}$.
In addition, we define the accessibility predicate on $\mathbb{V}$ as an
inductive predicate. This principle is used to iterate the higher-order
operator $\mathrm{u}^{\mathbb{M}}$ along a given $\alpha:\mathbb{V}$ (cf.
Definition 3). [Accessibility Predicate] The predicate $\mathrm{Acc}$ on
$\mathbb{V}$ is defined inductively: the formation, introduction, elimination
and computation rules are as follows.

$\Gamma\vdash\mathrm{Acc}\>\alpha\;\mathrm{type}\Gamma\vdash\alpha:\mathbb{V}\qquad\Gamma\vdash\mathsf{prog}\>f:\mathrm{Acc}\>\alpha\Gamma\vdash
f:\Pi_{(x:\overline{\alpha_{\mathsf{tc}}})}\mathrm{Acc}\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>x)\Gamma\vdash\alpha:\mathbb{V}$
$\Gamma\vdash\mathsf{E}_{\mathrm{Acc}}(\alpha,t,g):C[\alpha/\beta,t/x]\Gamma\vdash
g:\Pi_{(\gamma:\mathbb{V})}\Pi_{(f:\Pi_{(y:\overline{\gamma_{\mathsf{tc}}})}\mathrm{Acc}\>(\mathsf{pred}\>\gamma_{\mathsf{tc}}\>y))}(\Pi_{(y:\overline{\gamma_{\mathsf{tc}}})}C[\mathsf{pred}\>\gamma_{\mathsf{tc}}\>y/\beta,f\>y/x]\to
C[\gamma/\beta,\mathsf{prog}\>f/x])\Gamma,\beta:\mathbb{V},x:\mathrm{Acc}\>\beta\vdash
C\;\mathrm{type}\Gamma\vdash
t:\mathrm{Acc}\>\alpha\Gamma\vdash\alpha:\mathbb{V}$
$\Gamma\vdash\mathsf{E}_{\mathrm{Acc}}(\alpha,\mathsf{prog}\>f,g)=g\>\alpha\>f\>(\lambda
y.\mathsf{E}_{\mathrm{Acc}}(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y,f\>y,g)):C[\alpha/\beta,\mathsf{prog}\>f/x]\Gamma\vdash
g:\Pi_{(\gamma:\mathbb{V})}\Pi_{(f:\Pi_{(y:\overline{\gamma_{\mathsf{tc}}})}\mathrm{Acc}\>(\mathsf{pred}\>\gamma_{\mathsf{tc}}\>y))}(\Pi_{(y:\overline{\gamma_{\mathsf{tc}}})}C[\mathsf{pred}\>\gamma_{\mathsf{tc}}\>y/\beta,f\>y/x]\to
C[\gamma/\beta,\mathsf{prog}\>f/x])\Gamma,\beta:\mathbb{V},x:\mathrm{Acc}\>\beta\vdash
C\;\mathrm{type}\Gamma\vdash
f:\Pi_{(y:\overline{\alpha_{\mathsf{tc}}})}\mathrm{Acc}\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\Gamma\vdash\alpha:\mathbb{V}$

Informally speaking, the family
$\bigcup_{x:\overline{\alpha_{\mathsf{tc}}}}\mathsf{pred}\>\alpha_{\mathsf{tc}}\>x$
of sets exhausts all sets which are needed to construct the set $\alpha$, and
the introduction rule of $\mathrm{Acc}$ means that $\alpha$ is accessible if
any of such sets is accessible. The elimination rule of $\mathrm{Acc}$ enables
to provide an inductive argument for $C[\gamma/\beta,\mathsf{prog}\>f/x]$ with
the induction hypothesis that
$C[\mathsf{pred}\>\gamma_{\mathsf{tc}}\>y/\beta,f\>y/x]$ holds for any
$y:\overline{\gamma_{\mathsf{tc}}}$.

The induction principle on $\mathrm{Acc}$ provides the iterator of the
operator $\mathrm{u}^{\mathbb{M}}$ below. [Iterator of
$\mathrm{u}^{\mathbb{M}}$ along Accessibility] We define
$\Phi:\Pi_{(\alpha:\mathbb{V})}(\mathrm{Acc}\>\alpha\to\mathrm{O})$ by
induction on $t:\mathrm{Acc}\>\alpha$:

$\Phi\>\alpha\>(\mathsf{prog}\>f)\>(c,h):=\mathrm{u}^{\mathbb{M}}(\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
x.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>x)\>(f\>x))\>(c,h).$

We abbreviate $\Phi\>\alpha\>t\>(c,h)$ as $\Phi^{\alpha,t}_{(c,h)}$. Here the
iterator $\Phi$ takes a set $\alpha$ and a proof $\mathsf{prog}\>f$ of its
accessibility with a family $(c,h):\mathrm{Fam}(\mathbb{M})$ and returns the
subuniverse $\mathrm{U}$ of $\mathbb{M}$ such that

  * •

$\mathrm{U}$ is closed under the universe operator
$\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>x)\>(f\>x)$ for any
$x:\overline{\alpha_{\mathsf{tc}}}$, which is obtained by the induction
hypothesis, and

  * •

$\mathrm{U}$ includes the codes of $c$ and $h$.

The hierarchy of such subuniverses is defined by applying the left and right
projection to the output of the iterator $\Phi$. [Transfinite Hierarchy of
Subuniverses] Let $\alpha:\mathbb{V}$, $t:\mathrm{Acc}\>\alpha$ and
$(a,f):\mathrm{Fam}(\mathbb{M})$ be given. We define the transfinite hierarchy
of subuniverses with their decoding functions
$\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}$ along $\mathrm{Acc}$.

$\displaystyle\widehat{\mathcal{U}}^{\alpha,t}_{(a,f)}$
$\displaystyle:=\mathsf{p}_{1}(\Phi^{\alpha,t}_{(a,f)}):\mathbb{M}$
$\displaystyle\mathcal{U}^{\alpha,t}_{(a,f)}$
$\displaystyle:=\mathrm{T}_{\mathbb{M}}(\widehat{\mathcal{U}}^{\alpha,t}_{(a,f)})$
$\displaystyle\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}$
$\displaystyle:=\mathsf{p}_{2}(\Phi^{\alpha,t}_{(a,f)}):\mathcal{U}^{\alpha,t}_{(a,f)}\to\mathbb{M}$
$\displaystyle\mathrm{T}^{\alpha,t}_{(a,f)}$ $\displaystyle:=\lambda
x.\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(x))$

Each of subuniverses $\mathcal{U}^{\alpha,t}_{(a,f)}$ provides the type
$\mathcal{V}^{\alpha,t}_{(a,f)}$ of iterative sets on it, as we will define
below. The transfinite hierarchy of iterative sets consists of the sets each
of which is obtained by embedding the sets in $\mathcal{V}^{\alpha,t}_{(a,f)}$
into $\mathbb{V}$ via the mapping $\mathbf{h}^{\alpha,t}_{(a,f)}$ defined
below. [Transfinite Hierarchy of Iterative Sets] The transfinite hierarchy of
iterative sets is defined via the type $\mathcal{V}^{\alpha,t}_{(a,f)}$ and
the mapping
$\mathbf{h}^{\alpha,t}_{(a,f)}:\mathcal{V}^{\alpha,t}_{(a,f)}\to\mathbb{V}$:

$\displaystyle\widehat{\mathcal{V}}^{\alpha,t}_{(a,f)}$
$\displaystyle:=\widehat{\mathrm{W}}_{\mathbb{M}}(\widehat{\mathcal{U}}^{\alpha,t}_{(a,f)},\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}):\mathbb{M}$
$\displaystyle\mathcal{V}^{\alpha,t}_{(a,f)}$
$\displaystyle:=\mathrm{T}_{\mathbb{M}}(\widehat{\mathcal{V}}^{\alpha,t}_{(a,f)})$
$\displaystyle\mathbf{h}^{\alpha,t}_{(a,f)}\mathsf{sup}(b,g)$
$\displaystyle:=\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}b,\lambda
x.\mathbf{h}^{\alpha,t}_{(a,f)}(g\>x))$
$\displaystyle\mathbf{V}^{\alpha,t}_{(a,f)}$
$\displaystyle:=\mathsf{sup}(\widehat{\mathcal{V}}^{\alpha,t}_{(a,f)},\mathbf{h}^{\alpha,t}_{(a,f)}):\mathbb{V}$

Lemma 8 below shows that $\mathbf{V}^{\alpha,t}_{(a,f)}$ is $\alpha$-set-
inaccessible: it is the hierarchy defined above that validates the axiom Pi-
Numbers in $\mathbf{MLM}$ with $\mathrm{Acc}$. We first provide several lemmas
to prove Lemma 8. Note that the set-theoretic terms “transitive”, “regular”,
“$\alpha$-set-inaccessible” and “unbounded” below are in fact their
translations in $\mathbf{MLTT}$.

######  Lemma 4.

The following holds:

  1. (1)

For any $\alpha:\mathbb{V}$, we have
$\alpha\doteq\mathsf{sup}(\mathsf{index}\>\alpha,\mathsf{pred}\>\alpha)$.

  2. (2)

For any $\alpha,\beta:\mathbb{V}$, if $\alpha\doteq\beta$ holds then
$\Pi_{(\gamma:\mathbb{V})}(\gamma\in\alpha\to\gamma\in\beta)$ holds.

  3. (3)

For any $a:\mathbb{M}$ and $f,g:\mathrm{T}_{\mathbb{M}}a\to\mathbb{V}$, if
$\Pi_{(x:\mathrm{T}_{\mathbb{M}}a)}f\>x\doteq g\>x$ holds then
$\mathsf{sup}(a,f)\doteq\mathsf{sup}(a,g)$ holds.

  4. (4)

For any $\alpha,\beta:\mathbb{V}$, if both
$\Pi_{(\gamma:\mathbb{V})}(\gamma\in\alpha\to\gamma\in\beta)$ and
$\Pi_{(\gamma:\mathbb{V})}(\gamma\in\beta\to\gamma\in\alpha)$ holds then
$\alpha\doteq\beta$ holds.

######  Proof 3.1.

The statements (1) and (2) are provable by the induction principle of
$\mathbb{V}$. The statement (3) follows straightforwardly, and (4) holds
because the axiom Extensionality is interpretable in $\mathbf{MLTT}$.

In a way similar to define the relations $\doteq$ and $\in$ on $\mathbb{V}$,
the equivalence relation $\doteq^{\alpha,t}_{(a,f)}$ and the membership
relation $\in^{\alpha,t}_{(a,f)}$ on $\mathcal{V}^{\alpha,t}_{(a,f)}$ can be
defined, as remarked in [17]. One can prove the following lemma for these
relations.

######  Lemma 5.

The following holds:

  1. (1)

For any $x:\mathcal{V}^{\alpha,t}_{(a,f)}$, we have
$x\doteq^{\alpha,t}_{(a,f)}\mathsf{sup}(\mathsf{index}\>x,\mathsf{pred}\>x)$.

  2. (2)

$\mathbf{V}^{\alpha,t}_{(a,f)}$ is transitive.

  3. (3)

For any $x,y:\mathcal{V}^{\alpha,t}_{(a,f)}$, $x\in^{\alpha,t}_{(a,f)}y$ holds
if and only if
$\mathbf{h}^{\alpha,t}_{(a,f)}x\in\mathbf{h}^{\alpha,t}_{(a,f)}y$ holds.

  4. (4)

For any $x,y:\mathcal{V}^{\alpha,t}_{(a,f)}$, $x\doteq^{\alpha,t}_{(a,f)}y$
holds if and only if
$\mathbf{h}^{\alpha,t}_{(a,f)}x\doteq\mathbf{h}^{\alpha,t}_{(a,f)}y$ holds.

  5. (5)

$\mathbf{V}^{\alpha,t}_{(a,f)}$ is set-inaccessible.

######  Proof 3.2.

The statement (1) is proved by induction on $\mathcal{V}^{\alpha,t}_{(a,f)}$.
For the proofs of (2), (3) and (4), see [17, Lemma 4.7]; for the proof of (5),
see [17, Corollary 4.8].

By a standard argument using the induction principle of identity types, we
have the so-called indiscernibility of identicals, which is also called the
transport lemma: for any $A,B$ with $\Gamma,z:A\vdash B\;\mathrm{type}$,

$\mathsf{transport}^{B}:\Pi_{(x:A)}\Pi_{(y:A)}(x=_{A}y\to B[x/z]\to B[y/z]).$

For the sake of brevity, we often treat the first two arguments of
$\mathsf{transport}^{B}$ as implicit.

######  Lemma 6.

The following holds:

  1. (1)

For any $a,b:\mathbb{M}$, if $p:a=_{\mathbb{M}}b$ holds then for any
$g:\mathrm{T}_{\mathbb{M}}(b)\to\mathbb{V}$,

$\mathsf{sup}(a,\lambda
x.g\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(z)}\>a\>b\>p\>x))\doteq\mathsf{sup}(b,g)$

holds.

  2. (2)

For any $\alpha:\mathbb{V}$, $t:\mathrm{Acc}\>\alpha$, $a:\mathbb{M}$,
$g:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}$ and
$x:\mathrm{T}_{\mathbb{M}}(a)$, there is a term $c$ of type
$\mathcal{U}^{\alpha,t}_{(a,g)}$ such that
$\widehat{\mathrm{T}}^{\alpha,t}_{(a,g)}(c)=_{\mathbb{M}}g\>x$ holds.

######  Proof 3.3.

One can prove the statement (1) by the induction principle of identity types:
it suffices to verify that the claim

$\mathsf{sup}(a,\lambda
x.g\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(z)}\>a\>a\>\mathsf{refl}(a)\>x))\doteq\mathsf{sup}(a,g)$

holds. Since
$\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(z)}\>a\>a\>\mathsf{refl}(a)$ is
definitionally equal to the identity function on $\mathrm{T}_{\mathbb{M}}(a)$,
the claim holds by the definition of $\doteq$.

Next, we prove (2) by transfinite induction on $t:\mathrm{Acc}\;\alpha$, so
let $t$ be $\mathsf{prog}\>f^{\prime}$. We have

$\displaystyle\mathcal{U}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,g)}$
$\displaystyle=\mathrm{T}_{\mathbb{M}}(\mathsf{p}_{1}(\Phi\>\alpha\>(\mathsf{prog}\>f^{\prime})\>(a,g)))$
$\displaystyle=\mathrm{T}_{\mathbb{M}}(\mathsf{p}_{1}(\mathrm{u}^{\mathbb{M}}(\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
y.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\>(f^{\prime}\>y))\>(a,g)))$
$\displaystyle=\mathrm{U}_{f^{\mathbb{M}}[\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
y.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\>(f^{\prime}\>y),a,g]}.$

Put $f^{\ast}:=f^{\mathbb{M}}[\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
y.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\>(f^{\prime}\>y),a,g]$. Note
that we have
$\mathrm{U}_{f^{\ast}}=\mathcal{U}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,g)}$
and
$\widehat{\mathrm{T}}_{f^{\ast}}=\widehat{\mathrm{T}}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,g)}$.
It then follows that

$\widehat{\mathrm{T}}_{f^{\ast}}(\mathsf{res}^{1}_{f^{\ast}}(\widehat{\mathrm{N}_{0}}_{f^{\ast}},\lambda
v.\mathsf{E}_{0}v,\mathsf{i}\mathsf{i}\mathsf{j}\>x))=\mathsf{p}_{2}(f^{\ast}(\widehat{\mathrm{T}}_{f^{\ast}}(\widehat{\mathrm{N}_{0}}_{f^{\ast}}),\lambda
v.\widehat{\mathrm{T}}_{f^{\ast}}(\mathsf{E}_{0}v),\mathsf{i}\mathsf{i}\mathsf{j}\>x))=g\>x$

holds. So the term
$\mathsf{res}^{1}_{f^{\ast}}(\widehat{\mathrm{N}_{0}}_{f^{\ast}},\lambda
v.\mathsf{E}_{0}v,\mathsf{i}\mathsf{i}\mathsf{j}\>x):\mathrm{U}_{f^{\ast}}$
satisfies the claim.

The following is the main lemma in our proof. Informally, this lemma says that
$\mathbf{V}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$ is unbounded in
$(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u)$-set-inaccessibles for any
$u:\overline{\alpha_{\mathsf{tc}}}$.

######  Lemma 7 (Main Lemma).

If $\xi\in\mathbf{V}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$ holds, then
for any $u:\overline{\alpha_{\mathsf{tc}}}$, there are terms
$b:\mathcal{U}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$ and
$g:\mathrm{T}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}(b)\to\mathcal{U}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$
such that

$\xi\in\mathbf{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}\in\mathbf{V}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$

holds with
$b^{\ast}:=\widehat{\mathrm{T}}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}(b)$
and $g^{\ast}:=\lambda
x.\widehat{\mathrm{T}}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}(g\>x)$.

######  Proof 3.4.

Below we abbreviate $\mathsf{prog}\>f^{\prime}$ as $t$. Since
$\mathbf{V}^{\alpha,t}_{(a,f)}$ is set-inaccessible by Lemma 5.(5), the
singleton $\\{\xi\\}$ also belongs to $\mathbf{V}^{\alpha,t}_{(a,f)}$.
Moreover, there is a regular set $\beta\in\mathbf{V}^{\alpha,t}_{(a,f)}$ such
that $\xi\in\beta$ holds and $\beta$ is transitive. It follows that
$\beta\doteq\mathbf{h}^{\alpha,t}_{(a,f)}x$ holds for some
$x:\mathcal{V}^{\alpha,t}_{(a,f)}$. We have
$x\doteq^{\alpha,t}_{(a,f)}\mathsf{sup}(\mathsf{index}\>x,\mathsf{pred}\>x)$
by Lemma 5.(1), so

$\beta\doteq\mathbf{h}^{\alpha,t}_{(a,f)}x\doteq\mathbf{h}^{\alpha,t}_{(a,f)}\mathsf{sup}(\mathsf{index}\>x,\mathsf{pred}\>x)=\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(\mathsf{index}\>x),\lambda
y.\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>x\>y))$

holds by Lemma 5.(4).

Put

  * •

$b:=\mathsf{index}\>x:\mathcal{U}^{\alpha,t}_{(a,f)}$ and $g:=\lambda
z.\mathsf{index}\>(\mathsf{pred}\>x\>z):\mathrm{T}^{\alpha,t}_{(a,f)}(b)\to\mathcal{U}^{\alpha,t}_{(a,f)}$,
where
$\mathrm{T}^{\alpha,t}_{(a,f)}(b)=\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(b))$
holds by definition,

  * •

$b^{\ast}:=\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(b):\mathbb{M}$ and
$g^{\ast}:=\lambda
w.\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(g\>w):\mathrm{T}^{\alpha,t}_{(a,f)}(b)\to\mathbb{M}$,

  * •

$\widehat{\mathcal{U}}:=\widehat{\mathcal{U}}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}$.

We first show that $\mathcal{U}^{\alpha,t}_{(a,f)}$ has a code for
$\widehat{\mathcal{U}}$. We have by definition

$\displaystyle\mathcal{U}^{\alpha,t}_{(a,f)}$
$\displaystyle=\mathrm{T}_{\mathbb{M}}(\mathsf{p}_{1}(\Phi^{\alpha,t}_{(a,f)}))$
$\displaystyle=\mathrm{T}_{\mathbb{M}}(\mathsf{p}_{1}(\mathrm{u}^{\mathbb{M}}(\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
y.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\>(f^{\prime}\>y))(a,f)))$
$\displaystyle=\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{U}}_{f^{\mathbb{M}}[\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
y.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\>(f^{\prime}\>y),a,f]})$
$\displaystyle=\mathrm{U}_{f^{\mathbb{M}}[\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
y.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\>(f^{\prime}\>y),a,f]}.$

In this proof, we abbreviate
$f^{\mathbb{M}}[\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
y.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\>(f^{\prime}\>y),a,f]$ as
$f^{\mathbb{M}}$. Recall that $f^{\mathbb{M}}$ is of the form

$\lambda
w.(\widehat{\mathrm{N}_{1}}_{\mathbb{M}}\>\widehat{+}_{\mathbb{M}}\>a\>\widehat{+}_{\mathbb{M}}\>(\mathsf{index}\>\alpha_{\mathsf{tc}})\>\widehat{+}_{\mathbb{M}}\>\widehat{\Sigma}_{\mathbb{M}}(\mathsf{index}\>\alpha_{\mathsf{tc}},\lambda
w^{\prime}.\mathsf{p}_{1}((\lambda
y.\Phi\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>y)\>(f^{\prime}\>y))\>w^{\prime}\>w)),\>h^{\mathbb{M}}\>w)$

by Definition 2.2.

On the other hand, the following holds for
$\mathsf{res}^{1}_{f^{\mathbb{M}}}(b,g,\mathsf{i}\mathsf{j}\>u):\mathcal{U}^{\alpha,t}_{(a,f)}$.

$\displaystyle\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(\mathsf{res}^{1}_{f^{\mathbb{M}}}(b,g,\mathsf{i}\mathsf{j}\>u))$
$\displaystyle=\mathsf{p}_{2}(f^{\mathbb{M}}(b^{\ast},g^{\ast}))\>(\mathsf{i}\mathsf{j}\>u)$
$\displaystyle=h^{\mathbb{M}}(b^{\ast},g^{\ast})\>(\mathsf{i}\mathsf{j}\>u)=\widehat{\mathcal{U}}$

Therefore, $\mathsf{res}^{1}_{f^{\mathbb{M}}}(b,g,\mathsf{i}\mathsf{j}\>u)$ is
a code of $\widehat{\mathcal{U}}$ in $\mathcal{U}^{\alpha,t}_{(a,f)}$. Put
$\widetilde{\mathcal{U}}:=\mathsf{res}^{1}_{f^{\mathbb{M}}}(b,g,\mathsf{i}\mathsf{j}\>u)$.
Then, by defining

$\widetilde{\mathrm{T}}:=\lambda
z.\mathsf{res}^{1}_{f^{\mathbb{M}}}(b,g,\mathsf{j}(u,z)):\mathrm{T}^{\alpha,t}_{(a,f)}(\widetilde{\mathcal{U}})\to\mathcal{U}^{\alpha,t}_{(a,f)},$

we have
$\widetilde{\mathcal{V}}:=\widehat{\mathrm{W}}_{f^{\mathbb{M}}}(\widetilde{\mathcal{U}},\widetilde{\mathrm{T}}):\mathcal{U}^{\alpha,t}_{(a,f)}$.

Next, we show that
$\xi\in\mathbf{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}$
holds. Let
$\widehat{\mathbf{V}}:=\mathbf{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}$.
It suffices to verify that for any $\delta:\mathbb{V}$, if $\delta\in\beta$
holds then $\delta\in\widehat{\mathbf{V}}$ holds, because we have
$\xi\in\beta$.

We prove the claim by transfinite induction on $\delta$. Assume that
$\delta\in\beta$ holds, so we have
$\delta\doteq\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>x\>z)$ for some
$z:\mathrm{T}^{\alpha,t}_{(a,f)}(b)$. Let $C^{\prime}:=g\>z$. For any
$v:\mathrm{T}^{\alpha,t}_{(a,f)}(C^{\prime})$, we have

$\displaystyle\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>(\mathsf{pred}\>x\>z)\>v)$
$\displaystyle\in\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(\mathsf{index}(\mathsf{pred}\>x\>z)),\lambda
y.\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>(\mathsf{pred}\>x\>z)\>y))$
$\displaystyle=\mathbf{h}^{\alpha,t}_{(a,f)}\mathsf{sup}(\mathsf{index}\>(\mathsf{pred}\>x\>z),\mathsf{pred}\>(\mathsf{pred}\>x\>z))$
$\displaystyle\doteq\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>x\>z)$
$\displaystyle\doteq\delta.$

Since $\beta$ is transitive, we have
$\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>(\mathsf{pred}\>x\>z)\>v)\in\beta$,
so
$\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>(\mathsf{pred}\>x\>z)\>v)\in\widehat{\mathbf{V}}$
by IH of induction on $\delta$. Thus,

$\Pi_{(v:\mathrm{T}^{\alpha,t}_{(a,f)}(C^{\prime}))}\Sigma_{(y:\mathcal{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})})}\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>(\mathsf{pred}\>x\>z)\>v)\doteq\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}y$

holds, hence we have by the type-theoretic axiom of choice provable in
$\mathbf{MLTT}$

$\displaystyle\Sigma_{(g^{\prime}:\mathrm{T}^{\alpha,t}_{(a,f)}(C^{\prime})\to\mathcal{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})})}\Pi_{(v:\mathrm{T}^{\alpha,t}_{(a,f)}(C^{\prime}))}\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>(\mathsf{pred}\>x\>z)\>v)\doteq\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(g^{\prime}\>v).$
(1)

On the other hand, by Lemma 6.(2), there is a term $C$ of type
$\mathcal{U}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}$
such that
$\widehat{\mathrm{T}}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(C)=_{\mathbb{M}}g^{\ast}\>z$
holds. Since
$g^{\ast}\>z=\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(g\>z)=\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(C^{\prime})$
holds, we have a term $p$ of type
$\widehat{\mathrm{T}}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(C)=_{\mathbb{M}}\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(g\>z)$.
Therefore, we also have a term

$\mathsf{sup}(C,\lambda
y.g^{\prime}\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>y)):\mathcal{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})},$

because for any
$y:\widehat{\mathrm{T}}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(C)$,
we have
$g^{\prime}\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>y):\mathcal{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}$.
So

$\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}\mathsf{sup}(C,\lambda
y.g^{\prime}\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>y))\in\widehat{\mathbf{V}}=\mathbf{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}$

holds.

Then, by 1 and Lemma 6.(1),

$\displaystyle\;\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}\mathsf{sup}(C,\lambda
y.g^{\prime}\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>y))$
$\displaystyle\doteq\mathsf{sup}(\widehat{\mathrm{T}}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(C),\lambda
y.\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(g^{\prime}\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>y)))$
$\displaystyle\doteq\mathsf{sup}(\widehat{\mathrm{T}}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(C),\lambda
y.\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>(\mathsf{pred}\>x\>z)\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>y)))$
$\displaystyle\doteq\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(C^{\prime}),\lambda
y.\mathbf{h}^{\alpha,t}_{(a,f)}(\mathsf{pred}\>(\mathsf{pred}\>x\>z)\>y))$
$\displaystyle\doteq\delta$

holds, so we have $\delta\in\widehat{\mathbf{V}}$.

Finally, we show that $\widehat{\mathbf{V}}\in\mathbf{V}^{\alpha,t}_{(a,f)}$
holds. Recall that $\widetilde{\mathcal{V}}$ is of type
$\mathcal{U}^{\alpha,t}_{(a,f)}$, and put

$\mathcal{V}:=\mathrm{T}^{\alpha,t}_{(a,f)}(\widetilde{\mathcal{V}})=\mathrm{W}_{(v:\widehat{\mathcal{U}})}\mathrm{T}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(v).$

By recursion on $\mathcal{V}$, we define
$l:\mathcal{V}\to\mathcal{V}^{\alpha,t}_{(a,f)}$ as

$l\>\mathsf{sup}(d,q):=\mathsf{sup}(\widetilde{\mathrm{T}}\>d,\lambda
y.l\>(q\>y)),$

and put
$\mathbf{V}^{\prime}:=\mathsf{sup}(\widetilde{\mathcal{V}},l):\mathcal{V}^{\alpha,t}_{(a,f)}$.

We then define
$\beta^{\prime}:=\mathbf{h}^{\alpha,t}_{(a,f)}\mathbf{V}^{\prime}:\mathbb{V}$,
so $\beta^{\prime}\in\mathbf{V}^{\alpha,t}_{(a,f)}$ holds. It suffices to show
that we have $\beta^{\prime}\doteq\widehat{\mathbf{V}}$.

We first show that

$\displaystyle\Pi_{(v:\mathcal{V})}\mathbf{h}^{\alpha,t}_{(a,f)}(l\>v)\doteq\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}v$
(2)

holds by induction on $v=\mathsf{sup}(c,q)$. It follows from the induction
hypothesis that we have

$\Pi_{(y:\mathrm{T}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}c)}\mathbf{h}^{\alpha,t}_{(a,f)}(l\>(q\>y))\doteq\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(q\>y).$

So,

$\displaystyle\mathbf{h}^{\alpha,t}_{(a,f)}(l\>v)$
$\displaystyle=\mathbf{h}^{\alpha,t}_{(a,f)}\mathsf{sup}(\widetilde{\mathrm{T}}\>c,\lambda
y.l\>(q\>y))$
$\displaystyle=\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(\widetilde{\mathrm{T}}\>c),\lambda
y.\mathbf{h}^{\alpha,t}_{(a,f)}(l\>(q\>y)))$
$\displaystyle\doteq\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(\widetilde{\mathrm{T}}\>c),\lambda
y.\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(q\>y))$
$\displaystyle=\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}v$

holds. The last equation here holds because

$\displaystyle\widehat{\mathrm{T}}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}(c)$
$\displaystyle=\mathsf{p}_{2}(\Phi^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})})\>c$
$\displaystyle=h^{\mathbb{M}}(b^{\ast},g^{\ast})\>(\mathsf{j}(u,c))\text{ with
}u:\overline{\alpha_{\mathsf{tc}}}$
$\displaystyle=\mathsf{p}_{2}(f^{\mathbb{M}}(b^{\ast},g^{\ast}))\>\mathsf{j}(u,c)$
$\displaystyle=\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(\mathsf{res}^{1}_{f^{\mathbb{M}}}(b,g,\mathsf{j}(u,c)))$
$\displaystyle=\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(\widetilde{\mathrm{T}}\>c).$

Therefore, we have 2.

Since
$\beta^{\prime}=\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{(a,f)}(\widetilde{\mathcal{V}}),\lambda
y.\mathbf{h}^{\alpha,t}_{(a,f)}(l\>y))$ holds, if we have
$\eta\in\beta^{\prime}$ then $\eta\doteq\mathbf{h}^{\alpha,t}_{(a,f)}(l\>v)$
holds for some $v:\mathcal{V}$. We thus have
$\eta\doteq\mathbf{h}^{\alpha,t}_{(a,f)}(l\>v)\doteq\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}v\in\widehat{\mathbf{V}}$
by 2.

Conversely, if $\eta\in\widehat{\mathbf{V}}$ holds then
$\eta\doteq\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}v$
holds for some $v:\mathcal{V}$. So, we have

$\displaystyle\eta$
$\displaystyle\doteq\mathbf{h}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}v$
$\displaystyle\doteq\mathbf{h}^{\alpha,t}_{(a,f)}(l\>v)\text{ by
}\ref{eq:ell}$ $\displaystyle\in\beta^{\prime}.$

It follows that $\beta^{\prime}\doteq\widehat{\mathbf{V}}$.

We now prove the lemma saying that for any $\alpha:\mathbb{V}$ such that
$\mathrm{Acc}\>\alpha$ holds with $a:\mathbb{M}$ and
$f:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}$, $\mathbf{V}^{\alpha,t}_{(a,f)}$
is $\alpha$-set-inaccessible.

######  Lemma 8.

For all $\alpha:\mathbb{V}$, $t:\mathrm{Acc}\>\alpha$, $a:\mathbb{M}$ and
$f:\mathrm{T}_{\mathbb{M}}(a)\to\mathbb{M}$, $\mathbf{V}^{\alpha,t}_{(a,f)}$
is $\alpha$-set-inaccessible.

######  Proof 3.5.

Induction on $\alpha$ followed by subinduction on $t$. Let $\beta\in\alpha$ be
the case. We then have $\beta\in\alpha_{\mathsf{tc}}$, so
$\beta\doteq\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u$ for some
$u:\overline{\alpha_{\mathsf{tc}}}$.

If $\xi\in\mathbf{V}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$ holds then
Lemma 7 implies that there are terms
$b:\mathcal{U}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$ and
$g:\mathrm{T}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}(b)\to\mathcal{U}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$
with

$\xi\in\mathbf{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}\in\mathbf{V}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)},$

where
$b^{\ast}:=\widehat{\mathrm{T}}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}(b)$
and $g^{\ast}:=\lambda
x.\widehat{\mathrm{T}}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}(g\>x)$.

By IH of main induction,
$\mathbf{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}$
is $(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u)$-set-inaccessible. Since
$\alpha$-set-inaccessibility is the translation of a corresponding set-
theoretic formula for any $\alpha:\mathbb{V}$, Lemma 3 implies that if
$\delta\doteq\eta$ holds and $\gamma$ is $\delta$-set-inaccessible then
$\gamma$ is also $\eta$-set-inaccessible. Therefore,
$\mathbf{V}^{\mathsf{pred}\>\alpha_{\mathsf{tc}}\>u,f^{\prime}\>u}_{(b^{\ast},g^{\ast})}$
is also $\beta$-set-inaccessible, and it follows that $\beta$-set-
inaccessibles are unbounded in
$\mathbf{V}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$. By Lemmas 2 and
5.(5), $\mathbf{V}^{\alpha,\mathsf{prog}\>f^{\prime}}_{(a,f)}$ is
$\alpha$-set-inaccessible.

Below we use the following notations:

$\displaystyle\widehat{\mathcal{U}}^{\alpha,t}_{\beta}$
$\displaystyle:=\mathsf{p}_{1}(\Phi^{\alpha,t}_{(\mathsf{index}\>\beta,\lambda
x.\mathsf{index}\>(\mathsf{pred}\>\beta\>x))})$
$\displaystyle\mathcal{U}^{\alpha,t}_{\beta}$
$\displaystyle:=\mathrm{T}_{\mathbb{M}}\widehat{\mathcal{U}}^{\alpha,t}_{\beta}$
$\displaystyle\widehat{\mathrm{T}}^{\alpha,t}_{\beta}$
$\displaystyle:=\mathsf{p}_{2}(\Phi^{\alpha,t}_{(\mathsf{index}\>\beta,\lambda
x.\mathsf{index}\>(\mathsf{pred}\>\beta\>x))})$
$\displaystyle\mathrm{T}^{\alpha,t}_{\beta}$ $\displaystyle:=\lambda
x.\mathrm{T}_{\mathbb{M}}(\widehat{\mathrm{T}}^{\alpha,t}_{\beta}x)$
$\displaystyle\widehat{\mathcal{V}}^{\alpha,t}_{\beta}$
$\displaystyle:=\widehat{\mathrm{W}}_{\mathbb{M}}(\widehat{\mathcal{U}}^{\alpha,t}_{\beta},\widehat{\mathrm{T}}^{\alpha,t}_{\beta})$
$\displaystyle\mathcal{V}^{\alpha,t}_{\beta}$
$\displaystyle:=\mathrm{T}_{\mathbb{M}}\widehat{\mathcal{V}}^{\alpha,t}_{\beta}$

We also define $\mathbf{h}^{\alpha,t}_{\beta}$ and
$\mathbf{V}^{\alpha,t}_{\beta}$ as

$\mathbf{h}^{\alpha,t}_{\beta}\mathsf{sup}(b,g):=\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{\beta}(b),\lambda
x.\mathbf{h}^{\alpha,t}_{\beta}(g\>x)),\qquad\mathbf{V}^{\alpha,t}_{\beta}:=\mathsf{sup}(\widehat{\mathcal{V}}^{\alpha,t}_{\beta},\mathbf{h}^{\alpha,t}_{\beta}),$

respectively.

######  Lemma 9.

For any $\beta:\mathbb{V}$, if $\beta$ is transitive, then for any
$\alpha:\mathbb{V}$ and any $t:\mathrm{Acc}\>\alpha$, we have
$\Pi_{(\gamma:\mathbb{V})}(\gamma\in\beta\to\gamma\in\mathbf{V}^{\alpha,t}_{\beta})$.

######  Proof 3.6.

We prove
$\Pi_{(\gamma:\mathbb{V})}(\gamma\in\beta\to\gamma\in\mathbf{V}^{\alpha,t}_{\beta})$
by induction on $\gamma$. Suppose that $\gamma\in\beta$ holds. Then,
$\gamma\doteq\mathsf{pred}\>\beta\>x$ holds for some $x:\overline{\beta}$. Put
$\xi:=\mathsf{pred}\>\beta\>x$. If $u:\overline{\xi}$ holds, then we have
$\mathsf{pred}\>\xi\>u\in\gamma\in\beta$. Since $\beta$ is transitive, we also
have $\mathsf{pred}\>\xi\>u\in\beta$ and so
$\mathsf{pred}\>\xi\>u\in\mathbf{V}^{\alpha,t}_{\beta}$ holds by IH. We thus
have

$\Pi_{(u:\overline{\xi})}\Sigma_{(z:\mathcal{V}^{\alpha,t}_{\beta})}\mathsf{pred}\>\xi\>u\doteq\mathbf{h}^{\alpha,t}_{\beta}z.$

By the type-theoretic axiom of choice in $\mathbf{MLTT}$,

$\Sigma_{(f:\overline{\xi}\to\mathcal{V}^{\alpha,t}_{\beta})}\Pi_{(u:\overline{\xi})}\mathsf{pred}\>\xi\>u\doteq\mathbf{h}^{\alpha,t}_{\beta}(f\>u)$

holds.

On the other hand, by Lemma 6.(2), there is a term
$c:\mathcal{U}^{\alpha,t}_{\beta}$ such that

$p:\widehat{\mathrm{T}}^{\alpha,t}_{\beta}(c)=_{\mathbb{M}}(\lambda
z.\mathsf{index}\>(\mathsf{pred}\>\beta\>z))x$

holds. Then, it follows from Lemma 6.(1) that

$\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{\beta}(c),\lambda
x.\mathbf{h}^{\alpha,t}_{\beta}(f\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>x)))\doteq\mathsf{sup}(\mathsf{index}\>\xi,\lambda
u.\mathbf{h}^{\alpha,t}_{\beta}(f\>u))$

holds. Note that we have

$\mathsf{sup}(c,\lambda
x.f\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>x)):\mathcal{V}^{\alpha,t}_{\beta},\quad\mathbf{h}^{\alpha,t}_{\beta}\mathsf{sup}(c,\lambda
x.f\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>x))\in\mathbf{V}^{\alpha,t}_{\beta}.$

Moreover,

$\displaystyle\mathbf{h}^{\alpha,t}_{\beta}\mathsf{sup}(c,\lambda
x.f\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>x))$
$\displaystyle=\mathsf{sup}(\widehat{\mathrm{T}}^{\alpha,t}_{\beta}c,\lambda
x.\mathbf{h}^{\alpha,t}_{\beta}(f\>(\mathsf{transport}^{\mathrm{T}_{\mathbb{M}}(v)}\>p\>x)))$
$\displaystyle\doteq\mathsf{sup}(\mathsf{index}\>\xi,\lambda
u.\mathbf{h}^{\alpha,t}_{\beta}(f\>u))$
$\displaystyle\doteq\mathsf{sup}(\mathsf{index}\>\xi,\mathsf{pred}\>\xi)$
$\displaystyle\doteq\xi$

holds, hence we have $\gamma\doteq\xi\in\mathbf{V}^{\alpha,t}_{\beta}$.

######  Lemma 10.

The following holds:

  1. (1)

We have a term
$\mathrm{inv}:\Pi_{(\alpha:\mathbb{V})}(\mathrm{Acc}\>\alpha\to\Pi_{(x:\overline{\alpha_{\mathsf{tc}}})}\mathrm{Acc}\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>x))$.

  2. (2)

We have a function
$\mathrm{acc}:\Pi_{(\alpha:\mathbb{V})}\mathrm{Acc}\>\alpha$.

######  Proof 3.7.

(1) By induction on $t:\mathrm{Acc}\>\alpha$. Let $t$ be $\mathsf{prog}\>f$,
then we have $f\>x:\mathrm{Acc}\>(\mathsf{pred}\>\alpha_{\mathsf{tc}}\>x)$.

(2) By induction on $\alpha:\mathbb{V}$. Let $\alpha$ be $\mathsf{sup}(a,f)$,
and recall that $\overline{(\mathsf{sup}(a,f))_{\mathsf{tc}}}$ is
definitionally equal to
$\mathrm{T}_{\mathbb{M}}(a)+\Sigma_{(z:\mathrm{T}_{\mathbb{M}}(a))}\overline{(f\;z)_{\mathsf{tc}}}$.
Define
$g:\Pi_{(x:\overline{(\mathsf{sup}(a,f))_{\mathsf{tc}}})}\mathrm{Acc}\>(\mathsf{pred}\>(\mathsf{sup}(a,f))_{\mathsf{tc}}\>x)$
by

$\displaystyle g\>(\mathsf{i}\>z)$ $\displaystyle=\mathrm{acc}\>(f\>z),$
$\displaystyle g\>(\mathsf{j}\>w)$
$\displaystyle=\mathrm{inv}\>(f\>(\mathsf{p}_{1}\>w))\>(\mathrm{acc}\>(f\>(\mathsf{p}_{1}\>w)))\>(\mathsf{p}_{2}\>w).$

The function $g$ is well-defined because we have

$\mathsf{pred}\>(\mathsf{sup}(a,f))_{\mathsf{tc}}\>(\mathsf{i}\>z)=f\>z,\qquad\mathsf{pred}\>(\mathsf{sup}(a,f))_{\mathsf{tc}}\>(\mathsf{j}\>w)=\mathsf{pred}\>(f\>(\mathsf{p}_{1}\>w))_{\mathsf{tc}}\>(\mathsf{p}_{2}\>w).$

We then put $\mathrm{acc}\>(\mathsf{sup}(a,f)):=\mathsf{prog}\>g$.

We have an interpretation of Pi-Numbers in $\mathbf{MLM}$ by the theorem
below:

######  Theorem 11.

For any $\gamma,\alpha:\mathbb{V}$, there is a term $\beta:\mathbb{V}$ such
that $\gamma\in\beta$ holds and $\beta$ is $\alpha$-set-inaccessible.

######  Proof 3.8.

Let $\gamma,\alpha:\mathbb{V}$ be given. It is straightforward to define a
term $\gamma^{\prime}$ of $\mathbb{V}$ with $\gamma\in\gamma^{\prime}$, since
all axioms of $\mathbf{CZF}$ are interpretable in $\mathbf{MLTT}$. By Lemmas 9
and 10.(2), we have

$\Pi_{(\delta:\mathbb{V})}(\delta\in\gamma^{\prime}_{\mathsf{tc}}\to\delta\in\mathbf{V}^{\alpha,\mathrm{acc}\>\alpha}_{\gamma^{\prime}_{\mathsf{tc}}}).$

Therefore,
$\gamma\in\mathbf{V}^{\alpha,\mathrm{acc}\>\alpha}_{\gamma^{\prime}_{\mathsf{tc}}}$
holds, and
$\mathbf{V}^{\alpha,\mathrm{acc}\>\alpha}_{\gamma^{\prime}_{\mathsf{tc}}}$ is
$\alpha$-set-inaccessible by Lemma 8.

##  4\. Concluding Remark

In this paper, we showed that the system $\mathbf{CZF}_{\pi}$ of Aczel’s
constructive set theory with inaccessible sets is directly interpretable in a
variant of $\mathbf{MLTT}$ equipped with a Mahlo universe and accessibility
predicate $\mathrm{Acc}$. Our type-theoretic counterparts of inaccessible sets
were constructed by the transfinite iteration of a higher-order universe
operator whose definition used the reflection property of the Mahlo universe.
The accessibility predicate $\mathrm{Acc}$ provided a recursion principle to
iterate this operator.

A future research direction is to investigate the extent to which the
transfinite hierarchy of inaccessible sets can be extended in $\mathbf{MLTT}$.
In set-theoretic terms, the diagonalisation of this hierarchy gives the class
$\\{a\mid\text{$a$ is $a$-set-inaccessible}\\}$ (cf. [18]). Members of this
class can be considered as “fixed points” of an increasing sequence from
inaccessible sets. It would be interesting to examine whether $\mathbf{MLM}$
can construct an element of $\mathbb{V}$ corresponding to a member of this
class and, if possible, whether such elements of $\mathbb{V}$ are unbounded in
$\mathbb{V}$.

Another direction is to revisit our construction of inaccessible sets in
$\mathbf{MLM}$ from the viewpoint of homotopy type theory (HoTT). In [24],
Aczel’s interpretation of $\mathbf{CZF}$ in $\mathbf{MLTT}$ was refined: the
type of Aczel’s iterative sets was defined as a higher inductive type
$\mathbb{V}_{h}$. In addition to its ordinary introduction rule (i.e., its
point constructor rule), which is the same as that of $\mathbb{V}$, the higher
inductive type $\mathbb{V}_{h}$ also has path constructor rules. Although it
is unknown whether the axioms Strong Collection and Subset Collection of
$\mathbf{CZF}$ hold in this refined interpretation, several interesting
results on this interpretation have already been obtained (cf., e.g., [5]).
Later, a general framework for interpreting constructive set theory into HoTT
was proposed in [8]. Importantly, all axioms of $\mathbf{CZF}$ hold in some
interpretations of this framework; therefore, it would provide a HoTT
framework to revisit our direct interpretation of $\mathbf{CZF}_{\pi}$ in
$\mathbf{MLM}$ with $\mathrm{Acc}$.

## References

  * [1] Peter Aczel.  The type theoretic interpretation of constructive set theory.  In Angus Macintyre, Leszek Pacholski, and Jeff Paris, editors, Logic Colloquium ’77, volume 96 of Studies in Logic and the Foundations of Mathematics, pages 55–66. Elsevier, 1978.  doi:10.1016/S0049-237X(08)71989-X.
  * [2] Peter Aczel.  The type theoretic interpretation of constructive set theory: Choice principles.  In A. S. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 1–40. North-Holland, 1982.
  * [3] Peter Aczel.  The type theoretic interpretation of constructive set theory: Inductive definitions.  In R. B. Marcus, G. J. Dorn, and G. J. W. Dorn, editors, Logic, Methodology, and Philosophy of Science VII, pages 17–49. North-Holland, 1986\.
  * [4] Peter Aczel and Michael Rathjen.  Notes on constructive set theory.  Technical Report 40, Institut Mittag-Leffler, Djursholm, 2001.
  * [5] Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu.  Set-theoretic and type-theoretic ordinals coincide.  In LICS, pages 1–13, 2023.  doi:10.1109/LICS56636.2023.10175762.
  * [6] Frank R. Drake.  Set Theory, volume 76 of Studies in Logic and the Foundations of Mathematics.  Elsevier, 1974.  URL: http://www.sciencedirect.com/science/article/pii/S0049237X08717749, doi:https://doi.org/10.1016/S0049-237X(08)71774-9.
  * [7] Peter Dybjer and Erik Palmgren.  Intuitionistic Type Theory.  In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2020 edition, 2020.  URL: https://plato.stanford.edu/archives/sum2020/entries/type-theory-intuitionistic/.
  * [8] Cesare Gallozzi.  Homotopy type-theoretic interpretations of constructive set theories.  Math. Struct. Comput. Sci., 31(1):112–143, 2021.  doi:10.1017/S0960129519000148.
  * [9] Edward R. Griffor and Michael Rathjen.  The strength of some Martin-Löf type theories.  Arch. Math. Log., 33(5):347–385, 1994.  doi:10.1007/BF01278464.
  * [10] Martin Hofmann.  Syntax and semantics of dependent types.  In Andrew M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, Publications of the Newton Institute, pages 79–130. Cambridge University Press, Cambridge, 1997.  doi:10.1017/CBO9780511526619.004.
  * [11] Paul Mahlo.  Über lineare transfinite Mengen.  Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig. Mathematisch-Physische Klasse, 63:187–225, 1911.
  * [12] Per Martin-Löf.  Intuitionistic type theory: Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.  Bibliopolis, 1984.
  * [13] Bengt Nordström, Kent Petersson, and Jan M. Smith.  Programming in Martin-Löf’s type theory. An introduction. Oxford Univ. Press, 1990.
  * [14] Erik Palmgren.  On universes in type theory.  In Giovanni Sambin and Jan M. Smith, editors, Twenty Five Years of Constructive Type Theory, Oxford Logic Guides, pages 191–204. Oxford University Press, 1998.
  * [15] Michael Rathjen.  The superjump in Martin-Löf type theory.  In Samuel R. Buss, Petr Hájek, and Pavel Pudlák, editors, Logic Colloquium ’98, number 13 in Lecture Notes in Logic, pages 363–386. Cambridge University Press, Cambridge, 2000.  doi:10.1017/9781316756140.027.
  * [16] Michael Rathjen.  Realizing Mahlo set theory in type theory.  Arch. Math. Log., 42(1):89–101, 2003.  doi:10.1007/s00153-002-0159-6.
  * [17] Michael Rathjen, Edward R. Griffor, and Erik Palmgren.  Inaccessibility in constructive set theory and type theory.  Ann. Pure Appl. Log., 94(1-3):181–200, 1998.  doi:10.1016/S0168-0072(97)00072-9.
  * [18] Wayne Richter and Peter Aczel.  Inductive definitions and reflecting properties of admissible ordinals.  In J.E. Fenstad and P.G. Hinman, editors, Generalized Recursion Theory, volume 79 of Studies in Logic and the Foundations of Mathematics, pages 301–381. Elsevier, 1974.  doi:10.1016/S0049-237X(08)70592-5.
  * [19] Anton Setzer.  Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe.  PhD thesis, Universität München, 1993.
  * [20] Anton Setzer.  Well-ordering proofs for Martin-Löf type theory.  Ann. Pure Appl. Logic, 92(2):113–159, 1998.  doi:10.1016/S0168-0072(97)00078-X.
  * [21] Anton Setzer.  Extending Martin-Löf type theory by one Mahlo-universe.  Arch. Math. Log., 39(3):155–181, 2000.  doi:10.1007/s001530050140.
  * [22] Anton Setzer.  Proof theory and Martin-Löf Type Theory.  In M. van Atten, P. Boldini, M. Bourdeau, and G. Heinzmann, editors, One Hundred Years of Intuitionism (1907–2007), pages 257–279. Birkhäuser, 2008.  doi:10.1007/978-3-7643-8653-5_16.
  * [23] Anton Setzer.  Universes in type theory part I – Inaccessibles and Mahlo.  In A. Andretta, K. Kearnes, and D. Zambella, editors, Logic Colloquium ’04, pages 123–156. Association of Symbolic Logic, Lecture Notes in Logic 29, Cambridge University Press, 2008.  doi:10.1017/CBO9780511721151.009.
  * [24] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.