The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Are you sure that thing is inhabited as you say?  I can't prove it - I 
end up with subgoals like "True <> False", which I don't think can be 
proven.

Even if it were, can't such a collapsing reduction be only about 
equalities, in much the same way that axiom K is only about equalities?

-- Jonathan


On 05/09/2016 05:12 PM, Jason Gross wrote:
> 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