The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

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.

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.

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.

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".

With kind regards,

Andrej