From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.14.181 with SMTP id 50mr33632199otj.27.1468948730007; Tue, 19 Jul 2016 10:18:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.154.197 with SMTP id c188ls2308028ioe.0.gmail; Tue, 19 Jul 2016 10:18:48 -0700 (PDT) X-Received: by 10.36.236.70 with SMTP id g67mr591420ith.8.1468948728457; Tue, 19 Jul 2016 10:18:48 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id w1si1764396yww.7.2016.07.19.10.18.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Jul 2016 10:18:48 -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 u6JHIlcx019973 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Tue, 19 Jul 2016 13:18:47 -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 u6JHIl7i019967 for ; Tue, 19 Jul 2016 13:18:47 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX19z2XdMEQhTdK63NqYdPoTylxHy+QGiO6Ta3VHUlLGo9hSM mxPoFYkVdz2lEZ+P4h7c7v7dk1t12Op0KLEISc1r3my+sT4Xey1AWZmT80LgAUPH2pC8JIdt Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u6JHIlns019966 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Tue, 19 Jul 2016 13:18:47 -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 1bPYfP-0006qi-E0; Tue, 19 Jul 2016 13:18:47 -0400 From: Vladimir Voevodsky X-Pgp-Agent: GPGMail Content-Type: multipart/signed; boundary="Apple-Mail=_E677050E-EE78-40D1-9C94-CFBD91A69AF6"; protocol="application/pgp-signature"; micalg=pgp-sha512 Subject: FOMUS slides Date: Tue, 19 Jul 2016 19:18:45 +0200 Message-Id: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> Cc: "Prof. Vladimir Voevodsky" To: HomotopyTypeTheory@googlegroups.com Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-07-19_10:,, 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-1607190182 X-IAS-PPS-PHISH: NO --Apple-Mail=_E677050E-EE78-40D1-9C94-CFBD91A69AF6 Content-Type: multipart/alternative; boundary="Apple-Mail=_3BDF5ADA-51F0-4EDE-AD4A-031DAA8AEECB" --Apple-Mail=_3BDF5ADA-51F0-4EDE-AD4A-031DAA8AEECB Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii Hello, the slides of my FOMUS talk that have started the discussion about equaliti= es are now available at my website https://www.math.ias.edu/vladimir/lectur= es . Vladimir. --Apple-Mail=_3BDF5ADA-51F0-4EDE-AD4A-031DAA8AEECB Content-Transfer-Encoding: 7bit Content-Type: text/html; charset=us-ascii Hello,

the slides of my FOMUS talk that have started the discussion about equalities are now available at my website https://www.math.ias.edu/vladimir/lectures .

Vladimir.

