The Coq mailing list

[Anthony Bordg <bordg.anthony AT gmail.com>]

Hi,

to answer the question by Robbert Krebbers: yes, using univalence  one has (0 -> 0) = 1 where 0 is the empty type and 1 is the unit type (to use notations and the type theory in HoTT book). Indeed, via univalence it suffices to have (0 -> 0) \equiv 1. Now notice that  0 -> 0 is inhabited and it's a mere proposition (so we will have the required equivalence with 1. It's not hard to show that if A is a mere proposition and is inhabited then it is equivalent to 1 ). The type 0 -> 0 is certainly inhabited by identity and it's a mere proposition by the following more general fact:  if A is any type and B is a mere proposition then the type A -> B is a mere proposition and 0 is of course a mere proposition. Thus  univalence is inconsistent with the current version of Coq.

Best

Anthony

2013/12/13 Robbert Krebbers <mailinglists AT robbertkrebbers.nl>

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.