Re: [HoTT] Is [Equiv Type_i Type_i] contractible?

[Martin Escardo <escardo...@googlemail.com>]

There was a proof in this list that if you have excluded middle than
there is an automorphism of U that flips the types 0 and 1. (Peter
Lumsdaine.)

And conversely that if there is an automorphism that flips the types 0
and 1, then excluded middle holds. (Myself.)

Hence "potentially" there are at least two automorphisms of U.

Martin

On 27/10/16 16:15, 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
> 
> -- 
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to HomotopyTypeThe...@googlegroups.com
> <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.