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 thought Level was supposed to be in Set\omega?
1
1
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
Yeah this is what I had assumed and was rather surprised to see it as `Set` 🤔
1
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Oh yeah, that's the one Abbie posted! Need to look more closely, it looks neat!