Questions tagged [cumulativity]
A tower of universes is cumulative if A:Ui implies A:Ui+1 (rather than, say, Lift(A):Ui+1). (from Homotopy Type Theory)
2
questions
14
votes
1
answer
445
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,316
24
votes
2
answers
524
views
Why is cumulativity not a given in proof assistants?
It seems to me that there are no real reasons to not like cumulativity (the example given here seems to not be too relevant, according to the comments), and yet most proof assistants (apart from Coq?) ...
- 1,445