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
Replying to
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…?
Replying to
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
Show replies