The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You're playing with fire here.  Consider the inductive type
Inductive foo (A : Type) (x : A) : A -> Type := Build_foo (y z : A) : x <> y -> x <> z -> y <> z -> foo A x x.

Then [foo Set True True] is inhabited (let y be False and z be bool), but [foo Prop True True] contradicts prop_extensionality+LEM and so cannot be inhabited.

What rule for universes of inductive types can you formulate that permits what you want for equality but forbids collapsing [foo Set True True] is to [foo Prop True True]?

On Mon, May 9, 2016, 4:01 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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