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

## Advertising

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