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 HomotopyTypeTheory+unsub...@googlegroups.com
>> <mailto:HomotopyTypeTheory+unsub...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout.
>

--
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 HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.