From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.176.2.15 with SMTP id 15mr659880uas.9.1474585951730; Thu, 22 Sep 2016 16:12:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.61.202 with SMTP id l68ls7955631otc.1.gmail; Thu, 22 Sep 2016 16:12:31 -0700 (PDT) X-Received: by 10.237.36.12 with SMTP id r12mr906325qtc.48.1474585950979; Thu, 22 Sep 2016 16:12:30 -0700 (PDT) Return-Path: Received: from Princeton.EDU (ppa03.Princeton.EDU. [128.112.128.214]) by gmr-mx.google.com with ESMTPS id c75si321283ywh.0.2016.09.22.16.12.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 22 Sep 2016 16:12:30 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.214 as permitted sender) client-ip=128.112.128.214; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.214 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp202l.Princeton.EDU (csgsmtp202l.Princeton.EDU [140.180.223.155]) by ppa03.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id u8MNCTWY017888 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Thu, 22 Sep 2016 19:12:30 -0400 Received: from 192.168.1.4 (pool-96-239-81-135.nycmny.east.verizon.net [96.239.81.135]) (authenticated authid=dtsement bits=0) by csgsmtp202l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id u8MNCT12017783 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Thu, 22 Sep 2016 19:12:29 -0400 Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] new slides From: Dimitris Tsementzis In-Reply-To: <6E32CAD6-D1D3-4B4D-973A-BA872F84037B@ias.edu> Date: Thu, 22 Sep 2016 19:12:27 -0400 Cc: Univalent Mathematics , Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: <3D8D7C5A-350F-422C-89CD-2600AF68A8B0@princeton.edu> References: <6E32CAD6-D1D3-4B4D-973A-BA872F84037B@ias.edu> To: Vladimir Voevodsky X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-09-22_10:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=8 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1609020000 definitions=main-1609220399 On the fourth bullet point of slide 12 it is claimed that it might be easie= r to solve the problem of infinite objects in CTT. Why is that the case? Is this related to the third bullet point, namely because it might be easie= r to implement a strict equality in CTT? (I still don=E2=80=99t understand = 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.) Dimitris > 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 UniMat= h library. See https://www.math.ias.edu/vladimir/Lectures . >=20 > Vladimir. >=20 >=20 >=20 > --=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.