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

[Nicolai Kraus <nicola...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2728 bytes --]

On Thu, Oct 27, 2016 at 4:38 PM, 'Martin Escardo' via Homotopy Type Theory <
HomotopyT...@googlegroups.com> wrote:

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


Martin, I guess you mean:
https://groups.google.com/d/msg/homotopytypetheory/8CV0S2DuOI8/ZvS9S-gROfIJ

In your formulation of the construction, you can swap any two given types A
and B, not only 0 and 1. This is because you really only need to decide ||X
= A|| and ||X = B||.
-- Nicolai



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

[-- Attachment #2: Type: text/html, Size: 4381 bytes --]