From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a9f:222c:: with SMTP id 41mr4708318uad.88.1588992377494; Fri, 08 May 2020 19:46:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:5441:: with SMTP id i62ls227518vkb.11.gmail; Fri, 08 May 2020 19:46:16 -0700 (PDT) X-Received: by 2002:a1f:2c3:: with SMTP id 186mr4759490vkc.17.1588992376113; Fri, 08 May 2020 19:46:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588992376; cv=none; d=google.com; s=arc-20160816; b=I0ZuSUPIWS8yWsXg6eVNoMDVae8BD5/LkEeQ02uvKZ9PIOE4XBLS+jpRajw+ai/OR6 bMvQEJet7qYPlVL+6gpQGzksgxEGA4ojFMiYEV8J/JBW+FbTNJT11aHW+W6pvk8cPJt8 OAw9kuYKqkWbpNPyNrl8UGUTZzM0BSxOtiTmLy/szol+EnvhMN2QLyqVudZxqSmqm2cV vWGy5RXvW8etXZ3MqIB4VMNGHumBpWCwCnaDT1xjEZTD6zF+oLbxAE1EM701vFqzGCDp 0cEDH+BdfC0ais4/AEu4/Zq8NsSntDk6POwACGlVRZx+Zriiwp68Guhsn12OjvPCVotZ WYJg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:ironport-sdr; bh=yy91DU60Hwxpxq5viudCTj4gV24zMoPnTWrkJFIF9Jc=; b=z7KkQUsZ9m/RH6KfMBKJm6goICpUoeNI9dt76LRAX/A3VgfSoT+UPNfudF65WzmVnw MGnRvz8qi9HLUH0NdTwj5V1RN0pCcQBhJOUQTf1RIInJu+/iY4qo7N4umpKPCoIq5+3Y 9jBc0Pw8IsMRmLIQLWQdf0WLR/++PNhfVRPs9ZagTu1R78Ox1KWfBFC8rpY5qDVyUQNd UFfEcl3B+nMv3mmMfgTJW5cxotHCzyhTDCpWUAiQbxGoXUFziOP89DID+CXnZoijlhen 7ZWYGhB1E+duVGlAc/CnqHvf36l080c8jTVc/ou7lMJhJ8Db2Ua+mO75u5C/wG/KMwRP 2Pmw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail6.uqam.ca (mail.uqam.ca. [132.208.246.231]) by gmr-mx.google.com with ESMTP id v22si306007vsl.1.2020.05.08.19.46.15 for ; Fri, 08 May 2020 19:46:16 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) client-ip=132.208.246.231; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: W/EBjQ1Wf3L6p9G4aBz803jC4LpJ2TS5GIl10hHkL6IaAk59QezKyO4aMKncm3zsabVrFcjiZR SttzHEM4Y5TS9Qk0vkq1p74+xwxkDhBupWLPXHSRn6iBP88jHi5BnabdOG34Z4IEp0mSv6Or0z mNCRoPgY+bDEkIJRRdTbbXXohsmvR1+Kr1y2jL/V5bWnzYZnXZW0CZ992+AfnGFyQcCajB02M7 NU+oyNkN9n6UIVlUzXjyhGzs3UTRxqKtgsK99mxaXR1CXAy8ORH4Qh42QqlgvIzo8aETNSXdn+ g1A= X-IronPort-AV: E=Sophos;i="5.73,370,1583211600"; d="scan'208";a="10545243" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.216.70]) by mail6.uqam.ca with ESMTP; 08 May 2020 22:46:15 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Message.gst.uqam.ca ([169.254.1.218]) with mapi id 14.03.0439.000; Fri, 8 May 2020 22:46:14 -0400 From: =?utf-8?B?Sm95YWwsIEFuZHLDqQ==?= To: Steve Awodey CC: Thomas Streicher , David Roberts , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LWAALJlgP//xKOFgABhQICAAHDSgIAAmhfJgACD3wD//+pSdw== Date: Sat, 9 May 2020 02:46:14 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F5565@Pli.gst.uqam.ca> References: <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca>,<1044A78D-8F16-4856-9B50-9B7FB7EF579A@gmail.com> In-Reply-To: <1044A78D-8F16-4856-9B50-9B7FB7EF579A@gmail.com> Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.80] Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: base64 MIME-Version: 1.0 RGVhciBTdGV2ZSwKClRoYW5rIHlvdSBmb3Igc3RyZXNzaW5nIHRoZSBkaXN0aW5jdGlvbiBiZXR3 ZWVuIGNvbXB1dGluZyBhbmQgcHJvdmluZy4KSSB3YXMgdGhpbmtpbmcgYWJvdXQgdGhlIGNvbXB1 dGF0aW9uIG9mIGEgbmF0dXJhbCBudW1iZXIgYnkgcmVkdWN0aW9uIG9mIHRlcm1zLiAKSSBtdXN0 IGJlIGNvbmZ1c2VkLgoKQnV0IGluIHR5cGUgdGhlb3J5LCBpcyBpdCBub3QgdHJ1ZSB0aGF0IGV2 ZXJ5IHByb29mIGlzIGEgY29tcHV0YXRpb24/CgpCZXN0LApBbmRyw6kKCgoKCgpfX19fX19fX19f X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fCkZyb206IFN0ZXZlIEF3b2RleSBbc3RldmUu Li5AZ21haWwuY29tXQpTZW50OiBGcmlkYXksIE1heSAwOCwgMjAyMCA3OjQ0IFBNClRvOiBKb3lh bCwgQW5kcsOpCkNjOiBUaG9tYXMgU3RyZWljaGVyOyBEYXZpZCBSb2JlcnRzOyBUaG9yc3RlbiBB bHRlbmtpcmNoOyBNaWNoYWVsIFNodWxtYW47IFN0ZXZlIEF3b2RleTsgaG9tb3RvcHl0Li4uQGdv b2dsZWdyb3Vwcy5jb20KU3ViamVjdDogUmU6IFtIb1RUXSBJZGVudGl0eSB2ZXJzdXMgZXF1YWxp dHkKCkRlYXIgQW5kcsOpLAoKSSB3b3VsZCBwcmVmZXIgdG8gc2F5IHRoYXQgdCBjdXJyZW50IHN5 c3RlbXMgb2YgdHlwZSB0aGVvcnkgaGF2ZSBmYWlsZWQgdG8gKmNvbXB1dGUqIHBpXzQoU14zKSwg c28gYXMgbm90IHRvIGRpbWluaXNoIHRoZSB2YWx1ZSBvZiBHdWlsbGF1bWXigJlzIGJlYXV0aWZ1 bCBwcm9vZiwgd2hpY2ggaGFzIGV2ZW4gYmVlbiBmb3JtYWxseSBjaGVja2VkIGluIGRpZmZlcmVu dCBwcm9vZiBhc3Npc3RhbnRzLgpZb3Ugb2YgY291cnNlIGtub3cgdGhlIGRpZmZlcmVuY2UgYmV0 d2VlbiBwcm92aW5nIHNvbWV0aGluZyBpbiB0eXBlIHRoZW9yeSBhbmQgY29tcHV0aW5nIHRoZSB2 YWx1ZSBvZiBhIHRlcm0sIGJ1dCBzb21lIHJlYWRlcnMgbWF5IG5vdC4KCkJlc3Qgd2lzaGVzLAoK U3RldmUKClBzOiBJbiBteSBvcGluaW9uLCBmb3Igd2hhdCBpdOKAmXMgd29ydGgsIG1ha2luZyBh IHN5c3RlbSB0aGF0IHdpbGwgY29tcHV0ZSB0aGUgdmFsdWUgb2YgQnJ1bmVyaWXigJlzIGNvbnN0 YW50IGlzIGFuIGVuZ2luZWVyaW5nIHByb2JsZW0sIG5vdCBhIG1hdGhlbWF0aWNhbCBvbmUuIFdo aWNoIGlzIG5vdCB0byBzYXkgaXQgd291bGQgbm90IGJlIGFuIGltcG9ydGFudCBhZHZhbmNlIQoK PiBPbiBNYXkgOCwgMjAyMCwgYXQgMTc6MDYsIEpveWFsLCBBbmRyw6kgPGpveWFsLi4uQHVxYW0u Y2E+IHdyb3RlOgo+Cj4g77u/RGVhciBUaG9tYXMsCj4KPiBZb3UgYXJlIHJpZ2h0LCB0aGUgZXF1 YWxpdHkgb2Ygb2JqZWN0cyBpbiBhIEdyb3RoZW5kaWVjayBmaWJyYXRpb24gaXMganVkZ2VtZW50 YWwuCj4KPiBQcm9wb3NpdGlvbmFsIGVxdWFsaXR5IG9mIHR5cGUgdGhlb3J5IGhhcyBiZWVuIHN0 dWRpZWQgYSBsb3QgZHVyaW5nIHRoZSBsYXN0IGRlY2FkZXMuCj4gSSBmZWVsIHF1aXRlIGNvbmZv cnRhYmxlIHdpdGggaXQsIHdpdGggdGhlIGhvbW90b3B5IGludGVycHJldGF0aW9uIGFuZCB0aGUg dW5pdmFsZW5jZSBwcmluY2lwbGUsIGV0Yy4KPiBJIGNvbmZlc3MgdGhhdCBJIGFtIG11Y2ggbGVz cyBhdCBlYXNlIHdpdGgganVkZ21lbnRhbCBlcXVhbGl0eSBhbmQgdGhlIHN5bnRheCBvZiB0eXBl IHRoZW9yeS4KPiBVbnRpbCBub3csIHR5cGUgdGhlb3J5IGhhcyBmYWlsZWQgdG8gcHJvdmUgdGhh dCBwaV80KFNeMyk9Q18yLgo+IElzIGl0IHRoZSBzeW1wdG9tIG9mIGEgZnVuZGFtZW50YWwgcHJv YmxlbT8KPiBJcyBpdCBiZWNhdXNlIHRoZSByZWR1Y3Rpb24gYWxnb3JpdG1zIGFyZSBub3Qgb3B0 aW1hbD8KPiBPciBiZWNhdXNlIGNvbXB1dGVycyBhcmUgbm90IHBvd2VyZnVsIGVub3VnaD8KPiBX aGF0IGlzIHRoZSBhYnN0cmFjdCB0aGVvcnkgb2YgdGVybXMgcmVkdWN0aW9uIGluIHR5cGUgdGhl b3J5Pwo+IEkgYXBvbG9naXNlIGZvciBteSBpZ25vcmFuY2UuCj4KPiBCZXN0LAo+IEFuZHLDqQo+ Cj4gX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX3QKPiBGcm9tOiBUaG9t YXMgU3RyZWljaGVyIFtzdHJlLi4uQG1hdGhlbWF0aWsudHUtZGFybXN0YWR0LmRlXQo+IFNlbnQ6 IEZyaWRheSwgTWF5IDA4LCAyMDIwIDI6NDAgQU0KPiBUbzogRGF2aWQgUm9iZXJ0cwo+IENjOiBK b3lhbCwgQW5kcsOpOyBUaG9yc3RlbiBBbHRlbmtpcmNoOyBNaWNoYWVsIFNodWxtYW47IFN0ZXZl IEF3b2RleTsgaG9tb3RvcHl0Li4uQGdvb2dsZWdyb3Vwcy5jb20KPiBTdWJqZWN0OiBSZTogW0hv VFRdIElkZW50aXR5IHZlcnN1cyBlcXVhbGl0eQo+Cj4gRGVhciBSb2JlcnQsCj4KPiBpbiB3aGF0 IEkgc2FpZCBJIGRpZG4ndCBtZWFuIHNldCB0aGVvcnkgbGl0ZXJhbGx5LiBJIHdhcyByYXRoZXIg cmVmZXJyaW5nCj4gdG8gYWxsIGtpbmRzIG9mIGNhdGVnb3JpY2FsIGxvZ2ljIHdoZXJlIGVxdWFs aXR5IGlzIGludGVycHJldGVkIGFzCj4gKGZpYmVyd2lzZSkgZGlhZ29uYWwgbGlrZSAodHJhZGl0 aW9uYWwpIHRvcG9zIHRoZW9yeSBpbiBwYXJ0aWN1bGFyLgo+IFRoZXNlIGtpbmRzIG9mIGdhZGdl dHMgYWxsIGhhdmUgdGhlIGFkdmFudGFnZSB0aGF0ICJTZXQiIGlzIG5vdCBydWxlZAo+IG91dCBh cyBhIG1vZGVsLgo+Cj4gU2luY2UgdGhlIGRpYWdvbmFsIGlzIGhhcmRseSBldmVyIGZpYnJhbnQg SG9UVCBydWxlcyBvdXQgU2V0IGFzIGEgbW9kZWwuCj4KPiBCdXQgdGhpcyBpcyBub3QgbXkgbWFp biBwcm9ibGVtLiBNeSBtYWluIHByb2JsZW0gaXMgdGhhdCB0aGVyZSBpcyBhdCBsZWFzdAo+IG9u ZSBhcmVhIG9mIGNhdGVnb3J5IHRoZW9yeSB3aGVyZSBvbmUgaGFzIHRvIHNwZWFrIGFib3V0IGVx dWFsaXR5IG9mCj4gb2JqZWN0cyBhbmQgdGhlc2UgYXJlIEdyb3RoZW5kaWVjayBmaWJyYXRpb25z LiBBbmQgdGhlc2UgYXJlIGludHJpbnNpYwo+IGZvciBkb2luZyB0b3BvcyB0aGVvcnkgb3ZlciBn ZW5lcmFsIGJhc2UgdG9wb3Nlcy4KPiAoVGhhdCBJIHJlYWxseSBsaWtlIHRoZW0gaXMsIGFkbWl0 dGVkbHksIGFsc28gYW4gaW1wb3J0YW50IHJlYXNvbiBmb3IgbWUKPiBub3QgYmVpbmcgcmVhZHkg dG8gZ2l2ZSB0aGVtIHVwISBBbmQgZm9yIHJlYXNvbnMgb2YgcGVyc29uYWwgYW5kCj4gY3VsdHVy YWwgImFudGFnb25pc21zIiB0aGV5IGFyZSBub3QgdmVyeSBwb3B1bGFyIGFtb25nIHRoZSBtYWpv cml0eSBvZgo+IGNhdGVnb3J5IHRoZW9yaXN0cy4uLiBUaHVzLCB0aGVyZSBhcmUgbWFueSBwZW9w bGUgd2hvIHdvdWxkIG5vdCBiZSB0b28KPiBzYWQgYWJvdXQgd29ya2luZyBpbiBhIGZyYW1ld29y ayBub3QgYWxsb3dpbmcgdG8gc3BlYWsgYWJvdXQgdGhlbS4pCj4gQnV0IEkgd2FudCB0byBlbXBo YXNpemUgdGhhdCByZWFsIG1hc3RlcnMgb2YgaW5maW5pdGUgZGltZW5zaW9uYWwKPiBjYXRlZ29y aWVzIGRvIG5vdCBoYXZlIHRoZSBmYWludGVzdCBwcm9ibGVtIHNwZWFraW5nIGFib3V0IGVxdWFs aXR5Cj4gd2hlbiBzcGVha2luZyBhYm91dCBpbmZpbml0ZSBkaW1lbnNpb25hbCB2ZXJzaW9ucyBv ZiBHcm90aGVuZGllY2sKPiBmaWJyYXRpb25zISkKPgo+IFRob3VnaCAodHJhZGl0aW9uYWwpIHRv cG9zIHRoZW9yeSBjYW4gYmUgZGV2ZWxvcGVkIG92ZXIgZmFpcmx5IGdlbmVyYWwKPiB0b3Bvc2Vz IGFuZCB0aGlzLCBhdCBsZWFzdCBwaGlsb3NvcGhpY2FsbHksIGlzIGFuIGltcG9ydGFudCBhc3Bl Y3Qgb25lCj4gY2Fubm90IGRlbnkgdGhhdCBtb3N0IHRvcG9zZXMgb2YgaW50ZXJlc3QgaGVhdmls eSByZWx5IG9uIFNldCwgYmUgdGhleQo+IG9mIHRoZSBHcm90aGVuZGllY2sga2luZCBvciBiZSB0 aGV5IG9mIHRoZSByZWFsaXphYmlsaXR5IGtpbmQhCj4KPiBUaG9tYXMKPgo+IFBTICBBYm92ZSBJ IHB1dCBTZXQgaW50byBpbnZlcnRlZCBjb21tYXMgYmVjYXVzZSB0aGUgbG9naWNpYW4gaW4gbWUK PiBmaW5kcyBpdCBhbXVzaW5nIHRvIHNwZWFrIGFib3V0ICJ0aGUiIGNhdGVnb3J5IG9mIHNldHMg d2hpY2ggaXMKPiBub3RoaW5nIGJ1dCBhbiBpbGx1c2lvbi4uLiBFdmVuIHRoZSBub3dhZGF5cyBu b3Qgc28gbGl0dGxlIG51bWJlciBvZgo+IGFkaGVyZW50cyBvZiB0aGUgIm11bHRpdmVyc2UiIHZp ZXcgb2Ygc2V0IHRoZW9yeSB3b3VsZCBzaGFyZSB0aGlzIHZpZXchCj4gQnV0IGV2ZW4gdGhlICJ1 bml2ZXJzZSIgdmlldyBpcyBub3RoaW5nIGJ1dCBhbiBpZGVvbG9neSBiZWNhdXNlIHNpbmNlCj4g Q29oZW4gc2V0IHRoZW9yeSBpcyBtYWlubHkgYSBidXNpbmVzcyBvZiBjb25zdHJ1Y3RpbmcgZGlm ZmVyZW50IG1vZGVscwo+IHZpYSBmb3JjaW5nLgo+IFRodXMsIHNpbmNlIFNldCBpcyAoc29ydCBv ZikgYW4gaWxsdXNpb24gaXQgaXMgaW1wb3J0YW50IHRvIGRvIHRvcG9zZXMKPiBvdmVyIGFyYml0 cmFyeSBiYXNlcyBmb3Igd2hpY2ggcHVycG9zZSBvbmUgbmVlZHMgR3JvdGhlbmRpZWNrIGZpYnJh dGlvbnMKPiB3aGljaCBkbyBub3QgbWFrZSBzZW5zZSB3aXRob3V0IGVxdWFsaXR5IG9mIG9iamVj dHMuCj4KPiBQUFMgU29tZSBwZW9wbGUgbWlnaHQgZ2V0IHRoZSBpbXByZXNzaW9uIEkgYW0gYSAi Y3J5cHRvIHNldAo+IHRoZW9yaXN0Ii4gTm90aGluZyBjb3VsZCBiZSBtb3JlIHdyb25nLiBJIGFt IGFudGktaWRlb2xvZ2ljYWwgYW5kCj4gcGx1cmFsaXN0IGFuZCBJIGxpa2UgImRldmlhdGluZyIg aWRlYXMuIEJ1dCBJIGFtIGludGVyZXN0ZWQgaW4KPiBjYWxpYnJhdGluZyB3aGF0IG9uZSBuZWVk cyBmb3Igd2hpY2ggZ29hbHMuIFdoYXQgSSBhbSBhbGxlcmdpYyBhdCBpcwo+IGlkZW9sb2dpY2Fs IHBvc2l0aW9ucyB3aGljaCB3YW50IHRvIGZvcmJpZCBzb21lb25lIGRvaW5nIGNlcnRhaW4KPiB0 aGluZ3MgYmVjYXVzZSB0aGV5IGRvIG5vdCBmaXQgdG8gc29tZSBpZGVvbG9naWNhbCBwb3NpdGlv bnMuLi4KPiBBbmQgb25lIGhhcyB0byBhY2NlcHQgdGhhdCBub3QgYWxsIGNvbWJpbmF0aW9ucyBh cmUgcG9zc2libGUuIFRodXMKPiBwbHVyYWxpc3QgaXMgYmV0dGVyIHRvIGluZWdyaXN0IQo+Cj4g LS0KPiBZb3UgcmVjZWl2ZWQgdGhpcyBtZXNzYWdlIGJlY2F1c2UgeW91IGFyZSBzdWJzY3JpYmVk IHRvIHRoZSBHb29nbGUgR3JvdXBzICJIb21vdG9weSBUeXBlIFRoZW9yeSIgZ3JvdXAuCj4gVG8g dW5zdWJzY3JpYmUgZnJvbSB0aGlzIGdyb3VwIGFuZCBzdG9wIHJlY2VpdmluZyBlbWFpbHMgZnJv bSBpdCwgc2VuZCBhbiBlbWFpbCB0byBIb21vdG9weVQuLi5AZ29vZ2xlZ3JvdXBzLmNvbS4KPiBU byB2aWV3IHRoaXMgZGlzY3Vzc2lvbiBvbiB0aGUgd2ViIHZpc2l0IGh0dHBzOi8vZ3JvdXBzLmdv b2dsZS5jb20vZC9tc2dpZC9Ib21vdG9weVR5cGVUaGVvcnkvOEM1Nzg5NEM3NDEzRjA0QTk4RERG NTYyOUZFQzkwQjE2NTJGNTRDQyU0MFBsaS5nc3QudXFhbS5jYS4K