coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Cumulative inductive types and universe polymorphism

From: David Leduc <david.leduc6 AT googlemail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Cumulative inductive types and universe polymorphism
Date: Sun, 6 Nov 2016 22:49:48 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=david.leduc6 AT googlemail.com; spf=Pass smtp.mailfrom=david.leduc6 AT googlemail.com; spf=None smtp.helo=postmaster AT mail-ua0-f171.google.com
Ironport-phdr: 9a23:ripcdBFbrmv6EaPuPYg7Sp1GYnF86YWxBRYc798ds5kLTJ75oM2wAkXT6L1XgUPTWs2DsrQf2rCQ4vurADJdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3p7xhrv5osOOKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOH/U7E4ERCv47pgAEvkgTkGO3g9/W3KgZJYg6VcrxasohV+x8jfZ4TDZ6k2Rb/UYd5PHTkJZc1WTSEUR9rkN4Y=

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

[Coq-Club] Cumulative inductive types and universe polymorphism, David Leduc, 11/06/2016
- Re: [Coq-Club] Cumulative inductive types and universe polymorphism, Matthieu Sozeau, 11/07/2016
  - Re: [Coq-Club] Cumulative inductive types and universe polymorphism, Bas Spitters, 11/07/2016