From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.33.210 with SMTP id e201mr486096ita.8.1468876621793; Mon, 18 Jul 2016 14:17:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.217.147 with SMTP id p141ls677159itg.2.canary; Mon, 18 Jul 2016 14:17:01 -0700 (PDT) X-Received: by 10.66.147.132 with SMTP id tk4mr30087007pab.37.1468876621054; Mon, 18 Jul 2016 14:17:01 -0700 (PDT) Return-Path: Received: from Princeton.EDU (ppa04.Princeton.EDU. [128.112.128.215]) by gmr-mx.google.com with ESMTPS id d6si1211368ywd.4.2016.07.18.14.17.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 14:17:00 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.215 as permitted sender) client-ip=128.112.128.215; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.215 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp202l.Princeton.EDU (csgsmtp202l.Princeton.EDU [140.180.223.155]) by ppa04.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id u6ILGxM9031832 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Mon, 18 Jul 2016 17:17:00 -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 u6ILGr1F008212 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Mon, 18 Jul 2016 17:16:59 -0400 Content-Type: multipart/alternative; boundary="Apple-Mail=_22D23B1A-37C8-4665-A038-1213EE103070" Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] Different notions of equality; terminology From: Dimitris Tsementzis In-Reply-To: Date: Mon, 18 Jul 2016 17:16:53 -0400 Cc: Andrew Polonsky , Homotopy Type Theory Message-Id: <50986516-CF33-48F9-8EEB-9D10BDCFBD29@princeton.edu> References: To: Vladimir Voevodsky X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-07-18_07:,, 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-1604210000 definitions=main-1607180232 --Apple-Mail=_22D23B1A-37C8-4665-A038-1213EE103070 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 I think this is terminological. I understood Polonsky (and correct me if I= =E2=80=99m wrong) as saying that something like the =E2=80=9Cexact equality= =E2=80=9D of HTS is a =E2=80=9Csubstitutive equality=E2=80=9D that exists a= t the object (or what he is calling =E2=80=9Clogical=E2=80=9D) level and ca= n therefore be reasoned about. (It is of course distinct from the judgmenta= l equality of HTS which lies in the background.)=20 So is the so-called exact equality of HTS an example of a =E2=80=9Csubstitu= tive equality=E2=80=9D for you? Or do you still call that =E2=80=9Ctranspor= tational=E2=80=9D and reserve the name =E2=80=9Csubstitutive=E2=80=9D for m= eta-level equalities that can only be checked? (This is a terminological qu= estion.) Dimitris > On Jul 18, 2016, at 17:05, Vladimir Voevodsky wrote: >=20 >=20 >> On Jul 18, 2016, at 10:45 PM, Andrew Polonsky > wrote: >>=20 >> Finally, Voevodsky currently distinguishes between "substitutive" and "t= ransportational" equalities. But in his system, both concepts 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 object logic, while retai= ning other properties like the conversion rule. >=20 > I am not sure what you mean by this. In fact, I emphasized that the only= substitutional equality in MLTTs is the definitional equality that can not= be postulated or proved, only checked.=20 >=20 > Vladimir. >=20 >=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 . --Apple-Mail=_22D23B1A-37C8-4665-A038-1213EE103070 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
I = think this is terminological. I understood Polonsky (and correct me if I=E2= =80=99m wrong) as saying that something like the =E2=80=9Cexact equality=E2= =80=9D of HTS is a =E2=80=9Csubstitutive equality=E2=80=9D that exists at t= he object (or what he is calling =E2=80=9Clogical=E2=80=9D) level and can t= herefore be reasoned about. (It is of course distinct from the judgmental e= quality of HTS which lies in the background.) 
So is the so-called exact equality of HT= S an example of a =E2=80=9Csubstitutive equality=E2=80=9D for you? Or do yo= u still call that =E2=80=9Ctransportational=E2=80=9D and reserve the name = =E2=80=9Csubstitutive=E2=80=9D for meta-level equalities that can only be c= hecked? (This is a terminological question.)

Dimitris

On Jul 18, 2016, at 17:05, Vladimir= Voevodsky <vlad...@ias.ed= u> wrote:


On Jul 18, 20= 16, at 10:45 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

Finally, Voevodsky currently distinguishes between "su= bstitutive" and "transportational" equalities.  But in his system, bot= h concepts are of the "logical" kind.  The effect is therefore to prom= ote "strict" equality to the logical level; so one can reason about it in t= he object logic, while retaining other properties like the conversion rule.=

I am not sur= e what you mean by this.  In fact, I emphasized that the only substitu= tional equality in MLTTs is the definitional equality that can not be postu= lated or proved, only checked. 

Vladimir.




--
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 e= mail to H= omotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_22D23B1A-37C8-4665-A038-1213EE103070--