The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Are you sure about that? Univalence + (id:forall A, A->A->Prop) is problematic because 1/ it's incompatible with proof irrelevance (forall p:Prop, hprop p) 2/ it breaks extraction. But I don't think I've heard of an actual inconsistency of Univalence+Coq.

On 13 December 2013 14:09, Guillaume Brunerie <guillaume.brunerie AT gmail.com> wrote:

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