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…
2
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
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
2
1
1
Cheers! This rings a bell. And no worries, take care! 😊