From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.33.4 with SMTP id h4mr29567395ywh.24.1468878312087; Mon, 18 Jul 2016 14:45:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.11.58 with SMTP id a55ls7945884ota.18.gmail; Mon, 18 Jul 2016 14:45:11 -0700 (PDT) X-Received: by 10.157.38.144 with SMTP id l16mr29761707otb.24.1468878311645; Mon, 18 Jul 2016 14:45:11 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id f206si587740ywb.6.2016.07.18.14.45.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Jul 2016 14:45:11 -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 u6ILjAW0013196 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 18 Jul 2016 17:45:10 -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 u6ILjAQt013190; Mon, 18 Jul 2016 17:45:10 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX1840CBN5pQFV9ysvdHNHPx+x2aTFqeMW1H9AiyjriUywRC2 pI2WAG1ANBCpddjOA0wCddydqp/7peC1aSH2J9tQafBErkcQX7thHs7bDZ5iD8MmYfFGxqe9 Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u6ILjAkH013189 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 18 Jul 2016 17:45:10 -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 1bPGLd-0003Uo-Tv; Mon, 18 Jul 2016 17:45:10 -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=_0864434B-9934-476E-BF53-29CD1308FD86"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail From: Vladimir Voevodsky In-Reply-To: Date: Mon, 18 Jul 2016 23:45:07 +0200 Cc: "Prof. Vladimir Voevodsky" , Homotopy Type Theory Message-Id: <401A4D12-E6E7-4864-BE28-A13098CE9A68@ias.edu> References: <2506A3A8-8AC0-4B49-AD1E-D660A7A15245@ias.edu> <085E4ACF-BD06-484F-ACA3-17DD6249CF76@ias.edu> To: Andrew Polonsky X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-07-18_08:,, 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-1607180238 X-IAS-PPS-PHISH: NO --Apple-Mail=_0864434B-9934-476E-BF53-29CD1308FD86 Content-Type: multipart/alternative; boundary="Apple-Mail=_FCDF5577-18F7-461D-89E2-AADA9F532FBC" --Apple-Mail=_FCDF5577-18F7-461D-89E2-AADA9F532FBC Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii In the abstract (http://fomus.weebly.com/abstracts.html ) I meant the theory of Altenkich, Capriotti and Krau= s (http://arxiv.org/abs/1604.03799 ) or th= e logic-enriched type theory by Part and Lou (https://arxiv.org/abs/1506.04= 998 ). One can also apply it to the poss= ible theories with the second transportational equality of the form suggest= ed at the end of my talk today. In the HTS (https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/f= iles/HTS.pdf ) there is still only one substitutional and one transporta= tional equality but the substitutional one is, indeed, type-based and so ca= n be reasoned about at the object level. Vladimir. > On Jul 18, 2016, at 11:18 PM, Andrew Polonsky wrot= e: >=20 > I mean whatever system is implicitly referred to by the last sentence > in the abstract of your talk. >=20 > On Mon, Jul 18, 2016 at 11:16 PM, Vladimir Voevodsky wr= ote: >> Referring to it at what point in the talk? >>=20 >>> On Jul 18, 2016, at 11:16 PM, Andrew Polonsky wr= ote: >>>=20 >>> I assumed you were referring in your talk to HTS or some variant of it. >>>=20 >>> On Mon, Jul 18, 2016 at 11:15 PM, Vladimir Voevodsky = wrote: >>>> I still do not understand. What do you mean by my system? >>>>=20 >>>>> On Jul 18, 2016, at 11:13 PM, Andrew Polonsky = wrote: >>>>>=20 >>>>> On Mon, Jul 18, 2016 at 11:05 PM, Vladimir Voevodsky wrote: >>>>>> Finally, Voevodsky currently distinguishes between "substitutive" an= d >>>>>> "transportational" equalities. But in his system, both concepts are= of the >>>>>> "logical" kind. The effect is therefore to promote "strict" equalit= y to the >>>>>> logical level; so one can reason about it in the object logic, while >>>>>> retaining other properties like the conversion rule. >>>>>>=20 >>>>>>=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 c= an not >>>>>> be postulated or proved, only checked. >>>>>=20 >>>>> I mean that your system with two equalities promotes strict equality >>>>> of MLTT from definitional to the logical level. It remains >>>>> "substitutional" but can be asserted in context. >>>>>=20 >>>>> It would be nice to have a few simple demonstrations of the uses of >>>>> this, without getting into simplicial types. >>>>>=20 >>>>> Andrew >>>>>=20 >>>>> -- >>>>> You received this message because you are subscribed to the Google Gr= oups "Homotopy Type Theory" group. >>>>> To unsubscribe from this group and stop receiving emails from it, sen= d an email to HomotopyTypeThe...@googlegroups.com. >>>>> For more options, visit https://groups.google.com/d/optout. >>>>=20 >>=20 --Apple-Mail=_FCDF5577-18F7-461D-89E2-AADA9F532FBC Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=us-ascii In the abstract= (http://fomu= s.weebly.com/abstracts.html)  I meant the theory of Altenkich, Cap= riotti and Kraus (ht= tp://arxiv.org/abs/1604.03799) or the logic-enriched type theory b= y Part and Lou (htt= ps://arxiv.org/abs/1506.04998).  One can also apply it to the= possible theories with the second transportational equality of the form su= ggested at the end of my talk today.

