[TYPES] Transfinite universe levels

[Dan Doel]

To add to this a bit, the universes in Agda are actually (at least) Mahlo
universes. If you find the right paper by Setzer, it's not too hard to take
the definition of a Mahlo universe and write down something in Agda that
exhibits, say, Set as Mahlo (the sort of 'impredicative' definition of Mahlo
is the one you're looking for).

But also, Setzer has papers on universes that go _beyond_ Mahlo, to
incorporate (and understand) similar strong concepts from proof theory.
I forget if it's the Pi_3 universe or the Pi^1_1 universe (his page of
papers mentions both, and I don't remember enough details). But my
understanding is that it is a recursion-theoretic analogue of weakly
compact cardinals (whereas Mahlo universes/ordinals are related to
Mahlo cardinals). I don't think Agda's universes are this strong, though
I really don't understand well enough to say for sure.

-- Dan

On Tue, Jul 10, 2018 at 6:40 PM, Erik Palmgren <palmgren at math.su.se> wrote:

> [ 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/ma
>> ilman/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
>>
>