# [TYPES] Transfinite universe levels

Erik Palmgren palmgren at math.su.se
Tue Jul 10 18:40:12 EDT 2018

```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
```