Thanks all for the answer.

I think our question was more "is it compatible with univalence or 
implied by univalence + some parametricity assumption ?".

Of course, assuming other axioms in the theory that allow to distinguish
between types makes it false.

Best, 

On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau wrote:
>
> Dear all,
>
>   we've been stuck with N. Tabareau and his student Théo Winterhalter on 
> the above question. Is it the case that all equivalences between a universe 
> and itself are equivalent to the identity? We can't seem to prove (or 
> disprove) this from univalence alone, and even additional parametricity 
> assumptions do not seem to help. Did we miss a counterexample? Did anyone 
> investigate this or can produce a proof as an easy corollary? What is the 
> situation in, e.g. the simplicial model?
>
> -- Matthieu
>