coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] question about universes and equalities
Date: Mon, 09 May 2016 20:08:52 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f44.google.com
Ironport-phdr: 9a23:LPYl7RVtLCHWjFN8J3oPAEc2cujV8LGtZVwlr6E/grcLSJyIuqrYZhePt8tkgFKBZ4jH8fUM07OQ6PCxHzVaqs/a7zgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2CJVwSz2PmPvtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN/dwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl09tChTZ7BD3Q9/KtTn3v/c1jCyTIdH/SJgxUCi+5qItTwXn3nRUfwUl+X3a35QjxJlQpwis8kRy

On Mon, May 9, 2016 at 9:49 PM Stefan Monnier <monnier AT iro.umontreal.ca> wrote:

> Note that [@eq Type@{i} A B -> @eq Type@{j} A B] does not hold for [i > j],

Hmm.. which part of Coq's typing rules cause this?

Dependent elimination of the equality types forces you to abstract B by any type B' at level i, but then the @eq Type@{j} A B' won't typecheck.

-- Matthieu