The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 13 sept. 2014, at 00:19, Jonathan 
<jonikelee AT gmail.com>
 wrote:

> On 09/12/2014 06:10 PM, Adam Chlipala wrote:
>> On 09/12/2014 06:04 PM, Jonathan wrote:
>>> Inductive Erasable(A : Type) : Prop :=
>>>      erasable: A -> Erasable A.
>>> 
>>>   Arguments erasable [A] _.
>>> 
>>>   Axiom Erasable_inj : forall {A : Type}{a b : A}, erasable a=erasable
>>>   b -> a=b.
>> 
>> We did the same thing in Ynot, and I think this axiom turned out to be 
>> inconsistent, period.  You don't need to assume any others to run into 
>> trouble.  I don't remember the details of the proof, though.
> 
> Wow - really?  Does anyone remember those details?

If you don’t have proof irrelevance I don’t see how you could have any
other equalities in Prop than if you put Erasable in Type, and then it is
perfectly consistent (and provable using strong elimination to Type).
Another way to say it is that it should be valid in proof-relevant models.
— Matthieu