The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Dear Andrej,

On 17/12/2013 23:32, Andrej Bauer wrote:
> Several people have commented on the univalence and the present
> trouble. I would just like to clarify the situation a bit more.
>
> It is indeed the case that univalence implies that (False -> False) =
> True. However:
>
> 1) in HoTT we do not use Prop, so that should really be (Empty_set ->
> Empty_set) = unit.
Yes, but this is inconsistent as well with the current implementation. 
Naughty Prop has nothing to do with the current issue.

> 2) In HoTT we do not use match statements but rather the eliminators.
> I do not see how to reproduce the problem using False_rect.
True. As long as you're using the generated recursors, you are safe. 
None of the nice examples given by Cristobal Camarero do translate to 
the language of recursors.

> 3) There are numerous other incompatibilities between Coq and HoTT,
> which is why HoTT uses a patched Coq and abstains from using certain
> parts of Coq.
We'll have to apply the patch to HoTT-coq when we have it. I think I 
have a fix that rules out all of the counter-examples given on this 
list, but we need to be sure it is OK. And I'm not sure it'll be 
implemented before Christmas.

Anyway, people should not worry too much. The fix will probably change 
nothing for most people. Maybe Daniel Schepler will have to re-work on 
the last examples he submitted...

> On a more personal note, I think the present situation shows the value
> of having some semantics around to curb hasty adoption of rules that
> "look OK".
You need *formal* semantics ;-). Informal semantics did not save us here.

Bruno.