From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.53.203 with SMTP id l11mr2086804qtb.12.1474657521140; Fri, 23 Sep 2016 12:05:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.45.116 with SMTP id v107ls1404037ota.19.gmail; Fri, 23 Sep 2016 12:05:20 -0700 (PDT) X-Received: by 10.129.121.70 with SMTP id u67mr1955747ywc.2.1474657520519; Fri, 23 Sep 2016 12:05: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 63si819087ywe.1.2016.09.23.12.05.20 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 23 Sep 2016 12:05:20 -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 pps.reinject (pps3.ias.edu [127.0.0.1]) by pps3.ias.edu (8.15.0.59/8.15.0.59) with ESMTPS id u8NJ5J62028315 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Fri, 23 Sep 2016 15:05:19 -0400 Received: from pps3.ias.edu (pps3.ias.edu [127.0.0.1]) by pps.reinject (8.15.0.59/8.15.0.59) with SMTP id u8NJ5J8E028309; Fri, 23 Sep 2016 15:05:19 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX1/DXHm+UlBrp9x4q8qcGTaVaQXnaTFj6pBMhomvw6SL3yz4 u33CN+k27CkWffi7DLlaajRFWullhC0YI81ixDhXWF9Fi5db8KQNDqr4rahRnVtIT6QRUSrA Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u8NJ5JIY028307 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Fri, 23 Sep 2016 15:05:19 -0400 Received: from hsi-kbw-085-216-024-254.hsi.kabelbw.de ([85.216.24.254] helo=[192.168.58.189]) by imap.math.ias.edu with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.80.1) (envelope-from ) id 1bnVmg-00058u-7p; Fri, 23 Sep 2016 15:05:19 -0400 Subject: Re: [HoTT] new slides Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: multipart/signed; boundary="Apple-Mail=_A3E137FB-BF4B-422E-AB77-AA70EF268FF3"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail From: Vladimir Voevodsky In-Reply-To: <3D8D7C5A-350F-422C-89CD-2600AF68A8B0@princeton.edu> Date: Fri, 23 Sep 2016 21:05:16 +0200 Cc: "Prof. Vladimir Voevodsky" , Univalent Mathematics , Homotopy Type Theory Message-Id: References: <6E32CAD6-D1D3-4B4D-973A-BA872F84037B@ias.edu> <3D8D7C5A-350F-422C-89CD-2600AF68A8B0@princeton.edu> To: Dimitris Tsementzis X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-09-23_07:,, 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 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=donotscan adjust=0 reason=safe scancount=1 engine=8.0.1-1609020000 definitions=main-1609230348 X-IAS-PPS-PHISH: NO --Apple-Mail=_A3E137FB-BF4B-422E-AB77-AA70EF268FF3 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 No, it is more related to another idea that I am not quite ready to explain= yet. Vladimir. > On Sep 23, 2016, at 1:12 AM, Dimitris Tsementzis = wrote: >=20 > On the fourth bullet point of slide 12 it is claimed that it might be eas= ier to solve the problem of infinite objects in CTT. Why is that the case? >=20 > Is this related to the third bullet point, namely because it might be eas= ier to implement a strict equality in CTT? (I still don=E2=80=99t understan= d why implementing a strict equality in CTT is easier than in MLTT+UA, but = at least this way I see the connection with the problem of infinite objects= .) >=20 > Dimitris >=20 >> On Sep 22, 2016, at 15:46, Vladimir Voevodsky wrote: >>=20 >> Hello, >>=20 >> I have uploaded to me homepage the slides of my lecture at HLF 2016 with= a discussion of the Univalent Foundations and some discussion of the UniMa= th library. See https://www.math.ias.edu/vladimir/Lectures . >>=20 >> Vladimir. >>=20 >>=20 >>=20 >> -- >> 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. >=20 --Apple-Mail=_A3E137FB-BF4B-422E-AB77-AA70EF268FF3 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 iQEcBAEBCgAGBQJX5XzsAAoJEH5eMY79Hy7tV3gH/0ifCIR75T0HR285ffp8Re8z sMlVf3BVxojdNPXf1yMFml8qjI6XQBTgsNaeVBmNxNarRl4YASIW16SgSal0QZ1v xvFqEg2UjQMjeHM58oiHavTOBjkR7sOQw3QU6agy9VJ9CfM/Iwc3UAByPY2RK9Lp Ga08wRKXU8EFd5iXDQFYMZ+0grOJ07GtdlD3YI/vI/VBhqzfvcYxlzSHiPMkBw7r sqWn4F7fscVXJorVFg4FMQMwWixH60XL/r+tLtrMfqQDh6yEu0ic7Z2agC9Lib+4 +JqKxB9eGwC6cRVuTECB6qGnyEXDhT5wiJASAWseLnYx3Z1c+e3yOQR3saSLzJU= =Ak5w -----END PGP SIGNATURE----- --Apple-Mail=_A3E137FB-BF4B-422E-AB77-AA70EF268FF3--