Re: Is [Equiv Type_i Type_i] contractible?

[Ulrik Buchholtz <ulrikbu...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1119 bytes --]

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
>

[-- Attachment #1.2: Type: text/html, Size: 1952 bytes --]