From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.140.20.14 with SMTP id 14mr5459362qgi.7.1465029529403; Sat, 04 Jun 2016 01:38:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.99.50 with SMTP id p47ls1551410qge.35.gmail; Sat, 04 Jun 2016 01:38:48 -0700 (PDT) X-Received: by 10.159.37.72 with SMTP id 66mr5556826uaz.9.1465029528893; Sat, 04 Jun 2016 01:38:48 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id d71si732011ywb.3.2016.06.04.01.38.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 04 Jun 2016 01:38:48 -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 u548chjn000448 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Sat, 4 Jun 2016 04:38:43 -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 1b976R-0003uM-BR; Sat, 04 Jun 2016 04:38:43 -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=_99D453B5-DA99-4421-8118-613F763DC7A3"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail 2.6b2 From: Vladimir Voevodsky In-Reply-To: Date: Sat, 4 Jun 2016 11:38:40 +0300 Cc: Andrew Polonsky , Martin Escardo , Homotopy Type Theory Message-Id: References: <5750A527.4060705@cs.bham.ac.uk> To: =?utf-8?Q?andr=C3=A9_hirschowitz?= X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-06-04_03:,, 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-1606040098 X-IAS-PPS-PHISH: NO --Apple-Mail=_99D453B5-DA99-4421-8118-613F763DC7A3 Content-Type: multipart/alternative; boundary="Apple-Mail=_E445E4C0-7BB9-4981-AB7B-7C4D161CA1FF" --Apple-Mail=_E445E4C0-7BB9-4981-AB7B-7C4D161CA1FF Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Hi Andre, 1. Are you claiming for an "equivalent" definition "without sets"? Or for t= he "right" type-theoretic counterpart of "their" notion(s)? For the =E2=80=9Cright=E2=80=9D type-theoretic counterpart of =E2=80=9Cthei= r=E2=80=9D notion. To make it equivalent (to show that there exists, in the= weak sense, an equivalence) to the one constructed through sets one would = have to add axiom of choice in the form that says that for any surjection T= -> X where X is an h-set there exists, in the weak sense, a section X -> T= . Maybe more axioms will be required but it is possible that this one will = suffice. 2. And could you further say something about what you would accept for "equ= ivalent" or for "right=E2=80=9D? For the =E2=80=9Cright=E2=80=9D I will accept a collection of theorems, inc= luding construction of examples, that shows that these objects behave in th= e way expected from (inty,1)-categories. 3. By the way, I suspect the definition you claim for would be formalized, = and it would probably be quite involved. It is very easy to formalize, for example in UniMath, the concept of a quas= i-category. Vladimir. > On Jun 4, 2016, at 1:05 AM, andr=C3=A9 hirschowitz wrote: >=20 > Hi, >=20 > 2016-06-03 21:29 GMT+02:00 Vladimir Voevodsky >: > They don=E2=80=99t take us seriously so far because we can not define (in= fty,1)-categories. As soon 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 heads in our direction. >=20 > I can believe it is reachable to define "their" notion(s) of infty-cats = within UF "through sets". Are you claiming for an "equivalent" definition "= without sets"? Or for the "right" type-theoretic counterpart of "their" no= tion(s)? > And could you further say something about what you would accept for "equi= valent" or for "right"? >=20 > Anyway, why would "they" turn their heads? They have no need, do they? >=20 > By the way, I suspect the definition you claim for would be formalized, a= nd it would probably be quite involved. Except if you require (and prove) a= characteristic property, it would be a hard (human) task to check that it = is reasonable. >=20 > ah --Apple-Mail=_E445E4C0-7BB9-4981-AB7B-7C4D161CA1FF Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Hi Andre,

1. Are you claiming for an "equ= ivalent" definition "without sets"? Or for the "right"  type-theoretic= counterpart of "their" notion(s)? 

For the =E2=80=9Cright=E2=80=9D type-theoretic coun= terpart of =E2=80=9Ctheir=E2=80=9D notion. To make it equivalent (to show t= hat there exists, in the weak sense, an equivalence) to the one constructed= through sets one would have to add axiom of choice in the form that says t= hat for any surjection T -> X where X is an h-set there exists, in the w= eak sense, a section X -> T. Maybe more axioms will be required but it i= s possible that this one will suffice. 

2. And could you further say something about wh= at you would accept for "equivalent" or for "right=E2=80=9D? 

For the =E2=80=9Cright=E2= =80=9D I will accept a collection of theorems, including construction of ex= amples, that shows that these objects behave in the way expected from (inty= ,1)-categories. 

3. By the way, I suspect the definition you claim for would be formal= ized, and it would probably be quite involved. 
<= br class=3D"">
It is very easy to formalize, for examp= le in UniMath, the concept of a quasi-category. 
=
Vladimir.






On Jun 4, 2016, at 1:05 AM, andr=C3=A9 hirschowit= z <a...@unice.fr> wro= te:

Hi,

2016-06-0= 3 21:29 GMT+02:00 Vladimir Voevodsky <vlad...@ias.edu<= /a>>:
They don=E2=80=99t take us seriously so far because we can not define = (infty,1)-categories. As soon as we find a language that can be used to def= ine them and work with them directly without going through sets they will a= ll start to turn their heads in our direction.

I can believe it is reachable to define "their" notion(s) of=20 infty-cats  within UF "through sets". Are you claiming for an=20 "equivalent" definition "without sets"? Or for the "right" =20 type-theoretic counterpart of "their" notion(s)?
And could y= ou further say something about what you would accept for "equivalent" or fo= r "right"?

Anyway, why would "they" turn thei= r heads? They have no need, do they?

By the way, I suspect the definition you claim for would be formalized, and i= t would probably be quite involved. Except if you require (and prove) a=20 characteristic property, it would be a hard (human) task to check that=20 it is reasonable.

ah

--Apple-Mail=_E445E4C0-7BB9-4981-AB7B-7C4D161CA1FF-- --Apple-Mail=_99D453B5-DA99-4421-8118-613F763DC7A3 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 iQEcBAEBCgAGBQJXUpOQAAoJEH5eMY79Hy7t0DkH/3PwDEwkR1C9uflBFdAaRw47 euHsee1bvEVb+jiLtPp4wcTnC1pDbZ05tlaIONyvitqSrpDtNjv5FqVyHMtPS/pn KVjPDyfR+6G7rfhifodGAsXJNrbggrilysktaYYMXnIqWGeCOkOJ34hHN3ZDmFBh BoRuHhe77X3DgOMir/Kvt2OSG43m0FdtFoctPnidgvYRWRnc91u8eQS+KZtj8KZR I16unRaZv5nTW+fuJhmxDE5fHi/cfoZ5kAgo7aX3hPNr2yEzgT7pCHJzw3/0jwki bJM2b3JcpFe/J8C9o9oqX4vlVhS6QF4rSCMaeT9KiTM/ShSDA5c+0z8ZqqNsukM= =Qc5j -----END PGP SIGNATURE----- --Apple-Mail=_99D453B5-DA99-4421-8118-613F763DC7A3--