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)

Filter by
Sorted by
Tagged with
3 votes
1 answer

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 ...
Evaristo's user avatar
  • 133
24 votes
2 answers

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?) ...
It'sNotALie.'s user avatar
  • 1,427
13 votes
1 answer

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 <...
ice1000's user avatar
  • 5,857
14 votes
2 answers

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 ...
ionchy's user avatar
  • 906