This is (related to) Grothendieck's “inspiring assumption” of Pursuing Stacks section 28.

I only know of the treatment by Barwick and Schommer-Pries in On the Unicity of the Homotopy Theory of Higher Categories: https://arxiv.org/abs/1112.0040

Theorem 8.12 for n=0 says that the Kan complex of homotopy theories of (infinity,0)-categories is contractible. Of course this depends on their axiomatization, Definition 6.8. Perhaps some ideas can be adapted.

Cheers,

Ulrik

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