From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.172.10 with SMTP id v10mr12004143vke.14.1465197309233; Mon, 06 Jun 2016 00:15:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.16.110 with SMTP id o43ls746713oto.84.gmail; Mon, 06 Jun 2016 00:15:08 -0700 (PDT) X-Received: by 10.157.37.137 with SMTP id q9mr2983325ota.6.1465197308453; Mon, 06 Jun 2016 00:15:08 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id d71si1261343ywb.3.2016.06.06.00.15.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 06 Jun 2016 00:15:08 -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 u567F2no002397 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 6 Jun 2016 03:15:02 -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 1b9okY-0000pQ-Iu; Mon, 06 Jun 2016 03:15:02 -0400 Subject: Re: [HoTT] Re: 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=_147C2996-5F27-4A4D-9B79-4987ABB7B51B"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail 2.6b2 From: Vladimir Voevodsky In-Reply-To: Date: Mon, 6 Jun 2016 10:14:59 +0300 Cc: Andrew Polonsky , Martin Escardo , Homotopy Type Theory Message-Id: <7AC24044-EDEF-4490-BC72-24885504B619@ias.edu> References: <5750A527.4060705@cs.bham.ac.uk> To: Urs Schreiber X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-06-06_04:,, 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-1606060087 X-IAS-PPS-PHISH: NO --Apple-Mail=_147C2996-5F27-4A4D-9B79-4987ABB7B51B Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 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)-category. Vladimir. > On Jun 4, 2016, at 9:11 AM, Urs Schreiber wrot= e: >=20 >> They don=E2=80=99t take us seriously so far because we can not define >> (infty,1)-categories. >=20 > 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. >=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) 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". >=20 > 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. >=20 > 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. >=20 > 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. >=20 > 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. >=20 > 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. >=20 > Best wishes, > urs --Apple-Mail=_147C2996-5F27-4A4D-9B79-4987ABB7B51B 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 iQEcBAEBCgAGBQJXVSL0AAoJEH5eMY79Hy7tlPMIAITgsv1YhrJjlcbmV/r6hXod B7DEbjEyFD2HzX7SV9wLPh5iSABLI3ApnMfg3D83SYadjL0R1IB4JrAv9hki7QOu lQZ5pBC+Sr5h9Mb3YcZ/2NzT8ROm5QKE9d9IiNjyuO7HcyaFCL3Mw5wsR7qBcwzn B3U9Z1Fbvms3AWol4zm6eO1JvY2i4jNne89JUNsuTOcfsaWIoM2DjxrKK08ptpbD eCGjaGumUta1+lz+6KUhcH4EKwLPNqscpTqXQyKytT5DP4x3y2RSLZcyYORC+hev jOmeJVMRn1r+35HS3X7OdDwJd6uEbQVs+O4KZYzg4/nXGDgfyFBsnvA7TvRaeqA= =4xyK -----END PGP SIGNATURE----- --Apple-Mail=_147C2996-5F27-4A4D-9B79-4987ABB7B51B--