--Apple-Mail=_3BDF5ADA-51F0-4EDE-AD4A-031DAA8AEECB-- --Apple-Mail=_E677050E-EE78-40D1-9C94-CFBD91A69AF6 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 iQEcBAEBCgAGBQJXjmD1AAoJEH5eMY79Hy7t1d0IAMrlLoiCnx7le1V6QI/u67e3 UJy97mQn8u7Uls0U4s3ZeW0/M0IN0RHYpSjirFhhXinw0qc1nn53WXDQeUbU7RDg kDIdK8wbciWqVIVwvbyP4KyzY6YqiBvSVWAHTRC3hBQ7V8lj2Uyu1VDQcoSA0F8l uMf0TRZ2spibnYhFXzBg6a0gkkipBGAqwR6+VBCNlXxJuxqsBF+X8js/aHKlO3w7 aUcwYMJhmqrz0X4wRjJDTA0tiZiV4sAqzZNDx7OHcWgVGwa1+kcRzULw4BS+qrKQ fbtSUZ8TH9hZ+v9zYxn6J00Zz8BnqR8Ku9AnUiQme3+P9lqAr0xLZiCC3y4S6bw= =8stR -----END PGP SIGNATURE----- --Apple-Mail=_E677050E-EE78-40D1-9C94-CFBD91A69AF6-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.131.70 with SMTP id t67mr23938320ywf.28.1468952218851; Tue, 19 Jul 2016 11:16:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.1.65 with SMTP id 62ls4214336iob.45.gmail; Tue, 19 Jul 2016 11:16:58 -0700 (PDT) X-Received: by 10.66.76.66 with SMTP id i2mr32090048paw.39.1468952218281; Tue, 19 Jul 2016 11:16:58 -0700 (PDT) Return-Path: Received: from exchange.sandiego.edu ([192.195.154.6]) by gmr-mx.google.com with ESMTPS id ph9si2143779pac.1.2016.07.19.11.16.58 for (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 19 Jul 2016 11:16:58 -0700 (PDT) Received-SPF: neutral (google.com: 192.195.154.6 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=192.195.154.6; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 192.195.154.6 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: from mail-lf0-f52.google.com (10.0.26.240) by exchange.sandiego.edu (10.0.25.65) with Microsoft SMTP Server (TLS) id 14.3.294.0; Tue, 19 Jul 2016 11:16:57 -0700 Received: by mail-lf0-f52.google.com with SMTP id b199so21198831lfe.0 for ; Tue, 19 Jul 2016 11:16:57 -0700 (PDT) X-Gm-Message-State: ALyK8tK8kj5oH9HLNRmOaOGPVenJ9vq3v6eeghs3i9W1F3HPE4kvmoeJttbNrEgqRUcaAittyd/GGynK8XuRDg== X-Received: by 10.25.143.137 with SMTP id r131mr985206lfd.165.1468952214842; Tue, 19 Jul 2016 11:16:54 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Tue, 19 Jul 2016 11:16:35 -0700 (PDT) In-Reply-To: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> From: Michael Shulman Date: Tue, 19 Jul 2016 15:16:35 -0300 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] FOMUS slides To: Vladimir Voevodsky CC: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Return-Path: shu...@sandiego.edu X-Originating-IP: [10.0.26.240] Can you explain the idea on the last slide a little more? Did you actually mean to say that R and "transportb0 R e" both have type P2, or should one of them have had type P1? If the latter, then how can we tell what type(s) "transportb0 R e" is allowed to have based on knowing the types of R and e? On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky wrote: > Hello, > > the slides of my FOMUS talk that have started the discussion about > equalities are now available at my website > https://www.math.ias.edu/vladimir/lectures . > > 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 > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.154.146 with SMTP id c140mr33104916vke.12.1468956494246; Tue, 19 Jul 2016 12:28:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.10.20 with SMTP id 20ls7743284otg.20.gmail; Tue, 19 Jul 2016 12:28:13 -0700 (PDT) X-Received: by 10.129.162.6 with SMTP id z6mr33625397ywg.15.1468956493558; Tue, 19 Jul 2016 12:28:13 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id d6si1474701ywd.4.2016.07.19.12.28.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Jul 2016 12:28:13 -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 u6JJSCKr013640 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Tue, 19 Jul 2016 15:28:12 -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 u6JJSCHd013634; Tue, 19 Jul 2016 15:28:12 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX183KCRqg+6JDZppWAFOGAj6XvBCumkNEH1Gb+5J2Tdgor4G 2xQ+SLjnkA6AK/k5JhNuhJPn+8ti374XNP9JfxLPNyXZIeIb6G+AQRN+WRU4eyJ9HqMC1bQX Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u6JJSCfx013633 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Tue, 19 Jul 2016 15:28:12 -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 1bPage-00009G-D1; Tue, 19 Jul 2016 15:28:12 -0400 Subject: Re: [HoTT] FOMUS slides Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: multipart/signed; boundary="Apple-Mail=_C757B2D4-8522-489C-82F5-DBC496BF1D8E"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail From: Vladimir Voevodsky In-Reply-To: Date: Tue, 19 Jul 2016 21:28:10 +0200 Cc: "Prof. Vladimir Voevodsky" , "HomotopyT...@googlegroups.com" Message-Id: References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> To: Michael Shulman X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-07-19_12:,, 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-1607190206 X-IAS-PPS-PHISH: NO --Apple-Mail=_C757B2D4-8522-489C-82F5-DBC496BF1D8E Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii Thank you for spotting this typo. It is supposed to be P_1. I have correcte= d the slides. > On Jul 19, 2016, at 8:16 PM, Michael Shulman wrote: >=20 > Can you explain the idea on the last slide a little more? Did you > actually mean to say that R and "transportb0 R e" both have type P2, > or should one of them have had type P1? If the latter, then how can > we tell what type(s) "transportb0 R e" is allowed to have based on > knowing the types of R and e? >=20 > On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky wro= te: >> Hello, >>=20 >> the slides of my FOMUS talk that have started the discussion about >> equalities are now available at my website >> https://www.math.ias.edu/vladimir/lectures . >>=20 >> Vladimir. >>=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 > -- > 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=_C757B2D4-8522-489C-82F5-DBC496BF1D8E 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 iQEcBAEBCgAGBQJXjn9KAAoJEH5eMY79Hy7thlMH/00qeDaSvc5HZzfWdDCodAC/ 9BITfrYGuw8hckE7/KsZqYxTlbLNrFzYP5lSV+C8vppwIgXWYSKMKTBS/Md+XEDt O0FExKdaNu2LGsvv+GqOZfmUT+ZQjRFheGftZjzmm6MXmHLPUoG1i8RcH5NP0ysW 6ZqERSeWC3wV7ES3McppAeA6tavLHqvshrTZjnQSTLbRfVaAYFaKxH9Gzw0tPxpH uSBkazwCM0J1YGdLZaIfIdtWbMAC0YkG0sK8bX+IeLS3f0k+ix5pJzExLaMeF/6x TM/YV6u6JUWbiiQqmlZsGFcHkNEj8nxrfBDaDOyQVX2dte2gRt3Ay5qLf6yJ35w= =FfFk -----END PGP SIGNATURE----- --Apple-Mail=_C757B2D4-8522-489C-82F5-DBC496BF1D8E-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.85.196 with SMTP id e187mr4671104itb.2.1468956604018; Tue, 19 Jul 2016 12:30:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.73.68 with SMTP id z65ls259255ita.21.gmail; Tue, 19 Jul 2016 12:30:03 -0700 (PDT) X-Received: by 10.67.14.70 with SMTP id fe6mr33580925pad.5.1468956603199; Tue, 19 Jul 2016 12:30:03 -0700 (PDT) Return-Path: Received: from exchange.sandiego.edu ([192.195.154.6]) by gmr-mx.google.com with ESMTPS id a133si1595168pfa.0.2016.07.19.12.30.03 for (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 19 Jul 2016 12:30:03 -0700 (PDT) Received-SPF: neutral (google.com: 192.195.154.6 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=192.195.154.6; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 192.195.154.6 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: from mail-lf0-f41.google.com (10.0.26.241) by exchange.sandiego.edu (10.0.25.65) with Microsoft SMTP Server (TLS) id 14.3.294.0; Tue, 19 Jul 2016 12:30:01 -0700 Received: by mail-lf0-f41.google.com with SMTP id g62so22343523lfe.3 for ; Tue, 19 Jul 2016 12:30:01 -0700 (PDT) X-Gm-Message-State: ALyK8tJZl4+pO/wGx2iTuIXhRSjJ5Jo4sTKL/CYHyerRo0fe8FAr+KJui7v/nMNwVuyTK1VvaexzH0jK0+TfjQ== X-Received: by 10.25.143.137 with SMTP id r131mr1250985lfd.165.1468956599592; Tue, 19 Jul 2016 12:29:59 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Tue, 19 Jul 2016 12:29:39 -0700 (PDT) In-Reply-To: References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> From: Michael Shulman Date: Tue, 19 Jul 2016 16:29:39 -0300 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] FOMUS slides To: Vladimir Voevodsky CC: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Return-Path: shu...@sandiego.edu X-Originating-IP: [10.0.26.241] Okay, so then suppose I have e:Id0 T A B and R:P2. What is the type of transportb0 R e? On Tue, Jul 19, 2016 at 4:28 PM, Vladimir Voevodsky wrote: > Thank you for spotting this typo. It is supposed to be P_1. I have corrected the slides. > > >> On Jul 19, 2016, at 8:16 PM, Michael Shulman wrote: >> >> Can you explain the idea on the last slide a little more? Did you >> actually mean to say that R and "transportb0 R e" both have type P2, >> or should one of them have had type P1? If the latter, then how can >> we tell what type(s) "transportb0 R e" is allowed to have based on >> knowing the types of R and e? >> >> On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky wrote: >>> Hello, >>> >>> the slides of my FOMUS talk that have started the discussion about >>> equalities are now available at my website >>> https://www.math.ias.edu/vladimir/lectures . >>> >>> 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 >>> email to HomotopyTypeThe...@googlegroups.com. >>> For more options, visit https://groups.google.com/d/optout. >> >> -- >> 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. > > -- > 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. From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 19 Jul 2016 23:07:44 -0700 (PDT) From: Andrew Polonsky To: Homotopy Type Theory Cc: shu...@sandiego.edu, vlad...@ias.edu Message-Id: <6b38173e-7baf-44ba-8d18-b4dc06a5c300@googlegroups.com> In-Reply-To: References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> Subject: Re: [HoTT] FOMUS slides MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2297_1438408500.1468994864779" ------=_Part_2297_1438408500.1468994864779 Content-Type: multipart/alternative; boundary="----=_Part_2298_1776837257.1468994864780" ------=_Part_2298_1776837257.1468994864780 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable A couple of years ago, I have experimented with a system based on a similar= =20 idea. See page 7 here: https://dl.dropboxusercontent.com/u/7730626/ett3.pdf The reduction rules for transporting over a type equality e : A =E2=89=88 B= can=20 indeed be defined purely by induction on e, as on page 9. (And, if you=20 want to add univalence, then equivalence will be a constructor for this=20 type, in which case the transport will reduce to the function given in this= =20 constructor.) Cheers, Andrew On Tuesday, July 19, 2016 at 9:28:14 PM UTC+2, v v wrote: > > Thank you for spotting this typo. It is supposed to be P_1. I have=20 > corrected the slides.=20 > > > > On Jul 19, 2016, at 8:16 PM, Michael Shulman > wrote:=20 > >=20 > > Can you explain the idea on the last slide a little more? Did you=20 > > actually mean to say that R and "transportb0 R e" both have type P2,=20 > > or should one of them have had type P1? If the latter, then how can=20 > > we tell what type(s) "transportb0 R e" is allowed to have based on=20 > > knowing the types of R and e?=20 > >=20 > > On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky > wrote:=20 > >> Hello,=20 > >>=20 > >> the slides of my FOMUS talk that have started the discussion about=20 > >> equalities are now available at my website=20 > >> https://www.math.ias.edu/vladimir/lectures .=20 > >>=20 > >> Vladimir.=20 > >>=20 > >> --=20 > >> You received this message because you are subscribed to the Google=20 > Groups=20 > >> "Homotopy Type Theory" group.=20 > >> To unsubscribe from this group and stop receiving emails from it, send= =20 > an=20 > >> email to HomotopyTypeThe...@googlegroups.com .=20 > > >> For more options, visit https://groups.google.com/d/optout.=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeThe...@googlegroups.com .=20 > > > For more options, visit https://groups.google.com/d/optout.=20 > > ------=_Part_2298_1776837257.1468994864780 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
A couple of years ago, I have experimented with a system b= ased on a similar idea. =C2=A0See page 7 here:

https://d= l.dropboxusercontent.com/u/7730626/ett3.pdf

The re= duction rules for transporting over a type equality e : A =E2=89=88 B can i= ndeed be defined purely by induction on e, as on page 9. =C2=A0(And, if you= want to add univalence, then equivalence will be a constructor for this ty= pe, in which case the transport will reduce to the function given in this c= onstructor.)

Cheers,
Andrew

On Tu= esday, July 19, 2016 at 9:28:14 PM UTC+2, v v wrote:
Thank you for spotting this typo. It is supposed to b= e P_1. I have corrected the slides.


> On Jul 19, 2016, at 8:16 PM, Michael Shulman <shu...@sandiego.edu> wrote:
>=20
> Can you explain the idea on the last slide a little more? =C2=A0Di= d you
> actually mean to say that R and "transportb0 R e" both h= ave type P2,
> or should one of them have had type P1? =C2=A0If the latter, then = how can
> we tell what type(s) "transportb0 R e" is allowed to hav= e based on
> knowing the types of R and e?
>=20
> On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky <vla...@ias.edu= > wrote:
>> Hello,
>>=20
>> the slides of my FOMUS talk that have started the discussion a= bout
>> equalities are now available at my website
>> https://www.mat= h.ias.edu/vladimir/lectures .
>>=20
>> Vladimir.
>>=20
>> --
>> You received this message because you are subscribed to the Go= ogle Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from = it, send an
>> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> For more options, visit https://group= s.google.com/d/optout.
>=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 HomotopyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.go= ogle.com/d/optout.

------=_Part_2298_1776837257.1468994864780-- ------=_Part_2297_1438408500.1468994864779-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.46.70 with SMTP id c6mr30674719otd.28.1469004259375; Wed, 20 Jul 2016 01:44:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.36.203 with SMTP id k194ls2111896iok.43.gmail; Wed, 20 Jul 2016 01:44:18 -0700 (PDT) X-Received: by 10.36.228.8 with SMTP id o8mr6904014ith.11.1469004258547; Wed, 20 Jul 2016 01:44:18 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id w1si89218yww.7.2016.07.20.01.44.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 20 Jul 2016 01:44:18 -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 u6K8iHO1016395 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Wed, 20 Jul 2016 04:44:17 -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 u6K8iHwt016362; Wed, 20 Jul 2016 04:44:17 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX1/rArXNBjy1py/pLGYX19yuUIgLOfXQdSYZesRfgRFXDO83 oyhHqWSFc3MUN02ocHuo3M4vRbsDRW6EH0w6XYErtNS2geSdIYGC2T743DznwK7vfFQ+OMlD Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u6K8iHfA016340 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Wed, 20 Jul 2016 04:44:17 -0400 Received: from [88.128.80.86] (helo=[10.53.204.75]) by imap.math.ias.edu with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.80.1) (envelope-from ) id 1bPn73-0001US-2I; Wed, 20 Jul 2016 04:44:17 -0400 Subject: a new transport rule Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: multipart/signed; boundary="Apple-Mail=_0E4372F4-2402-42AA-B971-B8548C0C0D9D"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail From: Vladimir Voevodsky In-Reply-To: Date: Wed, 20 Jul 2016 10:44:13 +0200 Cc: "Prof. Vladimir Voevodsky" , Michael Shulman Message-Id: <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> <7DACC421-37E7-43CC-B61F-D6C5F99921DF@ias.edu> <1B8618C8-0499-4D96-BACF-9AA4623061B9@ias.edu> To: Homotopy Type Theory X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-07-20_06:,, 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-1607200102 X-IAS-PPS-PHISH: NO --Apple-Mail=_0E4372F4-2402-42AA-B971-B8548C0C0D9D Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 What I wrote with words on the last slide is best expressed, I think, by th= e following rule, where I omit the Gamma in front of each line: T type A:T B:T X:T |- P top P[A/X] type P[B/X] type R:P[B/X] e:Id0 T A B =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 trb0(R,*e,*X.P,*A,*B,*T):P[A/X] where "P top=E2=80=9D signifies that P is a syntactically correct type expression= but need not be well-formed (well typed, derivable) in Gamma, the =E2=80=9C*=E2=80=9D in front of an argument as in =E2=80=9C *e =E2=80= =9C signifies a non-essential argument, such arguments are ignored when two= expressions are compared for alpha-equivalence. This is semantically acceptable if Id0 is interpreted as exact equality. Syntactically we have the case when the well-formed sentences form somethin= g like an ideal in a ring because one operation has as one of its arguments= an element of the ambient structure (raw typing judgements). This came out stranger than I expected. Vladimir. --Apple-Mail=_0E4372F4-2402-42AA-B971-B8548C0C0D9D 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 iQEcBAEBCgAGBQJXjzndAAoJEH5eMY79Hy7t6MMIAKV0LYsRMUda8ObUstIS+oT1 3FQOTdOj2i8kk96zv65Jhy97ifStpfK4kxtQqW4EKpGVcTl7j4qOaKDpusuy/Xzn gPOt4es+IDB0psNVM3ZWq6Tnjk4S2BuAWsCiE8nBtPtZFAiYt2f9lGI1V0/YGO0J o2wKwQRTLmpVibg+oiVeQmij0Jd+VnQgW/Lzvv7oR8gXVgApqCynUyUF86E4Cog1 aKb8vsGh4XUM8bdgXK2zRACzAnJ+D3aJLT4twW2as3kefA2ovHKRA9mL79L6LZ0l ovSWtCWhockjJjupJuFKaOwaPOQuBtpeZvyysO+/u+o2Mjsq1ybRi16RSH4PXRU= =RtK8 -----END PGP SIGNATURE----- --Apple-Mail=_0E4372F4-2402-42AA-B971-B8548C0C0D9D-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.30.169 with SMTP id n38mr1845371otn.34.1469162127808; Thu, 21 Jul 2016 21:35:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.11.238 with SMTP id 101ls2671612oth.19.gmail; Thu, 21 Jul 2016 21:35:27 -0700 (PDT) X-Received: by 10.157.49.5 with SMTP id e5mr1767296otc.17.1469162127314; Thu, 21 Jul 2016 21:35:27 -0700 (PDT) Received: by 10.36.227.202 with SMTP id d193msith; Wed, 20 Jul 2016 02:10:48 -0700 (PDT) X-Received: by 10.36.54.199 with SMTP id l190mr3031910itl.0.1469005848420; Wed, 20 Jul 2016 02:10:48 -0700 (PDT) Return-Path: Received: from exchange.sandiego.edu (p24servers-nat.sandiego.edu. [192.195.154.5]) by gmr-mx.google.com with ESMTPS id ph9si174622pac.1.2016.07.20.02.10.48 for (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Wed, 20 Jul 2016 02:10:48 -0700 (PDT) Received-SPF: neutral (google.com: 192.195.154.5 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=192.195.154.5; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 192.195.154.5 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: from mail-lf0-f52.google.com (10.0.26.240) by exchange.sandiego.edu (10.0.25.30) with Microsoft SMTP Server (TLS) id 14.3.294.0; Wed, 20 Jul 2016 02:10:47 -0700 Received: by mail-lf0-f52.google.com with SMTP id l69so33672951lfg.1 for ; Wed, 20 Jul 2016 02:10:47 -0700 (PDT) X-Gm-Message-State: ALyK8tLmX2ItAjha6HbxzsG+Pz7zXua/GsoBgc8KluJsS1eYkxpc5D47jDHa/LEiMTd5BUf97AqUo7AFEIMzbw== X-Received: by 10.25.151.66 with SMTP id z63mr22680917lfd.159.1469005844730; Wed, 20 Jul 2016 02:10:44 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Wed, 20 Jul 2016 02:10:25 -0700 (PDT) In-Reply-To: <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> <7DACC421-37E7-43CC-B61F-D6C5F99921DF@ias.edu> <1B8618C8-0499-4D96-BACF-9AA4623061B9@ias.edu> <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> From: Michael Shulman Date: Wed, 20 Jul 2016 06:10:25 -0300 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] a new transport rule To: Vladimir Voevodsky CC: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Return-Path: shu...@sandiego.edu X-Originating-IP: [10.0.26.240] Can you give an example of such a P which becomes well-formed when A and B are substituted for X but is not well-formed with X as a variable? On Wed, Jul 20, 2016 at 5:44 AM, Vladimir Voevodsky wrote= : > What I wrote with words on the last slide is best expressed, I think, by = the following rule, where I omit the Gamma in front of each line: > > T type > A:T > B:T > X:T |- P top > P[A/X] type > P[B/X] type > R:P[B/X] > e:Id0 T A B > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94 > trb0(R,*e,*X.P,*A,*B,*T):P[A/X] > > where > > "P top=E2=80=9D signifies that P is a syntactically correct type expressi= on but need not be well-formed (well typed, derivable) in Gamma, > > the =E2=80=9C*=E2=80=9D in front of an argument as in =E2=80=9C *e =E2=80= =9C signifies a non-essential argument, such arguments are ignored when two= expressions are compared for alpha-equivalence. > > This is semantically acceptable if Id0 is interpreted as exact equality. > > Syntactically we have the case when the well-formed sentences form someth= ing like an ideal in a ring because one operation has as one of its argumen= ts an element of the ambient structure (raw typing judgements). > > This came out stranger than I expected. > > 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= email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.185.16 with SMTP id j16mr2720118vkf.2.1469181627306; Fri, 22 Jul 2016 03:00:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.7.230 with SMTP id 93ls2659228oto.22.gmail; Fri, 22 Jul 2016 03:00:26 -0700 (PDT) X-Received: by 10.200.56.7 with SMTP id q7mr2771734qtb.10.1469181626450; Fri, 22 Jul 2016 03:00:26 -0700 (PDT) Return-Path: Received: from mail-qt0-x233.google.com (mail-qt0-x233.google.com. [2607:f8b0:400d:c0d::233]) by gmr-mx.google.com with ESMTPS id d6si678224ywd.4.2016.07.22.03.00.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 22 Jul 2016 03:00:26 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::233 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c0d::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:400d:c0d::233 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-qt0-x233.google.com with SMTP id u25so58770144qtb.1 for ; Fri, 22 Jul 2016 03:00:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=wosUxdQ6DCCyt5DD639/JQKJDGHDENRdo0oc0NMNqUQ=; b=ou0PCglGADMMAmLIYnCeRFqJVd/3ZQ7DT66zg/3wYSbl6NZc+Pp7Jy4Lk9oUPaF6FY J68y0h4iH4QzBrKCfHAUJ5rgeaxFizp25/UQbKN+C0Eq7gccFW4SVXCi/9eJZwgO3Lyv e9CTnknKqpVZUzBYXotO3AFzZpXjQ0kbvGkYWhpUcUM2k5xfrf7mBt4ogAcvmnP+Y1UV 1EGR9Os9IUZ71Oge6kDfhdQodgYMdD/fbx+ztotTw2p8sCAz/nC5ESSCSyvaRycex4J0 xMe9PQlCXgQpYGBRVK09kGXooAni3xer5qGmoh11QGDfQ81mH/BhpJcFAGHCyp7J7TQj uXzg== X-Gm-Message-State: AEkoouvAkqLtLSKsEF3X9Y9tDJoX9IyRFGSCl4/pTjwNUlUjlri2nwTOUKtly0kr7SQr5K1rrmvTOC6uQ8pi5g== X-Received: by 10.200.42.69 with SMTP id l5mr4647089qtl.13.1469181625958; Fri, 22 Jul 2016 03:00:25 -0700 (PDT) MIME-Version: 1.0 Received: by 10.55.31.38 with HTTP; Fri, 22 Jul 2016 03:00:25 -0700 (PDT) In-Reply-To: References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> <7DACC421-37E7-43CC-B61F-D6C5F99921DF@ias.edu> <1B8618C8-0499-4D96-BACF-9AA4623061B9@ias.edu> <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> From: Andrej Bauer Date: Fri, 22 Jul 2016 12:00:25 +0200 Message-ID: Subject: Re: [HoTT] a new transport rule To: Michael Shulman Cc: Vladimir Voevodsky , Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman wrote: > Can you give an example of such a P which becomes well-formed when A > and B are substituted for X but is not well-formed with X as a > variable? Let T := Universe nat : Universe Nat type El nat = Nat 42 : Nat P(X) := Id (El X) 42 42 Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes: T := bool P(X) := Id (match X with true => Nat | false => (Nat -> Nat) end) 42 42 Now P(true) is well formed, but P(X) is not. With kind regards, Andrej From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.238.196 with SMTP id m187mr19228877vkh.7.1469519534096; Tue, 26 Jul 2016 00:52:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.63.221 with SMTP id i29ls6599412ote.17.gmail; Tue, 26 Jul 2016 00:52:13 -0700 (PDT) X-Received: by 10.237.52.67 with SMTP id w61mr19084178qtd.30.1469519533665; Tue, 26 Jul 2016 00:52:13 -0700 (PDT) Received: by 10.36.227.202 with SMTP id d193msith; Fri, 22 Jul 2016 04:08:48 -0700 (PDT) X-Received: by 10.36.67.147 with SMTP id s141mr994613itb.12.1469185728160; Fri, 22 Jul 2016 04:08:48 -0700 (PDT) Return-Path: Received: from exchange.sandiego.edu (p24servers-nat.sandiego.edu. [192.195.154.5]) by gmr-mx.google.com with ESMTPS id d201si1987481pfd.2.2016.07.22.04.08.48 for (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Fri, 22 Jul 2016 04:08:48 -0700 (PDT) Received-SPF: neutral (google.com: 192.195.154.5 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=192.195.154.5; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 192.195.154.5 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: from mail-lf0-f45.google.com (10.0.26.240) by exchange.sandiego.edu (10.0.25.30) with Microsoft SMTP Server (TLS) id 14.3.294.0; Fri, 22 Jul 2016 04:08:47 -0700 Received: by mail-lf0-f45.google.com with SMTP id g62so83107616lfe.3 for ; Fri, 22 Jul 2016 04:08:46 -0700 (PDT) X-Gm-Message-State: AEkoous1VozHEFtZnPsDCdMcCDbGxRHhrzUplPamPPKeZGdIGkiZzyZG5weTg5HW1Vy96MtavUx96AomNLvutA== X-Received: by 10.46.0.39 with SMTP id 39mr2391709lja.48.1469185724668; Fri, 22 Jul 2016 04:08:44 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Fri, 22 Jul 2016 04:08:24 -0700 (PDT) In-Reply-To: References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> <7DACC421-37E7-43CC-B61F-D6C5F99921DF@ias.edu> <1B8618C8-0499-4D96-BACF-9AA4623061B9@ias.edu> <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> From: Michael Shulman Date: Fri, 22 Jul 2016 08:08:24 -0300 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] a new transport rule To: Andrej Bauer CC: Vladimir Voevodsky , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Return-Path: shu...@sandiego.edu X-Originating-IP: [10.0.26.240] Thanks! I see. But I must admit I don't immediately see a use for such a transport rule (or how to give it any semantics). On Fri, Jul 22, 2016 at 7:00 AM, Andrej Bauer wrote: > On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman wrote: >> Can you give an example of such a P which becomes well-formed when A >> and B are substituted for X but is not well-formed with X as a >> variable? > > Let > > T := Universe > > nat : Universe > Nat type > El nat = Nat > 42 : Nat > > P(X) := Id (El X) 42 42 > > Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes: > > T := bool > > P(X) := Id (match X with true => Nat | false => (Nat -> Nat) end) 42 42 > > Now P(true) is well formed, but P(X) is not. > > With kind regards, > > Andrej > > -- > 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. From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.154.1 with SMTP id c1mr2581588wme.2.1469190181281; Fri, 22 Jul 2016 05:23:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.5.193 with SMTP id 184ls286618ljf.20.gmail; Fri, 22 Jul 2016 05:23:00 -0700 (PDT) X-Received: by 10.25.42.197 with SMTP id q188mr635323lfq.7.1469190180498; Fri, 22 Jul 2016 05:23:00 -0700 (PDT) Return-Path: Received: from mail-wm0-x243.google.com (mail-wm0-x243.google.com. [2a00:1450:400c:c09::243]) by gmr-mx.google.com with ESMTPS id o10si490841wme.0.2016.07.22.05.23.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 22 Jul 2016 05:23:00 -0700 (PDT) Received-SPF: pass (google.com: domain of mphm...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) client-ip=2a00:1450:400c:c09::243; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of mphm...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) smtp.mailfrom=mphm...@gmail.com Received: by mail-wm0-x243.google.com with SMTP id o80so5991090wme.0 for ; Fri, 22 Jul 2016 05:23:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc; bh=T+rcIrtN1A+cz9QJxPSamcpZyef/Pvih1jc6c8zLq1I=; b=NknrZkz5UdA4+fLuR2U+6CLGGoXhHipbcZujTCEEjlL8DLw0lls/VD4Tv7laoETp4L 32CBEixZiUG0ZIY5V6nRjFlXtK7SePbxA/DyZOIkxv5gFfGdA4DuOgcsBmMiqjp4KqQf ukD9xCqncjgVatFpnr4cIznmWikbzZFVwnyaCmg87EPkOluVTOVoOZk5M99tLVbuGj8A SinO79XuxuAijlFOaMd8pwXN5rh7V1/3d6703ifqgpKnUWD7jnKtfEIUw2JatrK5TYKj G2RU8Dq0c4BYpQNFGltGV6ZKBIOAO8WW2lQbyDeYk8us+PJHcXlwibWnAOWnKs7nCTjq tIVQ== X-Gm-Message-State: ALyK8tLePCQFUH2vs98JxSIlOQiik+vMIvjyCg49llbL51xgaxdKo3SC11QM7H4bjuNbqZkltXuCqSn55aEyug== X-Received: by 10.28.31.147 with SMTP id f141mr23649189wmf.69.1469190179373; Fri, 22 Jul 2016 05:22:59 -0700 (PDT) MIME-Version: 1.0 Sender: mphm...@gmail.com Received: by 10.194.133.5 with HTTP; Fri, 22 Jul 2016 05:22:40 -0700 (PDT) In-Reply-To: References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> <7DACC421-37E7-43CC-B61F-D6C5F99921DF@ias.edu> <1B8618C8-0499-4D96-BACF-9AA4623061B9@ias.edu> <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> From: =?UTF-8?Q?andr=C3=A9_hirschowitz?= Date: Fri, 22 Jul 2016 14:22:40 +0200 Message-ID: Subject: Re: [HoTT] a new transport rule To: Andrej Bauer Cc: Michael Shulman , Vladimir Voevodsky , Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a114bddfebfc8220538387eb3 --001a114bddfebfc8220538387eb3 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I looked for an example without universe/El and found P(X) ;=3D forall p: Id X a, Id p (refl a). It seems that the formula must involve a "type from term constructor" (here Id, or there El). andr=C3=A9 2016-07-22 12:00 GMT+02:00 Andrej Bauer : > On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman > wrote: > > Can you give an example of such a P which becomes well-formed when A > > and B are substituted for X but is not well-formed with X as a > > variable? > > Let > > T :=3D Universe > > nat : Universe > Nat type > El nat =3D Nat > 42 : Nat > > P(X) :=3D Id (El X) 42 42 > > Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes= : > > T :=3D bool > > P(X) :=3D Id (match X with true =3D> Nat | false =3D> (Nat -> Nat) end)= 42 42 > > Now P(true) is well formed, but P(X) is not. > > With kind regards, > > Andrej > > -- > 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. > --001a114bddfebfc8220538387eb3 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I looked for an example without universe/El=C2= =A0 and found

P(X) ;=3D forall p: Id X a, Id p (refl a).
It seems that the formula must involve a "type from term = constructor"
(here Id, or there El).

andr= =C3=A9

2= 016-07-22 12:00 GMT+02:00 Andrej Bauer <andrej...@andrej.com>:
On Wed, Jul 20, 20= 16 at 11:10 AM, Michael Shulman <= shu...@sandiego.edu> wrote:
> Can you give an example of such a P which becomes well-formed when A > and B are substituted for X but is not well-formed with X as a
> variable?

Let

=C2=A0T :=3D Universe

=C2=A0 nat : Universe
=C2=A0 Nat type
=C2=A0 El nat =3D Nat
=C2=A0 42 : Nat

=C2=A0P(X) :=3D Id (El X) 42 42

Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes:<= br>
=C2=A0T :=3D bool

=C2=A0 P(X) :=3D Id (match X with true =3D> Nat | false =3D> (Nat -&g= t; Nat) end) 42 42

Now P(true) is well formed, but P(X) is not.

With kind regards,

Andrej

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a114bddfebfc8220538387eb3-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.161.208 with SMTP id k199mr19263261vke.8.1469520454767; Tue, 26 Jul 2016 01:07:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.16.27 with SMTP id y27ls4141556ioi.41.gmail; Tue, 26 Jul 2016 01:07:33 -0700 (PDT) X-Received: by 10.66.170.208 with SMTP id ao16mr19875461pac.9.1469520453709; Tue, 26 Jul 2016 01:07:33 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id r127si2101288ywh.0.2016.07.26.01.07.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 26 Jul 2016 01:07:33 -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 u6Q87VqX009731 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Tue, 26 Jul 2016 04:07:31 -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 u6Q87U1v009725; Tue, 26 Jul 2016 04:07:30 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX19qydhfBq4RITRolReP6z+bEZTkfeRfSOqp12GP4njUbXDj V09DXTwYwB5fmIoN7Ogb2sp9OiIRU8cmEIVl3pfwMn3qtm8i0CstUtcMp6lf4JvCN2jynPma Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u6Q87U6v009724 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Tue, 26 Jul 2016 04:07:30 -0400 Received: from cbl217-132-141-136.bb.netvision.net.il ([217.132.141.136] helo=[10.100.102.4]) by imap.math.ias.edu with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.80.1) (envelope-from ) id 1bRxOk-0002A9-GM; Tue, 26 Jul 2016 04:07:30 -0400 Subject: Re: [HoTT] a new transport rule Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: multipart/signed; boundary="Apple-Mail=_915C9D4F-4F3B-4E5E-B948-F1A92ECD4BB5"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail From: Vladimir Voevodsky In-Reply-To: Date: Tue, 26 Jul 2016 11:07:27 +0300 Cc: "Prof. Vladimir Voevodsky" , Andrej Bauer , Homotopy Type Theory Message-Id: <92AF5F3E-2770-457F-A2DA-65C9A784660D@ias.edu> References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> <7DACC421-37E7-43CC-B61F-D6C5F99921DF@ias.edu> <1B8618C8-0499-4D96-BACF-9AA4623061B9@ias.edu> <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> To: Michael Shulman X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-07-26_03:,, 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-1607260097 X-IAS-PPS-PHISH: NO --Apple-Mail=_915C9D4F-4F3B-4E5E-B948-F1A92ECD4BB5 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii The semantics is the strict equality. > On Jul 22, 2016, at 2:08 PM, Michael Shulman wrote: >=20 > Thanks! I see. >=20 > But I must admit I don't immediately see a use for such a transport > rule (or how to give it any semantics). >=20 > On Fri, Jul 22, 2016 at 7:00 AM, Andrej Bauer wrot= e: >> On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman = wrote: >>> Can you give an example of such a P which becomes well-formed when A >>> and B are substituted for X but is not well-formed with X as a >>> variable? >>=20 >> Let >>=20 >> T :=3D Universe >>=20 >> nat : Universe >> Nat type >> El nat =3D Nat >> 42 : Nat >>=20 >> P(X) :=3D Id (El X) 42 42 >>=20 >> Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universe= s: >>=20 >> T :=3D bool >>=20 >> P(X) :=3D Id (match X with true =3D> Nat | false =3D> (Nat -> Nat) end)= 42 42 >>=20 >> Now P(true) is well formed, but P(X) is not. >>=20 >> With kind regards, >>=20 >> Andrej >>=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 > -- > 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=_915C9D4F-4F3B-4E5E-B948-F1A92ECD4BB5 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 iQEcBAEBCgAGBQJXlxo/AAoJEH5eMY79Hy7tVnUIAI6umu/v0kdxfRetsmW/xuuO /br8ut6TQYTe3dtBjbTgXFDA2J4tZoh5QZdo0JG5pgWpgojNQ/gfACQKxSr6ecuW 1HHvhvFlOZYSTO5GCXKKvy5kQqsJInX9mUBEjX5TlpTDQRD2TqHXR3zktwjoZmgm F6MzZlvddy4+vvJOrACpa8WKVoDdAMcK3hKbahr9b2ngSQKQ4mUgSlxNPSrDamXZ N0Nck33Dk3ZQD+Tk21qGo1CAqeuWMvj05ljI0smf965Ley8eCsv4sYki5igTZF3g 2XUEev4Gw+c054+wnFC5gjNk0udkJ/dl4mzsKk8t6WDotzqhTG0w+R9KwMDXGkk= =QVeG -----END PGP SIGNATURE----- --Apple-Mail=_915C9D4F-4F3B-4E5E-B948-F1A92ECD4BB5--