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!
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
Show replies