The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Does this work?

Lemma out_of_thin_air : forall {T1 T2: Prop},
    T1 = T2 -> T1 -> T2.
Proof.
  destruct 1; apply id.
Qed.

Goal True <> False.
  intro Heq.
  destruct (@out_of_thin_air True False Heq I).
Qed.


On 2016-05-09 18:03, Jonathan Leivent wrote:
> 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
>>>
>>>
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature