From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.39.131 with SMTP id g125mr958684ita.7.1464982154275; Fri, 03 Jun 2016 12:29:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.104.212 with SMTP id a78ls1384286qgf.9.gmail; Fri, 03 Jun 2016 12:29:13 -0700 (PDT) X-Received: by 10.237.49.134 with SMTP id 6mr3841183qth.20.1464982153794; Fri, 03 Jun 2016 12:29:13 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id u2si495266ywf.6.2016.06.03.12.29.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 03 Jun 2016 12:29:13 -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 u53JT82W006649 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Fri, 3 Jun 2016 15:29:08 -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 1b8umK-0001QU-AS; Fri, 03 Jun 2016 15:29:08 -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=_1136A7DD-68AC-4EA2-9526-05C3F59F3ACB"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail 2.6b2 From: Vladimir Voevodsky In-Reply-To: Date: Fri, 3 Jun 2016 22:29:05 +0300 Cc: Martin Escardo , Homotopy Type Theory Message-Id: References: <5750A527.4060705@cs.bham.ac.uk> To: Andrew Polonsky X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-06-03_10:,, 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-1606030213 X-IAS-PPS-PHISH: NO --Apple-Mail=_1136A7DD-68AC-4EA2-9526-05C3F59F3ACB Content-Type: multipart/alternative; boundary="Apple-Mail=_EE429F7F-FA55-4AA0-BCEC-EE7DFC9DC1B4" --Apple-Mail=_EE429F7F-FA55-4AA0-BCEC-EE7DFC9DC1B4 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Certainly not to the synthetic homotopy theory branch with which we communi= cate all the time. I refer to mathematicians who do not know type theory and want to have a co= nvenient language of working with what we would call structures on types of= higher h-level. For example, there are people like that in the geometric representation the= ory. They don=E2=80=99t take us seriously so far because we can not define (inft= y,1)-categories. As soon as we find a language that can be used to define t= hem and work with them directly without going through sets they will all st= art to turn their heads in our direction. And this is a necessary pre-condition for talking seriously about the UF as= a new foundation of mathematics. Vladimir. > On Jun 3, 2016, at 5:12 PM, Andrew Polonsky wrote: >=20 > Dear Vladimir, >=20 > We are also isolated from many and many mathematicians who are trying to = find a way to express ideas that in my opinion are most naturally expressed= in the UF in various theories formulated inside the set theory. >=20 > In this paragraph, are you referring to what Martin called "synthetic hom= otopy theory/infinity-toposes" branch of the HoTT community, or to a dispar= ate body of mathematical research with different objectives? >=20 > Greetings, > Andrew --Apple-Mail=_EE429F7F-FA55-4AA0-BCEC-EE7DFC9DC1B4 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Certainly not to t= he synthetic homotopy theory branch with which we communicate all the time.=

I refer to mathematici= ans who do not know type theory and want to have a convenient language of w= orking with what we would call structures on types of higher h-level. =

For example, the= re are people like that in the geometric representation theory. 
=

They don=E2=80=99t tak= e us seriously so far because we can not define (infty,1)-categories. As so= on as we find a language that can be used to define them and work with them= directly without going through sets they will all start to turn their head= s in our direction.

And this is a necessary pre-condition for talking seriously about the UF= as a new foundation of mathematics. 

Vladimir.

<= /div>




On Jun 3, 2016, at 5= :12 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

Dear Vladimir,

We are also isolated from many and many mathematici= ans who are trying to find a way to express ideas that in my opinion are mo= st naturally expressed in the UF in various theories formulated inside the = set theory.

In this paragraph, are you referring to what Martin called "s= ynthetic homotopy theory/infinity-toposes" branch of the HoTT community, or= to a disparate body of mathematical research with different objectives?

Greetings,
Andrew

--Apple-Mail=_EE429F7F-FA55-4AA0-BCEC-EE7DFC9DC1B4-- --Apple-Mail=_1136A7DD-68AC-4EA2-9526-05C3F59F3ACB 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 iQEcBAEBCgAGBQJXUdqCAAoJEH5eMY79Hy7t/34IAIxGBJR41DR7AZCZNlv1a/EM OBFHdKAcEgU1ep+Sd4hb08eReBbliD0iTHIJ29LXbRy3uR3jJPStnZdJkyyHKMwq cSBG8Q9tu00s6SP55F4sWML08k702DYSgINVgjzE3WBY4Y1ZPvpkPMhEOmRDhCRI 7/2OyZM/jllSzcbbukNHkFjbD7HH6grC4vx3hI9w9HBgwrD8uQxia1r1bbl4kYQZ T38StsQU2to9Ul6ZPkqWqh3DcgKpaqgADwK0tMTL/Dw5bJxtrYrmCAF4V6VXg5tq um1qD1U9EtqSN7K/5Q/cah0Du1l6VhPOSxXLHbwv6fAhPEO7kgiJ47SjiIXMQiE= =ijZx -----END PGP SIGNATURE----- --Apple-Mail=_1136A7DD-68AC-4EA2-9526-05C3F59F3ACB--