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)
4
questions
3
votes
1
answer
112
views
Cumulativity unsafe in Agda 2.6.3
I've been reading and understand the design choices behind Agda not having a cumulative universe hierarchy by default. However, while tinkering with the language, I've noticed that, at least for Agda ...
- 133
24
votes
2
answers
436
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,427
13
votes
1
answer
365
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 <...
- 5,857
14
votes
2
answers
123
views
Formal description of algorithmic subtyping/cumulativity
Are there any references (papers, documentation, etc.) for how proof assistants with subtyping due to cumulativity actually implement algorithmic subtyping? Coq, for instance, has subtyping, but the ...
- 906