From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.212.149 with SMTP id w143mr16927747ywd.23.1468875920300; Mon, 18 Jul 2016 14:05:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.41.245 with SMTP id g50ls9154475otd.1.gmail; Mon, 18 Jul 2016 14:05:19 -0700 (PDT) X-Received: by 10.129.108.149 with SMTP id h143mr23250485ywc.30.1468875919917; Mon, 18 Jul 2016 14:05:19 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id w1si1483511yww.7.2016.07.18.14.05.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 14:05:19 -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 u6IL5Ih1007790 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 18 Jul 2016 17:05:18 -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 u6IL5Icn007782; Mon, 18 Jul 2016 17:05:18 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX1+tq4Z0qzV+vU9wQbz1o2g4ZgTMcYpHuZjUonCFoHGr6+Us uCtjEpl5oPfzbGQQRsC2rc55RO/x5QkIzyC0ttiKBgIj1GbEY1sWYoB0WuyE2igqG8r1/zeb Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u6IL5IM0007781 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 18 Jul 2016 17:05:18 -0400 Received: from [89.245.134.42] (helo=[10.11.168.153]) by imap.math.ias.edu with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.80.1) (envelope-from ) id 1bPFj4-00023o-7t; Mon, 18 Jul 2016 17:05:18 -0400 Subject: Re: [HoTT] Different notions of equality; terminology Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: multipart/signed; boundary="Apple-Mail=_907A06A9-2460-44D7-9B21-74B8D57D1385"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail From: Vladimir Voevodsky In-Reply-To: Date: Mon, 18 Jul 2016 23:05:15 +0200 Cc: "Prof. Vladimir Voevodsky" , Homotopy Type Theory Message-Id: References: To: Andrew Polonsky X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-07-18_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 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-1607180230 X-IAS-PPS-PHISH: NO --Apple-Mail=_907A06A9-2460-44D7-9B21-74B8D57D1385 Content-Type: multipart/alternative; boundary="Apple-Mail=_DCFF5E6A-7AB5-4FFB-BD2A-962F7821843B" --Apple-Mail=_DCFF5E6A-7AB5-4FFB-BD2A-962F7821843B Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii > On Jul 18, 2016, at 10:45 PM, Andrew Polonsky wrot= e: >=20 > Finally, Voevodsky currently distinguishes between "substitutive" and "tr= ansportational" equalities. But in his system, both concepts are of the "l= ogical" kind. The effect is therefore to promote "strict" equality to the = logical level; so one can reason about it in the object logic, while retain= ing other properties like the conversion rule. I am not sure what you mean by this. In fact, I emphasized that the only s= ubstitutional equality in MLTTs is the definitional equality that can not b= e postulated or proved, only checked. Vladimir. --Apple-Mail=_DCFF5E6A-7AB5-4FFB-BD2A-962F7821843B Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=us-ascii
=
On Jul 18, 2016, = at 10:45 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

Finally, Voevodsky currently distinguishes between "substi= tutive" and "transportational" equalities.  But in his system, both co= ncepts are of the "logical" kind.  The effect is therefore to promote = "strict" equality to the logical level; so one can reason about it in the o= bject logic, while retaining other properties like the conversion rule.

I am not sure wh= at you mean by this.  In fact, I emphasized that the only substitution= al equality in MLTTs is the definitional equality that can not be postulate= d or proved, only checked. 

=
Vladimir.



<= /html> --Apple-Mail=_DCFF5E6A-7AB5-4FFB-BD2A-962F7821843B-- --Apple-Mail=_907A06A9-2460-44D7-9B21-74B8D57D1385 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 iQEcBAEBCgAGBQJXjUSMAAoJEH5eMY79Hy7t7+UH/3BYkekrUuly7qqMKphG9u8k y4GT2kc+DTggj5rg3k2tuMxAQ/1ib64k77s/4MEjd1Ki5TZSrHRIe+HM5sojX5XL Aiqoj2OlAEEjMZhdfQ7S3KVT2lIv6K/62GThvWTfzWjROjHOre8TixypB4P2Vt5Y I1a5JIhG14VfdHqslBnJmOaDU3l1zAJgaUapZT50UXKECcLrclDY0vcdllOOI3mm Hd+SxHnKcwMhpUIZVQ9kWjNRrZV7EoM5nYZeRR8w4+NTtlVihxMHgDKc+reCXNOR sRj7b/imQfWvB/HwrmOAxI7eCUDerIGJpB8XaxugHFWn/aW3KmPgPTHPEpgEOe8= =2UUI -----END PGP SIGNATURE----- --Apple-Mail=_907A06A9-2460-44D7-9B21-74B8D57D1385--