From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.53.185 with SMTP id c54mr12818742qte.11.1465213238722; Mon, 06 Jun 2016 04:40:38 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.130.147 with SMTP id m19ls1047064ioi.69.gmail; Mon, 06 Jun 2016 04:40:38 -0700 (PDT) X-Received: by 10.107.146.67 with SMTP id u64mr975054iod.29.1465213238163; Mon, 06 Jun 2016 04:40:38 -0700 (PDT) Return-Path: Received: from mail-io0-x22a.google.com (mail-io0-x22a.google.com. [2607:f8b0:4001:c06::22a]) by gmr-mx.google.com with ESMTPS id p189si695836itc.1.2016.06.06.04.40.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 06 Jun 2016 04:40:38 -0700 (PDT) Received-SPF: pass (google.com: domain of drobert...@gmail.com designates 2607:f8b0:4001:c06::22a as permitted sender) client-ip=2607:f8b0:4001:c06::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of drobert...@gmail.com designates 2607:f8b0:4001:c06::22a as permitted sender) smtp.mailfrom=drobert...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-io0-x22a.google.com with SMTP id 5so14004119ioy.1 for ; Mon, 06 Jun 2016 04:40:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc; bh=+nfkWcWTCGF1NFbg4JcGRqHKXdUj+IneMxgFbLBINcU=; b=XlAJSw8HpFvas33KOc45CyWiaS+S1Ip8/jc65SgwUSqPziRVgIZwodDaclRsA9ChJL UxGVM11JMURY78HeTlMg6FH7hI917uDP8YkzIbdhTwBDxk2sMxpZKfU6eiKI0JpGPDR9 cFfkTQvu1VFfr8Vey7yjgNMRsiEu+HSDnQNS3Y3wnnB7HzizDxvnSlq5pJkLBTXrQeUQ cONWQTADaBMG0bSm1/pIAHeY32uexzATmqzI+Up5X5eZHOkHFWcLl2eg11j3Bi7Jc8AH x0P9ViFu1jfjQte+rbNc93CApizHqnrCpAxU0RIUeI8HI291dJUE86HQx8Uz+2ayus5n 73Tw== X-Gm-Message-State: ALyK8tLT5o+u/kdfKZflVj1bvqU7KFHQyQwNiSFy5WItHoqAKutdvSaDL+ArDltnERq756mN39YQbTX9I6dvKw== MIME-Version: 1.0 X-Received: by 10.107.163.211 with SMTP id m202mr19989057ioe.79.1465213237879; Mon, 06 Jun 2016 04:40:37 -0700 (PDT) Received: by 10.107.26.68 with HTTP; Mon, 6 Jun 2016 04:40:36 -0700 (PDT) Received: by 10.107.26.68 with HTTP; Mon, 6 Jun 2016 04:40:36 -0700 (PDT) In-Reply-To: <876863B3-A791-466D-B4AA-D321CF5867E7@ias.edu> References: <5750A527.4060705@cs.bham.ac.uk> <7AC24044-EDEF-4490-BC72-24885504B619@ias.edu> <876863B3-A791-466D-B4AA-D321CF5867E7@ias.edu> Date: Mon, 6 Jun 2016 21:10:36 +0930 Message-ID: Subject: Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory? From: David Roberts To: Vladimir Voevodsky Cc: Urs Schreiber , Martin Escardo , homotopytypetheory , Andrew Polonsky Content-Type: multipart/alternative; boundary=001a1140ff7a906ad305349a8ab3 --001a1140ff7a906ad305349a8ab3 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hi again, I should have provided a reference to Rezk's paper -- here is an nLab page with a link and context: https://ncatlab.org/nlab/show/Global+Homotopy+Theory+and+Cohesion Some of the ideas go back to Henriques-Gepner, and before that Elmendorf and presumably others, but I'm not intimately familiar with the history. So they are not plucked from the air, but fit into a more recent framework with an explicitly \infty-topos-theoretic slant. That's all I can say for now. Best regards, David On 6 Jun 2016 8:26 pm, "Vladimir Voevodsky" wrote: > When one gives a false mathematical statement I can call it false. > > When the statement itself is not mathematical and I believe it to be > intentionally misleading I call it a lie. In this particular case it is > possible that I was wrong, in which case I apologize. > > I did not notice that the statement was about *a* class of categories. > > It might be the case that geometric representation theorists care about > *some* class of (infty,1)-categories that can be obtained by adding "a > certain adjoint triple of modal operators=E2=80=9D to HoTT (whatever that= means). > > In any case the sentence in question is not a mathematical statement and > includes a reference to whether or not a certain group of people cares > about something. > > Vladimir. > > > On Jun 6, 2016, at 10:32 AM, David Roberts > wrote: > > Dear Vladimir, > > Please see Charles Rezk's work on globally equivariant homotopy theoretic > models of cohesion. It is not something out of Urs' imagination. > > Also, if something is false, call it false, not a 'lie', and provide a > mathematical basis for such a statement. > > Best regards, > David > On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky" wrote: > >> Dear Urs, >> >> > For instance a class of (infinity,1)-categories that geometric >> > representation theorists care about is neatly obtained in HoTT by just >> > adding a certain adjoint triple of modal operators (differential >> > cohesion) >> >> this is a lie. >> >> Geometric representation theorists care about the (infty,1)-categories >> that corresponds to different groups and to their interaction with each >> other. They care not about sitting inside one universal (infty,1)-catego= ry. >> >> Vladimir. >> >> >> >> >> >> > On Jun 4, 2016, at 9:11 AM, Urs Schreiber >> wrote: >> > >> >> They don=E2=80=99t take us seriously so far because we can not define >> >> (infty,1)-categories. >> > >> > The good news is, without even having to define them, HoTT already is >> > the internal language of certain (infinity,1)-categories. Which ones >> > precisely depends on which axioms are added or omitted. >> > >> > For instance a class of (infinity,1)-categories that geometric >> > representation theorists care about is neatly obtained in HoTT by just >> > adding a certain adjoint triple of modal operators (differential >> > cohesion) This yields a synthetic axiomatization of the homotopy >> > theory of D-modules and their representation theory, which is what is >> > mostly meant by "geometric representation theory". >> > >> > This route is the homotopy version of Lawvere's seminal vision of all >> > mathematics taking place synthetically inside a suitable elementary >> > topos. It's slightly ironic that this route is not more popular. >> > Because over in the community of ordinary (i.e. non-type theoretic) >> > infinity-category theory, there is the nagging feeling that handling >> > all those incarnations of infinity categories as simplicial and n-fold >> > simplicial objects from the outside may be rather inefficient for >> > deriving results. In order to overcome this there is the work on >> > derivators and the work by Riehl-Verity. >> > >> > A colleague of mine championing derivators praises the fact that they >> > offer him a formal way to verify the simplicial reasoning in work by >> > Lurie et al, which he finds intricate to the point of being >> > unverifiable to him. This certainly applies to other people, too. >> > >> > To check this, you should do a survey among your colleagues whether or >> > not they think that Lurie actually gave a proof of the cobordism >> > hypothesis. Lurie gives an intriciate argument in terms of >> > infinity-categories modeled on simplicial set, and while I fully trust >> > that it is correct, it is true that it gets to the point of compexity >> > where it seems that checking the proof is not just a matter of >> > mchanically checking derivation steps, but requires extra ingenuity. >> > >> > Now, HoTT, regarded as an internal language, shares with the concept >> > of derivators the potential to make much of this somewhat >> > messy-looking simplicial infinity-category theory become more >> > transparent and systematic, more mechanical. Therefore it might be >> > argued to be a little be backwards to try to force that messy >> > simplicial technology to realize itself inside HoTT. It might be >> > missing the golden opportunity to turn this around and use the >> > synthetic reasong. >> > >> > There is now one person, Felix Wellen, working on formalizing some >> > first basics of geometric representation theory within differentially >> > cohesion HoTT. I think it's a topic with plenty of opportunity. >> > >> > Best wishes, >> > urs >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> 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. > > > --001a1140ff7a906ad305349a8ab3 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

