The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Well, yes. I think that was implicit in Daniel's original e-mail. There 
may be tricky details, though.

Maxime.

On 12/12/2013 07:52 PM, Robbert Krebbers 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.