<div dir="ltr">> but I wonder what is the "smallest"<br>universe?<div><br></div><div>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.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Peter Hancock <<a href="mailto:hancock@fastmail.fm">hancock@fastmail.fm</a>> ezt írta (időpont: 2021. máj. 20., Cs, 19:43):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 20/05/2021 17:56, András Kovács wrote:<br>
> Making Level a first-class type, and putting it in the smallest universe,<br>
> is OK: <a href="https://arxiv.org/abs/2103.00223" rel="noreferrer" target="_blank">https://arxiv.org/abs/2103.00223</a><br>
<br>
I'm sorry to admit I haven't yet read your paper, but I wonder what is the "smallest"<br>
universe? Isn't that the empty universe?<br>
<br>
A very interesting (and important) universe may be the boolean universe. One reason <br>
to think it is important is explained in Jan Smith's paper:<br>
The Independence of Peano's Fourth Axiom from Martin-Löf's Type Theory without Universes<br>
April 1996Journal of Symbolic Logic 5 3(3)<br>
<br>
In between, there may be the singleton universe, in which there is only the empty set.<br>
And then, one may wonder whether there is a universe of finite sets. Etc.<br>
<br>
What's a universe?<br>
<br>
Peter Hancock<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>