# Re: [TYPES] Transfinite universe levels

`[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]`
```

Hi

```
In my PhD thesis (Uppsala University 1991) I consider transfinite hierarchies of type universes in Martin-Löf type theory. Some of this was published in a 1998 proceedings:
```
```
"On universes in type theory, in: G. Sambin and J. Smith (eds.) Twenty Five Years of Constructive Type Theory. Oxford Logic Guides, Oxford University Press 1998, 191-204 (refereed collection of papers). Near final version in PDF."
```
http://staff.math.su.se/palmgren/publications.html

http://www2.math.uu.se/~palmgren/universe.pdf

```
The so-called superuniverses (V,S) (which admits transfinite iterations of universes) have been formalized in Agda. Here is an example of such a formalization:
```
---

-- building a universe above a family (A,B)

mutual
data U (A : Set) (B : A -> Set) : Set where
n₀ : U A B
n₁ : U A B
ix : U A B
lf : A -> U A B
_⊕_ : U A B -> U A B -> U A B
σ : (a : U A B) -> (T a -> U A B) -> U A B
π : (a : U A B) -> (T a -> U A B) -> U A B
n : U A B
w : (a : U A B) -> (T a -> U A B) -> U A B
i : (a : U A B) -> T a -> T a -> U A B

T : {A : Set} {B : A -> Set} ->  U A B -> Set
T n₀              = N₀
T n₁              = N₁
T {A} {B} ix      = A
T {A} {B} (lf a)  = B a
T (a ⊕ b)         = T a + T b
T (σ a b)         = Σ (T a) (\x -> T (b x))
T (π a b)         = Π (T a) (\x -> T (b x))
T n               = N
T (w a b)         = W (T a) (\x -> T (b x))
T (i a b c)       = I (T a) b c

-- the super universe (V, S): a universe which is closed also
-- under the above universe building operation

mutual
data V : Set where
n₀ : V
n₁ : V
_⊕_ : V -> V -> V
σ : (a : V) -> (S a -> V) -> V
π : (a : V) -> (S a -> V) -> V
n : V
w : (a : V) -> (S a -> V) -> V
i : (a : V) -> S a -> S a -> V
u : (a : V) -> (S a -> V) -> V
t : (a : V) -> (b : S a -> V) -> U (S a) (\x -> S (b x))  -> V

S : V -> Set
S n₀        = N₀
S n₁        = N₁
S (a ⊕ b)   = S a + S b
S (σ a b)   = Σ (S a) (\x -> S (b x))
S (π a b)   = Π (S a) (\x -> S (b x))
S n         = N
S (w a b)   = W (S a) (\x -> S (b x))
S (i a b c) = I (S a) b c
S (u a b)   = U (S a) (\x -> S (b x))
S (t a b c) = T {S a} {\x -> S (b x)} c
--

```
There is also work by Anton Setzer (Swansea U) of type universes that go far beyond this, Mahlo universes - a kind of ultimate universe polymorphism. These are significant constructions in proof theory.
```

Best Regards

Erik

Erik Palmgren
Prof Mathematical Logic
Department of Mathematics
Stockholm University

Den 2018-07-10 kl. 23:50, skrev Stefan Monnier:
```
```[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Most type theory-based tools nowadays are based on a calculus with an
infinite hierarchy of predicative universes.  Some of them, such as
Agda, also allow abstraction over those levels, so we end up with a PTS
along the lines of:

ℓ ::= z | s ℓ | ℓ₁ ∪ ℓ₂ | l      (where `l` is a level variable)

S = { Type ℓ, Type ω, SortLevel }
A = { Type ℓ : Type (ℓ + 1), TypeLevel : SortLevel }
R = { (Type ℓ₁, Type ℓ₂, Type (ℓ₁ ∪ ℓ₂)),
(SortLevel, Type ℓ, Type ω),
(SortLevel, Type ω, Type ω) }

I was wondering if there's been work to push this to larger ordinals, to
allow maybe rules like

(Type ω, Type ω, Type (ω·ω))

I.e. "deep universe polymorphism"

Stefan
```