All Questions
Tagged with universe-polymorphism agda
2
questions
15
votes
2
answers
417
views
In Agda, why is universe polymorphism explicit?
I've noticed that the process of coding a definition in Agda that is universe polymorphic usually requires little thought in how the Level parameters are specified. ...
- 361
13
votes
1
answer
429
views
Why did Agda give up cumulative universes?
In Ulf Norell's PhD thesis, which is considered the standard reference of the Agda 2 language, the universes are cumulative, say, Set i is not just an instance of <...
- 6,306