The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/09/2016 03:48 PM, Stefan Monnier 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?
>
>
>          Stefan

I'd just like to make it go away.  Specifically, I'd like [@eq Type@{i} 
A B] to reduce to [@eq Type@{j} A B] where j is the minimum permissible 
level considering A and B.

I guess one could have a type theory where some things are provably 
equal at higher levels but not at lower ones.  But, such a thing seems 
quite bizarre.

-- Jonathan