-
Notifications
You must be signed in to change notification settings - Fork 70
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Level universe #1023
Labels
help wanted
Extra attention is needed
Comments
Perhaps we should be looking for a modification of the definition of telescopes. I would much prefer that over enabling universe cumulativity. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Currently, the library is blocked from enabling the
--level-universe
option globally due to a single definition, namelytelescope
. Althoughtelescope
is a very useful construction, having--level-universe
enabled is also advantageous, for instance in modal type theory, where we currently have to distinguish between crisp and cohesive universe levels. Something which doesn't really make sense and leads to trouble.One route that reconciles having both
telescope
and--level-universe
is to enable the--cumulativity
option. This givessmall-telescope
the same expressivity astelescope
has currently, but comes with its own set of advantages and disadvantages:raise-...
constructs, and perhaps we will be able to infer telescopes without using the instance resolution mechanism.On the other hand
The text was updated successfully, but these errors were encountered: