The Coq mailing list

[Eric Finster <ericfinster AT gmail.com>]

> This proposition is false in the univalent model which gives one of the 
> possible proofs of the fact that it s not provable in Coq.

Indeed, there is a very simple topologically motivated counter example
which should be very easy to construct using the theory of higher
inductive types.
(http://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/)

>>>   Proposition projT2_fun (x : X) (s1 s2 : P x) : existT _ x s1 = existT _ 
>>> x s2
>>> ->  s1 = s2.

In the notation of the link, take X to be the circle, P base := bool,
s1 = true, s2 = false and P loop to be the self equivalence
interchanging true and false.  Topologically this is the degree 2 map
of the circle to itself.  The fiber is disconnected, but the total
space is connected.

Eric