Skip to main content
19 votes

Why is cumulativity not a given in proof assistants?

The short answer is that cummulativity is just one possible design choice which does not fit all purposes. The slightly longer answer is that baking commulativity into type theory is a very dramatic ...
Andrej Bauer's user avatar
  • 9,553
14 votes
Accepted

Why did Agda give up cumulative universes?

One reason (not particularly specific to Agda) might be that eta reduction is not compatible with cumulativity. With cumulativity (that is $Set_0 \leq Set_1$), and given \begin{align*} f &:= \...
Couchy's user avatar
  • 2,241
10 votes

Why is cumulativity not a given in proof assistants?

The biggest problem in my head is that cumulativity opens the door of subtyping in type theory, which, IMO, a potential calamity to type theory. If you elaborate cumulativity to non-cumulativity + ...
ice1000's user avatar
  • 6,256
8 votes

Formal description of algorithmic subtyping/cumulativity

See Universe Polymorphism in Coq (ITP 2014) by Matthieu Sozeau and Nicolas Tabareau (freely available draft) which explains in detail what Coq is doing.
Andrej Bauer's user avatar
  • 9,553
5 votes
Accepted

Formal description of algorithmic subtyping/cumulativity

For more recent references for, you can look at what MetaCoq does, either the code (there’s now a proof of correctness and completeness of an actual checker wrt. a declarative spec) or the papers (the ...
Meven Lennon-Bertrand's user avatar
2 votes
Accepted

Cumulativity unsafe in Agda 2.6.3

The --cumulativity flag is currently marked as unsafe because of the (quite poor) heuristic it uses for solving universe levels, which might lose solutions and ...
Jesper's user avatar
  • 506

Only top scored, non community-wiki answers of a minimum length are eligible