Questions tagged [universe-polymorphism]
Universe polymorphism is the ability for definitions to be implicitly duplicated at different universe levels, with the types they contain. (from nLab).
3
questions
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
16
votes
1
answer
400
views
What happened to Conor McBride's universe polymorphism proposal?
Conor proposed a seemingly promising way towards universe polymorphism: https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html IMHO, the idea behind this proposal is:
You build things starting ...
- 6,306
8
votes
4
answers
246
views
What's the difference between a universe level and a natural number?
It seems that universe levels are just a type generated by a zero constant and a successor constructor (like in Agda), so why don't we adapt natural numbers as universe levels?
In Lean, it is also ...
- 6,306