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