From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.202.135 with SMTP id a129mr10918871iog.33.1465210580672; Mon, 06 Jun 2016 03:56:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.88.211 with SMTP id t77ls2362041qgd.86.gmail; Mon, 06 Jun 2016 03:56:20 -0700 (PDT) X-Received: by 10.159.33.173 with SMTP id 42mr868942uac.2.1465210580075; Mon, 06 Jun 2016 03:56:20 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id u2si1152180ywf.6.2016.06.06.03.56.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 06 Jun 2016 03:56:19 -0700 (PDT) Received-SPF: pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) client-ip=192.16.204.88; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) smtp.mailfrom=vlad...@ias.edu; dmarc=pass (p=NONE dis=NONE) header.from=ias.edu Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu (8.15.0.59/8.15.0.59) with ESMTPS id u56AuE9k018564 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 6 Jun 2016 06:56:14 -0400 Received: from ppp91-78-240-175.pppoe.mtu-net.ru ([91.78.240.175] helo=[192.168.100.3]) by imap.math.ias.edu with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.80.1) (envelope-from ) id 1b9sCc-0003ra-22; Mon, 06 Jun 2016 06:56:14 -0400 Subject: Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory? Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: multipart/signed; boundary="Apple-Mail=_8DCAE3B2-2165-4463-B7E8-74A1DE9B43E0"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail 2.6b2 From: Vladimir Voevodsky In-Reply-To: Date: Mon, 6 Jun 2016 13:56:11 +0300 Cc: homotopytypetheory , Urs Schreiber , Martin Escardo , Andrew Polonsky Message-Id: <876863B3-A791-466D-B4AA-D321CF5867E7@ias.edu> References: <5750A527.4060705@cs.bham.ac.uk> <7AC24044-EDEF-4490-BC72-24885504B619@ias.edu> To: David Roberts X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-06-06_05:,, signatures=0 X-Proofpoint-Spam-Reason: safe X-IAS-PPS-SPAM: NO X-Proofpoint-Spam-Details: rule=ias_safe policy=ias score=0 spamscore=0 malwarescore=0 suspectscore=0 phishscore=0 bulkscore=0 adultscore=0 classifier=donotscan adjust=0 reason=safe scancount=1 engine=8.0.1-1604210000 definitions=main-1606060131 X-IAS-PPS-PHISH: NO --Apple-Mail=_8DCAE3B2-2165-4463-B7E8-74A1DE9B43E0 Content-Type: multipart/alternative; boundary="Apple-Mail=_3F103027-8C92-4C27-AC93-9DF8E8A50D46" --Apple-Mail=_3F103027-8C92-4C27-AC93-9DF8E8A50D46 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 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 intent= ionally 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 *so= me* 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 in= cludes 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: >=20 > Dear Vladimir, >=20 > Please see Charles Rezk's work on globally equivariant homotopy theoretic= models of cohesion. It is not something out of Urs' imagination. >=20 > Also, if something is false, call it false, not a 'lie', and provide a ma= thematical basis for such a statement. >=20 > Best regards, > David >=20 > On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky" > wrote: > Dear Urs, >=20 > > 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) >=20 > this is a lie. >=20 > Geometric representation theorists care about the (infty,1)-categories th= at corresponds to different groups and to their interaction with each other= . They care not about sitting inside one universal (infty,1)-category. >=20 > Vladimir. >=20 >=20 >=20 >=20 >=20 > > 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 >=20 > -- > 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 . >=20 > -- > 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 . --Apple-Mail=_3F103027-8C92-4C27-AC93-9DF8E8A50D46 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 When one gives a f= alse mathematical statement I can call it 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.&nb= sp;

I did not not= ice that the statement was about *a* class of categories. 

It might be the case that ge= ometric representation theorists care about *some* class of (infty,1)-categ= ories that can be obtained by adding "a certain adjoint triple of modal ope= rators=E2=80=9D to HoTT (whatever that means). 
<= br class=3D"">
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 <drobert...@gmail.com> w= rote:

Dear Vladimir,

Please see = Charles Rezk's work on globally equivariant homotopy theoretic models of co= hesion. It is not something out of Urs' imagination.

Also, if something is false, call it false, not a 'lie', and provid= e a mathematical basis for such a statement.

B= est regards,
David

On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky" <= vlad...@ias.edu> wrote= :
Dear Ur= s,

> 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> wrote:
>
>> 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 class=3D""> > 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 class=3D""> > mostly meant by "geometric representation theory".
>
> This route is the homotopy version of Lawvere's seminal vision of all<= br class=3D""> > 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 class=3D""> > 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 class=3D""> > 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 class=3D""> > 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 "= 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/op= tout.

<= /div> --
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 e= mail to H= omotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_3F103027-8C92-4C27-AC93-9DF8E8A50D46-- --Apple-Mail=_8DCAE3B2-2165-4463-B7E8-74A1DE9B43E0 Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature; name=signature.asc Content-Description: Message signed with OpenPGP using GPGMail -----BEGIN PGP SIGNATURE----- Comment: GPGTools - https://gpgtools.org iQEcBAEBCgAGBQJXVVbLAAoJEH5eMY79Hy7ttTcIAMm7Jn3byVnq57TuqOta7d6u pUfv/k+eqgnsIOWmZbyuN6xK2M1c94q2HuJVjDnpQyHn2oonXlnjhy0OTab0bojL C9GSPBSm3ygWHxRHZoKzaILvVvmfMyPEVzKoJS8O23m0wNC1nqc53V8py58mORzu Z07L51gk9oFC7hXcnxZ+wtTIXkaaygGqlYG3ALisgFtrHxODqAFp1X+ZeLpQwid8 FF65rC8QUipxeH6j0nG5NIYSin0Oz9E+YhQD5vsj+dqgF1v550Pt2A/MRML146ZI VI7xJJ2aRjgKKj/IDdnUEcmsKcEhagptYfafMUi1LSOD8A7ULD/GAlJPKP9UyVw= =wLky -----END PGP SIGNATURE----- --Apple-Mail=_8DCAE3B2-2165-4463-B7E8-74A1DE9B43E0--