Should we use cumulative inductives by default?

[Alizter]

In Coq, we can specify a polymorphic inductive type A to be Cumulative which means that constructors of A@{i} can be lifted definitionally to act as constructors of A@{j} for i <= j.

We already use cumulativity for Equiv and paths. Would it be a good idea to set this globally?

Semantically, I believe that when we add type constructors to a CwF universe hierarchy, we want the constructor to commute strictly with lifts. I believe by setting cumulative polymorphic inductive types we are basically doing this for W-types.

Another question, is there any reason anybody would need to care about lifting operations? I'm not aware of any mathematics that explicitly requires them to work.

[SkySkimmer]

We can try to enable cumulative inductives, but prepare for many issues with universe constraint heuristics going wrong.

In Coq, we can specify a polymorphic inductive type A to be Cumulative which means that constructors of A@{i} can be lifted definitionally to act as constructors of A@{j} for i <= j.

This is slightly incorrect, the constraints on the universes depend on A.

[jdchristensen]

See #1680 and #1657 for some cases where it was easy to add cumulativity.