Hi again,

I should have provided a reference to Rezk's paper -- he= re is an nLab page with a link and context:

https://ncatlab.org/nlab/show/Global+Homotopy+Theory+and+= Cohesion

Some of the ideas go back to Henriques-Gepner, and before th= at Elmendorf and presumably others, but I'm not intimately familiar wit= h the history. So they are not plucked from the air, but fit into a more re= cent framework with an explicitly \infty-topos-theoretic slant. That's = all I can say for now.

Best regards,
David

On 6 Jun 2016 8:26 pm, "Vladimir Voevodsky&= quot; <vlad...@ias.edu> wrote:=
When one gives a false mathematical statement I can call i= t false.

When the statement itself is not mathematical a= nd I believe it to be intentionally misleading I call it a lie. In this par= ticular case it is possible that I was wrong, in which case I apologize.=C2= =A0

I did not notice that the statement was about = *a* class of categories.=C2=A0

It might be the cas= e that geometric representation theorists care about *some* class of (infty= ,1)-categories that can be obtained by adding "a certain adjoint tripl= e of modal operators=E2=80=9D to HoTT (whatever that means).=C2=A0

In any case the sentence in question is not a mathematical= statement and includes a reference to whether or not a certain group of pe= ople cares about something.

Vladimir.

On Jun 6, 2016, at 10:= 32 AM, David Roberts <drobert...@gmail.com> wrote:

