From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 27 Oct 2016 13:38:15 -0700 (PDT) From: Ulrik Buchholtz To: Homotopy Type Theory Cc: ulrikbu...@gmail.com, matthie...@inria.fr Message-Id: In-Reply-To: <20161027194440.GA826@richard> References: <9ced56b8-66bb-4f7f-996e-bbbb84c227ab@googlegroups.com> <20161027194440.GA826@richard> Subject: Re: [HoTT] Re: Is [Equiv Type_i Type_i] contractible? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_262_662137996.1477600695586" ------=_Part_262_662137996.1477600695586 Content-Type: multipart/alternative; boundary="----=_Part_263_971235406.1477600695586" ------=_Part_263_971235406.1477600695586 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Thanks, Richard! Of course, this is not directly pertaining to Matthieu, Nicolas and Th=C3= =A9o's=20 question, but it's trying to capture an intuition that a universe should be= =20 rigid, at least when considered together with some structure. How much structure suffices to make the universe rigid, and can we define= =20 this extra structure in HoTT? (We don't know how to say yet that the=20 universe can be given the structure of an infinity-category strongly=20 generated by 1, for example.) Do you know other references that pertain to the inspiring assumption/hypot= h=C3=A8se=20 inspiratrice? Best wishes, Ulrik On Thursday, October 27, 2016 at 9:44:43 PM UTC+2, Richard Williamson wrote= : > > I think the earliest proof of some version of Grothendieck's=20 > hypoth=C3=A8se inspiratrice is in the following paper of Cisinki.=20 > > http://www.tac.mta.ca/tac/volumes/20/17/20-17abs.html=20 > > It is my belief that Grothendieck's original formulation, which=20 > was for the homotopy category itself (as opposed to a lifting of=20 > it), is independent of ZFC. A proof of this would be fascinating.=20 > I have occasionally speculated about trying to use HoTT to give=20 > such an independence proof. Vladimir's comment suggests that one=20 > direction of this is already done.=20 > > Best wishes,=20 > Richard=20 > > On Thu, Oct 27, 2016 at 10:12:50AM -0700, Ulrik Buchholtz wrote:=20 > > This is (related to) Grothendieck's =E2=80=9Cinspiring assumption=E2=80= =9D of Pursuing=20 > > Stacks section 28.=20 > >=20 > > 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=20 > >=20 > > Theorem 8.12 for n=3D0 says that the Kan complex of homotopy theories o= f=20 > > (infinity,0)-categories is contractible. Of course this depends on thei= r=20 > > axiomatization, Definition 6.8. Perhaps some ideas can be adapted.=20 > >=20 > > Cheers,=20 > > Ulrik=20 > >=20 > > On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau=20 > wrote:=20 > > >=20 > > > Dear all,=20 > > >=20 > > > we've been stuck with N. Tabareau and his student Th=C3=A9o Winterh= alter=20 > on=20 > > > the above question. Is it the case that all equivalences between a=20 > universe=20 > > > and itself are equivalent to the identity? We can't seem to prove (or= =20 > > > disprove) this from univalence alone, and even additional=20 > parametricity=20 > > > assumptions do not seem to help. Did we miss a counterexample? Did=20 > anyone=20 > > > investigate this or can produce a proof as an easy corollary? What is= =20 > the=20 > > > situation in, e.g. the simplicial model?=20 > > >=20 > > > -- Matthieu=20 > > >=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeThe...@googlegroups.com .=20 > > > For more options, visit https://groups.google.com/d/optout.=20 > > ------=_Part_263_971235406.1477600695586 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Thanks, Richard!

Of course, this is not= directly pertaining to=C2=A0Matthieu, = Nicolas and Th=C3=A9o's question, but it's trying to capture an int= uition that a universe should be rigid, at least when considered together w= ith some structure.

How much= structure suffices to make the universe rigid, and can we define this extr= a structure in HoTT? (We don't know how to say yet that the universe ca= n be given the structure of an infinity-category strongly generated by 1, f= or example.)

Do you know other= references that pertain to the inspiring assumption/hypoth=C3=A8se = inspiratrice?

Best wishes,
Ulrik

On Thursday, October 27, 2016 at 9:44:43 PM UTC+2, Richard Williamso= n wrote:
I think the earliest p= roof of some version of Grothendieck's
hypoth=C3=A8se inspiratrice is in the following paper of Cisinki.

http://www.tac.mta.ca/tac/volumes/20/17/20-17abs.htm= l

It is my belief that Grothendieck's original formulation, which
was for the homotopy category itself (as opposed to a lifting of
it), is independent of ZFC. A proof of this would be fascinating.
I have occasionally speculated about trying to use HoTT to give
such an independence proof. Vladimir's comment suggests that one
direction of this is already done.

Best wishes,
Richard

On Thu, Oct 27, 2016 at 10:12:50AM -0700, Ulrik Buchholtz wrote:
> This is (related to) Grothendieck's =E2=80=9Cinspiring assumpt= ion=E2=80=9D of Pursuing
> Stacks section 28.
>
> I only know of the treatment by Barwick and Schommer-Pries in On t= he
> Unicity of the Homotopy Theory of Higher Categories:
> https://arxiv.org/abs/1112.0040
>
> Theorem 8.12 for n=3D0 says that the Kan complex of homotopy theor= ies of
> (infinity,0)-categories is contractible. Of course this 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 Sozeau= wrote:
> >
> > Dear all,
> >
> > =C2=A0 we've been stuck with N. Tabareau and his student = Th=C3=A9o Winterhalter on
> > the above question. Is it the case that all equivalences betw= een a universe
> > and itself are equivalent to the identity? We can't seem = to prove (or
> > disprove) this from univalence alone, and even additional par= ametricity
> > 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.
> For more options, visit https://groups.go= ogle.com/d/optout.

------=_Part_263_971235406.1477600695586-- ------=_Part_262_662137996.1477600695586--