From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 27 Oct 2016 10:12:50 -0700 (PDT) From: Ulrik Buchholtz To: Homotopy Type Theory Cc: homotopyt...@googlegroups.com, matthie...@inria.fr Message-Id: <9ced56b8-66bb-4f7f-996e-bbbb84c227ab@googlegroups.com> In-Reply-To: References: Subject: Re: Is [Equiv Type_i Type_i] contractible? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_191_1897780265.1477588370336" ------=_Part_191_1897780265.1477588370336 Content-Type: multipart/alternative; boundary="----=_Part_192_1574491679.1477588370337" ------=_Part_192_1574491679.1477588370337 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable This is (related to) Grothendieck's =E2=80=9Cinspiring assumption=E2=80=9D = of Pursuing=20 Stacks section 28. I only know of the treatment by Barwick and Schommer-Pries in On the=20 Unicity of the Homotopy Theory of Higher Categories:=20 https://arxiv.org/abs/1112.0040 Theorem 8.12 for n=3D0 says that the Kan complex of homotopy theories of=20 (infinity,0)-categories is contractible. Of course this depends on their=20 axiomatization, Definition 6.8. Perhaps some ideas can be adapted. Cheers, Ulrik On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau wrote: > > Dear all, > > we've been stuck with N. Tabareau and his student Th=C3=A9o Winterhalte= r on=20 > the above question. Is it the case that all equivalences between a univer= se=20 > and itself are equivalent to the identity? We can't seem to prove (or=20 > disprove) this from univalence alone, and even additional parametricity= =20 > assumptions do not seem to help. Did we miss a counterexample? Did anyone= =20 > investigate this or can produce a proof as an easy corollary? What is the= =20 > situation in, e.g. the simplicial model? > > -- Matthieu > ------=_Part_192_1574491679.1477588370337 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
This is (related to) Grothendieck's =E2=80=9Cinspiring= assumption=E2=80=9D of Pursuing Stacks section 28.

I on= ly know of the treatment by Barwick and Schommer-Pries in On the Unicity of= the Homotopy Theory of Higher Categories: https://arxiv.org/abs/1112.0040<= /div>

Theorem 8.12 for n=3D0 says that the Kan complex o= f homotopy theories of (infinity,0)-categories is contractible. Of course t= his depends on their axiomatization, Definition 6.8. Perhaps some ideas can= be adapted.

Cheers,
Ulrik
On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Soz= eau wrote:
Dear all,

=C2= =A0 we've been stuck with N. Tabareau and his student Th=C3=A9o Winterh= alter 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 p= rove (or disprove) this from univalence alone, and even additional parametr= icity assumptions do not seem to help. Did we miss a counterexample? Did an= yone investigate this or can produce a proof as an easy corollary? What is = the situation in, e.g. the simplicial model?

-- Matth= ieu
------=_Part_192_1574491679.1477588370337-- ------=_Part_191_1897780265.1477588370336--