The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

For the record, we found some likely applications for cumulative
inductive types here.
(As Matthieu knows well :-)  )

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman,
Matthieu Sozeau, Bas Spitters,
The HoTT Library: A formalization of homotopy type theory in Coq
https://arxiv.org/abs/1610.04591

On Mon, Nov 7, 2016 at 7:35 AM, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:
> Hi David,
>
> Yes, we're planning to work on it with Amin Timany for 8.7 or the following
> version.
> Do you have a particular application in mind?
>
> Best,
> -- Matthieu
>
> On Sun, 6 Nov 2016 at 23:50, David Leduc 
> <david.leduc6 AT googlemail.com>
> wrote:
>>
>> Hello,
>>
>> Universe polymorphism does not currently support cumulativity for
>> inductive types [1]. Is there any plan to add this feature in future
>> versions of Coq (8.6 or later)?
>>
>> [1] Amin Timany, Bart Jacobs. First Steps Towards Cumulative Inductive
>> Types in CIC.
>> http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW684.abs.html