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