[TYPES] Transfinite universe levels

[Erik Palmgren]

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