I'm a bit confused by `Level : Set` in Agda. Isn't this a bit circular, assuming `Set` is sugar for `Set 0`?
Level : Set lzero
lzero : Level
agda.github.io/agda-stdlib/Ag
Conversation
I'm not really convinced, haha… eg. defining it in a LF-style signature:
u : el level -> sort.
level : u lzero.
lzero : el level.
lsuc : el level -> el level.
el : {l : el level} -> u l -> sort.
…this mutual recursion seems super sketchy!
1
like, the `u` needs `el`, which is not yet declared… 😳
1
even worse `el` refers to… itself? but maybe this is ok. I'm not really clued up on the theory stuff… but maybe this is the insanity you were referring to…
tbh I don't think Level should be allowed to be a type at all
idk if this loopy stuff actually gets you an inconsistency but imo Level should be some sort of pretype, and you have a separate kind of quantification/abstraction/application of Levels
2
1
hmm yeah. I guess I had assumed that `Level` was `Setω` to prevent this kind of thing…?
1
1
1
Show replies
Oooh, I think I goofed here. You can break the mutual recursion by having something like:
tp : sort.
el : tp -> sort.
level : tp.
lzero : el level.
lsuc : el level -> el level.
u : level -> tp.
…etc. (too big for a tweet)
1
1
Section “3.4 Tarskian Universes” of “An Equational Logical Framework for Type Theories” goes through a version of this, although they have `Lvl` as a primitive in their logical framework: arxiv.org/abs/2106.01484
(This paper reminded me of it twitter.com/plt_abbie/stat)
Quote Tweet
Replying to @brendanzab @ionathanch and @i2talics
arxiv.org/pdf/2103.00223 i found this paper that seems to have Level : Set₀ but I'm not gonna read it right now I'm spent
1
1
Show replies