De= ar Vladimir,

Please see Charles Rezk's work on global= ly equivariant homotopy theoretic models of cohesion. It is not something o= ut of Urs' imagination.

Also, if something is false,= call it false, not a 'lie', and provide a mathematical basis for s= uch a statement.

Best regards,
David

On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky&= quot; <vlad...@ias.= edu> wrote:
D= ear Urs,

> For instance a class of (infinity,1)-categories that geometric
> representation theorists care about is neatly obtained in HoTT by just=
> adding a certain adjoint triple of modal operators (differential
> cohesion)

this is a lie.

Geometric representation theorists care about the (infty,1)-categories that= corresponds to different groups and to their interaction with each other. = They care not about sitting inside one universal (infty,1)-category.

Vladimir.





> On Jun 4, 2016, at 9:11 AM, Urs Schreiber <urs.sc...@googlemail.com> wrot= e:
>
>> They don=E2=80=99t take us seriously so far because we can not def= ine
>> (infty,1)-categories.
>
> The good news is, without even having to define them, HoTT already is<= br> > the internal language of certain (infinity,1)-categories. Which ones > precisely depends on which axioms are added or omitted.
>
> For instance a class of (infinity,1)-categories that geometric
> representation theorists care about is neatly obtained in HoTT by just=
> adding a certain adjoint triple of modal operators (differential
> cohesion) This yields a synthetic axiomatization of the homotopy
> theory of D-modules and their representation theory, which is what is<= br> > mostly meant by "geometric representation theory".
>
> This route is the homotopy version of Lawvere's seminal vision of = all
> mathematics taking place synthetically inside a suitable elementary > topos. It's slightly ironic that this route is not more popular. > Because over in the community of ordinary (i.e. non-type theoretic) > infinity-category theory, there is the nagging feeling that handling > all those incarnations of infinity categories as simplicial and n-fold=
> simplicial objects from the outside may be rather inefficient for
> deriving results. In order to overcome this there is the work on
> derivators and the work by Riehl-Verity.
>
> A colleague of mine championing derivators praises the fact that they<= br> > offer him a formal way to verify the simplicial reasoning in work by > Lurie et al, which he finds intricate to the point of being
> unverifiable to him. This certainly applies to other people, too.
>
> To check this, you should do a survey among your colleagues whether or=
> not they think that Lurie actually gave a proof of the cobordism
> hypothesis. Lurie gives an intriciate argument in terms of
> infinity-categories modeled on simplicial set, and while I fully trust=
> that it is correct, it is true that it gets to the point of compexity<= br> > where it seems that checking the proof is not just a matter of
> mchanically checking derivation steps, but requires extra ingenuity. >
> Now, HoTT, regarded as an internal language, shares with the concept > of derivators the potential to make much of this somewhat
> messy-looking simplicial infinity-category theory become more
> transparent and systematic, more mechanical. Therefore it might be
> argued to be a little be backwards to try to force that messy
> simplicial technology to realize itself inside HoTT. It might be
> missing the golden opportunity to turn this around and use the
> synthetic reasong.
>
> There is now one person, Felix Wellen, working on formalizing some
> first basics of geometric representation theory within differentially<= br> > cohesion HoTT. I think it's a topic with plenty of opportunity. >
> Best wishes,
> urs

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

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

--001a1140ff7a906ad305349a8ab3--