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

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

On 27/10/16 16:19, 'Martin Escardo' via Homotopy Type Theory wrote:
> 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.)

I can't find the link to this proof. But here is one proof which is
either what Peter said or very similar to it.

To define such an automorphism f:U->U, given X:U, we have that X=0 and
X=1 are propositions. Hence we can use excluded middle to check if any
them holds, and define f(X) accordingly. Otherwise take f(X)=X.

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

I can find this one, which is slightly more complicated, but still short:

https://groups.google.com/d/msg/homotopytypetheory/8CV0S2DuOI8/Jn5EeSwxc4gJ

Martin



> 
> 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.
>