Construction of an infinite hierarchy of sets using types.

Question

This is not a duplicate of Sets. Classes. …?, because the linked question asks about the existence of a something larger than class. My question is about a construction of an infinite series of $\mathrm{Class}_1, \mathrm{Class}_2, \mathrm{Class}_3, \dots$ by a specific repeatable method using types.

---

The collection of all sets is a class. I think we can collect classes and continue this process as follows:

1. The collection of all sets is $\mathrm{Class}_1$.
2. The collection of all $\mathrm{Class}_1$ is $\mathrm{Class}_2$.
3. The collection of all $\mathrm{Class}_2$ is $\mathrm{Class}_3$.

...

---

First, let's look at how to construct natural numbers.

1. Let $\mathrm{N}$ be the type of natural numbers.
2. $1:\mathrm{N}$ .
3. If $n:\mathrm{N}$, then $\mathrm{suc}(n):\mathrm{N}$ .
4. All terms of $\mathrm{N}$ are constructed by repeating rules 2 and 3 finitely.

In addition to this, we need to define propositions and axioms of them:

5. $a:\mathrm{N}, b:\mathrm{N}\vdash a=b:\mathrm{Prop}$ .
6. $\forall n:\mathrm{N}. [\mathrm{suc}(n)\neq 1]$ is true.
7. $\forall m:\mathrm{N}. \forall n:\mathrm{N}. [a\neq b\Rightarrow \mathrm{suc}(a)\neq \mathrm{suc}(b)]$ is true.
8. If $\varphi(1)$ and $\varphi(n)\Rightarrow \varphi(n+1)$ are true, then $\forall n:\mathrm{N}. [\varphi(n)]$ is true.

In summary, the above process has 6 parts:

1. Define a type $T$.
2. Define initial terms of $T$.
3. Define construction rules of $T$.
4. The extension of type $T$ is the closure of 2 and 3.
5. Define the propositions of $T$.
6. Define the axioms of $T$.

---

Let's construct $\mathrm{Class}_1$.

The initial term of $\mathrm{Class}_1$ is $\emptyset$.

The construction rules are

• $A:\mathrm{Class}_1\vdash \mathcal{P}(A):\mathrm{Class}_1$
• $A:\mathrm{Class}_1, B:\mathrm{Class}_1\vdash A\cup B, A\cap B, A\times B, A\coprod B:\mathrm{Class}_1$
• $A:\mathrm{Class}_1, (x:A(\varphi(x)):\mathrm{PropositionInContext}_1\vdash \{x\in A| \varphi(x)\}:\mathrm{Class}_1$

etc.

The axioms are something like this:

• $A:\mathrm{Class}_1, B:\mathrm{Class}_1\vdash \forall x: \mathrm{Class}_1 (x\in A\cap B\Leftrightarrow x\in A \wedge x\in B)$
• $A:\mathrm{Class}_1, B:\mathrm{Class}_1\vdash \forall x: \mathrm{Class}_1 (x\in A\cup B\Leftrightarrow x\in A \vee x\in B)$
• $A:\mathrm{Class}_1, (x:A(\varphi(x)):\mathrm{PropositionInContext}_1\vdash \forall x:\mathrm{Class}_1(x\in \{x\in A| \varphi(x)\}\Leftrightarrow x\in A \wedge\varphi(x))$

etc.

The extension of $\mathrm{Class}_1$ is the closure of above rules. Let $\mathrm{Ext}(\mathrm{Class}_1)$ be this set. $\mathrm{Class}_2$ is constructed similarly but its initial term is $\mathrm{Ext}(\mathrm{Class}_1)$. Generally, the initial term of $\mathrm{Class}_{n+1}$ is $\mathrm{Ext}(\mathrm{Class}_n)$.

---

Is it possible to construct an infinite series of classes this way?