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
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
I see my article being mentioned here but I can give the short answer: we can put Level in whatever universe we want.
4
er... its just mutual recursion! dont worry about it! (or else youll go insane)
1
1
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
Show replies
Oh lol jinx
Quote Tweet
Replying to @ionathanch and @i2talics
hmm yeah. I guess I had assumed that `Level` was `Setω` to prevent this kind of thing…?
1
Show replies