From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.41.16 with SMTP id p16mr2038893lfp.3.1477908059307; Mon, 31 Oct 2016 03:00:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.22.160 with SMTP id 32ls247928lfw.31.gmail; Mon, 31 Oct 2016 03:00:58 -0700 (PDT) X-Received: by 10.25.22.104 with SMTP id m101mr2046694lfi.2.1477908058244; Mon, 31 Oct 2016 03:00:58 -0700 (PDT) Return-Path: Received: from mail-wm0-x243.google.com (mail-wm0-x243.google.com. [2a00:1450:400c:c09::243]) by gmr-mx.google.com with ESMTPS id y7si1645232wme.0.2016.10.31.03.00.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 31 Oct 2016 03:00:58 -0700 (PDT) Received-SPF: pass (google.com: domain of ericf...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) client-ip=2a00:1450:400c:c09::243; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of ericf...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) smtp.mailfrom=ericf...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x243.google.com with SMTP id m83so17625728wmc.0 for ; Mon, 31 Oct 2016 03:00:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=FWsA69LkT89UV/s+CqnyzRyECLPQH3cHhLXQtNg52Bc=; b=ZbxGIlhhb7EqSyUi4JwWiJ+kbaUGC3s3caiGkLjb1pmd5KGnuHqCFi2iYG/LzVqUnU +LinZe7kbvwFvOB9blqOaFGGDIlrGqBgBcp6xQi2Rpi8GX95s7zj5It33xEiQR/Q2BOf rj7cGdnUScxh8THQdtX6trMB/pgngyJCF5LhLPak3SehRsWPOLIo1F+llPGqY2DOKZY3 COgAW2lHDuvMJ8sp6q7jauwBbguuHgIfosguon8f13CRUTEtasUkL+xTWOTI+NjUp/Ap B7hofKdpc7MYczRH2RsjagjXBikJ9zdqsCXW8FUC7fRzE9Wp0m9ApMoeFzxBqg+3VP0B YPFA== X-Gm-Message-State: ABUngvfNNPOP/mzk6veUctqq5pK/fif1dUmzzKvOJmGkpvutExKPTuDRG3eFjOpIVdOLhpO2CcaadQ9Z2P6/OA== X-Received: by 10.194.105.41 with SMTP id gj9mr26359624wjb.58.1477908057955; Mon, 31 Oct 2016 03:00:57 -0700 (PDT) MIME-Version: 1.0 References: <9ced56b8-66bb-4f7f-996e-bbbb84c227ab@googlegroups.com> <20161027194440.GA826@richard> <20161030205656.GA1487@richard> In-Reply-To: <20161030205656.GA1487@richard> From: Eric Finster Date: Mon, 31 Oct 2016 10:00:47 +0000 Message-ID: Subject: Re: [HoTT] Re: Is [Equiv Type_i Type_i] contractible? To: Richard Williamson , Ulrik Buchholtz Cc: Homotopy Type Theory , matthie...@inria.fr Content-Type: multipart/alternative; boundary=001a1130cd26ce24c1054026480b --001a1130cd26ce24c1054026480b Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Just wanted to mention quickly for those who are interested in this kind of thing that a similar statement for the *stable* homotopy category is a theorem of Stefan Schwede's: http://www.math.uni-bonn.de/people/schwede/rigid.pdf Eric On Sun, Oct 30, 2016 at 9:57 PM Richard Williamson wrote: > Hi Ulrik, > > I mis-remembered the history a little: Corollary 5.2.2 of the > following paper of To=C3=ABn and Vezzozi, from 2002, also gives a > proof of a lifting of the hypoth=C3=A8se inspiratrice. > > https://arxiv.org/abs/math/0212330 > > As one would expect, the paper 'La th=C3=A9orie de l'homotopie de > Grothendieck' of Maltsiniotis also briefly discusses the original > hypoth=C3=A8se inspiratrice, early on in the introduction (see especially > the footnote). > > I don't think that I know of other direct references beyond these, > except possibly in other writings of these authors; though the > quasi-categorical literature also, as one would expect, has a proof of > the same theorem as in the papers of Cisinski and To=C3=ABn-Vezzosi. > > I think that the Cisinski's paper gives a very clear reason to > expect the result to be true when formulated in the language of a > sufficiently rich 'homotopical category theory', whether the > language be that of derivators, (=E2=88=9E,1)-categories, or whatever. > > It is remarkable that the result can be proven relatively easily > when formulated in a certain language, but if one insists on the > original version at the level of homotopy categories, then there seems > to be no way to approach it. This is the aspect of the hypothesis that > I am most interested in. A proof that the original hypothesis is > independent of ZFC would no doubt shed some very interesting light on > this dichotomy. > > Best wishes, > Richard > > On Thu, Oct 27, 2016 at 01:38:15PM -0700, Ulrik Buchholtz wrote: > > Thanks, Richard! > > > > Of course, this is not directly pertaining to Matthieu, Nicolas and > Th=C3=A9o's > > question, but it's trying to capture an intuition that a universe shoul= d > be > > rigid, at least when considered together with some structure. > > > > How much structure suffices to make the universe rigid, and can we defi= ne > > this extra structure in HoTT? (We don't know how to say yet that the > > universe can be given the structure of an infinity-category strongly > > generated by 1, for 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 Williamson > wrote: > > > > > > I think the earliest proof 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.html > > > > > > 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 assumption= =E2=80=9D of > Pursuing > > > > Stacks section 28. > > > > > > > > I only know of the treatment by Barwick and Schommer-Pries in On th= e > > > > 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 theori= es > 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, > > > > > > > > > > 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 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? Di= d > > > anyone > > > > > investigate this or can produce a proof as an easy corollary? Wha= t > 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. > > -- > 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. > --001a1130cd26ce24c1054026480b Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Just wanted to mention quickly for those who are intereste= d in this kind of thing that a similar statement for the *stable* homotopy = category is a theorem of Stefan Schwede's:


Eric


On= Sun, Oct 30, 2016 at 9:57 PM Richard Williamson <rwilli...@gmail.com> wrote:
Hi Ulrik,

I mis-remembered the history a little: Corollary 5.2.2 of the
following paper of To=C3=ABn and Vezzozi, from 2002, also gives a
proof of a lifting of the hypoth=C3=A8se inspiratrice.

https://arxiv.org/abs/math/0212330

As one would expect, the paper 'La th=C3=A9orie de l'homotopie de Grothendieck' of Maltsiniotis also briefly discusses the original
hypoth=C3=A8se inspiratrice, early on in the introduction (see especially the footnote).

I don't think that I know of other direct references beyond these,
except possibly in other writings of these authors; though the
quasi-categorical literature also, as one would expect, has a proof of
the same theorem as in the papers of Cisinski and To=C3=ABn-Vezzosi.

I think that the Cisinski's paper gives a very clear reason to
expect the result to be true when formulated in the language of a
sufficiently rich 'homotopical category theory', whether the
language be that of derivators, (=E2=88=9E,1)-categories, or whatever.

It is remarkable that the result can be proven relatively easily
when formulated in a certain language, but if one insists on the
original version at the level of homotopy categories, then there seems
to be no way to approach it. This is the aspect of the hypothesis that
I am most interested in. A proof that the original hypothesis is
independent of ZFC would no doubt shed some very interesting light on
this dichotomy.

Best wishes,
Richard

On Thu, Oct 27, 2016 at 01:38:15PM -0700, Ulrik Buchholtz wrote:
> Thanks, Richard!
>
> Of course, this is not directly pertaining to Matthieu, Nicolas and Th= =C3=A9o's
> question, but it's trying to capture an intuition that a universe = should be
> rigid, at least when considered together with some structure.
>
> How much structure suffices to make the universe rigid, and can we def= ine
> this extra structure in HoTT? (We don't know how to say yet that t= he
> universe can be given the structure of an infinity-category strongly > generated by 1, for 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 Williamson = wrote:
> >
> > I think the earliest proof of some version of Grothendieck's<= br class=3D"gmail_msg"> > > hypoth=C3=A8se inspiratrice is in the following paper of Cisinki.=
> >
> > http://www.tac.mt= a.ca/tac/volumes/20/17/20-17abs.html
> >
> > It is my belief that Grothendieck's original formulation, whi= ch
> > was for the homotopy category itself (as opposed to a lifting of<= br class=3D"gmail_msg"> > > 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:<= br class=3D"gmail_msg"> > > > This is (related to) Grothendieck's =E2=80=9Cinspiring a= ssumption=E2=80=9D of Pursuing
> > > Stacks section 28.
> > >
> > > I only know of the treatment by Barwick and Schommer-Pries i= n On the
> > > 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= theories of
> > > (infinity,0)-categories is contractible. Of course this depe= nds on their
> > > axiomatization, Definition 6.8. Perhaps some ideas can be ad= apted.
> > >
> > > Cheers,
> > > Ulrik
> > >
> > > On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu = Sozeau
> > wrote:
> > > >
> > > > Dear all,
> > > >
> > > >=C2=A0 =C2=A0we've been stuck with N. Tabareau and h= is student Th=C3=A9o Winterhalter
> > on
> > > > the above question. Is it the case that all equivalence= s between a
> > universe
> > > > and itself are equivalent to the identity? We can't= seem to prove (or
> > > > disprove) this from univalence alone, and even addition= al
> > parametricity
> > > > assumptions do not seem to help. Did we miss a countere= xample? Did
> > anyone
> > > > investigate this or can produce a proof as an easy coro= llary? 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 fro= m it, send
> > an email to HomotopyTypeThe...@googlegroups.co= m <javascript:>.
> >
> > > For more options, visit https:/= /groups.google.com/d/optout.
> >
> >
>
> --
> You received this message because you are subscribed to the Google Gro= ups "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.go= ogle.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 HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google= .com/d/optout.
--001a1130cd26ce24c1054026480b--