From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.194.220.66 with SMTP id pu2mr781096wjc.4.1477588148604; Thu, 27 Oct 2016 10:09:08 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.46.145 with SMTP id u139ls5321wmu.22.canary-gmail; Thu, 27 Oct 2016 10:09:07 -0700 (PDT) X-Received: by 10.194.113.106 with SMTP id ix10mr764563wjb.7.1477588147898; Thu, 27 Oct 2016 10:09:07 -0700 (PDT) Return-Path: Received: from mail-wm0-x22f.google.com (mail-wm0-x22f.google.com. [2a00:1450:400c:c09::22f]) by gmr-mx.google.com with ESMTPS id h82si306943wmh.2.2016.10.27.10.09.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 27 Oct 2016 10:09:07 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::22f as permitted sender) client-ip=2a00:1450:400c:c09::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::22f as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x22f.google.com with SMTP id n67so59942015wme.1 for ; Thu, 27 Oct 2016 10:09:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=6QVMTeDyLnHHUatY22BqGicoDBI9ar9A4i8wLsK2vzw=; b=B4bjz9QLRHH9zhGdobHzIOuM4+hngokFxkgj3PAuP6vn9ecplQ16Zv0yTJ55i3JtS3 WyXZpFgHrAMplCfpktt/ElI4xHJIi9dHRDaV80Gwl9VLUW3Ny8kt2joO5te5i4c6z9Ye WNLkCcSewjKF4EOfaUIT9jAkEtERans+gAWQCdckgISXp7N/3xJB/5fFZuomQLJ8xY9I SDNDcSRc0fPIVkgIH4KVnp00qdwPS8ruNzvVhfAh2xDAqMD0JUdzmI43aJCJxr9eqLzC +mBxgJL+uayUng8iEfUpzrdakX9NgUpqKT3ipmnSV1jefAg2H5yy83Nr659awOwpvz5h pFwA== X-Gm-Message-State: ABUngvcm6jMNpb88w6bqztbKRegEBfQXeSpHttTdLAR5Ehi5nvSw9b4hN5ueE3sF0R0gfMXyDDKgzJRL847F6Q== X-Received: by 10.28.32.132 with SMTP id g126mr9458332wmg.131.1477588147655; Thu, 27 Oct 2016 10:09:07 -0700 (PDT) MIME-Version: 1.0 Received: by 10.80.151.188 with HTTP; Thu, 27 Oct 2016 10:09:07 -0700 (PDT) In-Reply-To: <73e93a79-8002-34b6-93b5-35ca6aba9628@googlemail.com> References: <058585c6-426c-a0d7-f035-9dcc2d6cda61@googlemail.com> <73e93a79-8002-34b6-93b5-35ca6aba9628@googlemail.com> From: Nicolai Kraus Date: Thu, 27 Oct 2016 18:09:07 +0100 Message-ID: Subject: Re: [HoTT] Is [Equiv Type_i Type_i] contractible? To: Martin Escardo Cc: Matthieu Sozeau , homotopytypetheory Content-Type: multipart/alternative; boundary=001a113d58b6aa5a4e053fdbcc5e --001a113d58b6aa5a4e053fdbcc5e Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 =3D A|| and ||X =3D 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=3D0 and > X=3D1 are propositions. Hence we can use excluded middle to check if any > them holds, and define f(X) accordingly. Otherwise take f(X)=3DX. > > > 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=C3=A9o Winterha= lter 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 > >> . > >> 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. > --001a113d58b6aa5a4e053fdbcc5e Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On T= hu, Oct 27, 2016 at 4:38 PM, 'Martin Escardo' via Homotopy Type The= ory <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.
In your formulation of the construction, you can swap any=20 two given types A and B, not only 0 and 1. This is because you really only = need to decide ||X =3D A|| and ||X =3D B||.
-- Nicolai

=C2=A0
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=3D0 and=
X=3D1 are propositions. Hence we can use excluded middle to check if any them holds, and define f(X) accordingly. Otherwise take f(X)=3DX.

> 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 s= hort:

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,
>>
>>=C2=A0 =C2=A0we've been stuck with N. Tabareau and his student = Th=C3=A9o 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 s= eem to
>> prove (or disprove) this from univalence alone, and even additiona= l
>> 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 mode= l?
>>
>> -- 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a113d58b6aa5a4e053fdbcc5e--