The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

On 2013/12/13 Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>
 wrote:
> On 12/13/2013 10:23 AM, Pierre-Marie Pédrot wrote:
>>
>> That's really surprising, to say the least... Is there a lot of
>> contributions using this axiom in the wild?
>
> Cannot we prove
>
>   (False -> False) = True
>
> using univalence? In that case, univalence would be inconsistent with the
> current version of Coq, which would be quite bad.

Well, even when this bug will be fixed, univalence is still
inconsistent with the calculus of constructions anyway, which is why
the HoTT people using Coq need a different version of Coq where the
identity type lands in Type and not in Prop.

Guillaume