[Agda] another level problem

[András Kovács]

> but I wonder what is the "smallest"
universe?

I meant the universe with the smallest level index in the particular
universe hierarchy that we're using. In Agda, the smallest such universe is
Set0, and indeed we have Level : Set0 there.

Peter Hancock <hancock at fastmail.fm> ezt írta (időpont: 2021. máj. 20., Cs,
19:43):

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210520/d1cc4b66/attachment.html>