[Agda] another level problem

[Peter Hancock]

On 20/05/2021 17:56, András Kovács wrote:
> Making Level a first-class type, and putting it in the smallest universe,
> is OK: https://arxiv.org/abs/2103.00223

I'm sorry to admit I haven't yet read your paper, but I wonder what is the "smallest"
universe? Isn't that the empty universe?

A very interesting (and important) universe may be the boolean universe. One reason 
to think it is important is explained in Jan Smith's paper:
The Independence of Peano's Fourth Axiom from Martin-Löf's Type Theory without Universes
April 1996Journal of Symbolic Logic 5 3(3)

In between, there may be the singleton universe, in which there is only the empty set.
And then, one may wonder whether there is a universe of finite sets. Etc.

What's a universe?

Peter Hancock