In the HTS (https://www.math.ias.edu/= vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf)  there is stil= l only one substitutional and one transportational equality but the substit= utional one is, indeed, type-based and so can be reasoned about at the obje= ct level. 

V= ladimir.


On Jul 18, 2016, at 11:18 PM, Andrew Polonsky &= lt;andrew....@gmail.com<= /a>> wrote:

I mean whatever system is implicitly referred to by the la= st sentence
in the abstract of your talk.

On Mon, Jul 18, 2016 at 11:16 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
Referring to it at what point= in the talk?

On Jul 18, 2016, at 11:16 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

I assumed you were referring in your talk to HTS or s= ome variant of it.

On Mon, Jul 18, 2016 at 11:= 15 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
I still do not understand. What do you mean by my system?

On Jul 18, 2016, = at 11:13 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

O= n Mon, Jul 18, 2016 at 11:05 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
Finally, Voevodsky currently distinguishe= s between "substitutive" and
"transportational" equalities. &= nbsp;But in his system, both concepts are of the
"logical" ki= nd.  The effect is therefore to promote "strict" equality to the
logical level; so one can reason about it in the object logic, whi= le
retaining other properties like the conversion rule.


I am not sure what you mean by this.=  In fact, I emphasized that the only
substitutional equ= ality in MLTTs is the definitional equality that can not
be p= ostulated or proved, only checked.

I mean that your system with two equalities promotes strict equality
of MLTT from definitional to the logical level.  It remains<= br class=3D"">"substitutional" but can be asserted in context.

It would be nice to have a few simple demonstrations of th= e uses of
this, without getting into simplicial types.

Andrew

--
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.



<= /body> --Apple-Mail=_FCDF5577-18F7-461D-89E2-AADA9F532FBC-- --Apple-Mail=_0864434B-9934-476E-BF53-29CD1308FD86 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 iQEcBAEBCgAGBQJXjU3kAAoJEH5eMY79Hy7t8doH/2EWioZWAHQgge3LcVrKDmrD Sio8EyN4PxF0zxZP1UsgIZF0/fcUcw9x8nz9VVHd10JHLIVV+pi51gXZV5o2xvrj 4VlmgHieChZAWGJKuI+M8nIwUtQw6Yi9ri4hUfP8ehoTJQbq2iQHfgWu0XBHKaF5 uR5p8oZIFRjjofbBqDE3SYY9axBkXkEBRw97Y8bIQq5TES8EHWbSzQHsqMiFRcO2 3fErTWWDb62HCEYloZIC19qbUSiNiSmev+50Lx+h4aEn+JHOH+ovS0JcTlPo5TP6 CmbfJICs5mGIe91s3vMqWe29OexfAYz+2403fDf5yeOSe9u/5Y3EGAXKAwCwBxw= =nufq -----END PGP SIGNATURE----- --Apple-Mail=_0864434B-9934-476E-BF53-29CD1308FD86--