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