From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.8.21 with SMTP id 21mr1402862oty.111.1476342875006; Thu, 13 Oct 2016 00:14:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.46.248 with SMTP id w111ls5267241ota.38.gmail; Thu, 13 Oct 2016 00:14:34 -0700 (PDT) X-Received: by 10.237.59.118 with SMTP id q51mr1349211qte.64.1476342874518; Thu, 13 Oct 2016 00:14:34 -0700 (PDT) Return-Path: Received: from data.hamecon.telecom.uqam.ca (mail2.uqam.ca. [132.208.246.165]) by gmr-mx.google.com with ESMTP id i84si781537ywg.0.2016.10.13.00.14.34 for ; Thu, 13 Oct 2016 00:14:34 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.165 as permitted sender) client-ip=132.208.246.165; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL...@uqam.ca Authentication-Results: data2.hamecon.telecom.uqam.ca; spf=None smtp.mailfrom=joyal...@uqam.ca; spf=None smtp.helo=postm...@Message.gst.uqam.ca Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of joyal...@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="joyal...@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of postm...@Message.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="postm...@Message.gst.uqam.ca"; x-conformance=spf_only X-Cloudmark-SP-Filtered: true X-Cloudmark-SP-Result: =?us-ascii?q?v=3D2=2E1_cv=3DWODfJiYR_c=3D1_sm=3D2_tr?= =?us-ascii?q?=3D0_a=3DzdVg5ADNf/sAC0uRWyjItQ=3D=3D=3A17?= =?us-ascii?q?_a=3DSgJDDHH=5FwjgA=3A10_a=3DCH0kA5CcgfcA=3A10_a=3D4RBUngkUAAA?= =?us-ascii?q?A=3A8_a=3DpGLkceISAAAA=3A8?= =?us-ascii?q?_a=3DKBmCG8goAAAA=3A8_a=3D1XWaLZrsAAAA=3A8_a=3DBI1i3DDHQTucQZU?= =?us-ascii?q?Cu5QA=3A9?= =?us-ascii?q?_a=3DeW6zNlXIbvEVR2q1=3A21_a=3DqA1UdxRwkEjB4qFV=3A21_a=3DmFyHD?= =?us-ascii?q?rcPJccA=3A10?= =?us-ascii?q?_a=3Dc4S9Whzb7AQA=3A10_a=3DWwjVK5tPuAIA=3A10_a=3D0i5-nK=5FWe?= =?us-ascii?q?=5FdFCmV1mkMA=3A9?= =?us-ascii?q?_a=3D507jjP5ERfGZwCM6=3A21_a=3DbHX5D6vYCIUgnuiN=3A21_a=3DAj8YY?= =?us-ascii?q?bUwShRlGf6B=3A21?= =?us-ascii?q?_a=3D=5FW=5FS=5F7VecoQA=3A10_a=3Dfrz4AuCg-hUA=3A10_a=3D=5FsbA2?= =?us-ascii?q?Q-Kp09kWB8D3iXc=3A22?= =?us-ascii?q?_a=3D6kGIvZw6iX1k4Y-7sg4=5F=3A22_a=3Dk5BapZiL03w2Mc6BGfFH=3A22?= =?us-ascii?q?_a=3DnJcEw6yWrPvoIXZ49MH8=3A22?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2CEAgDmMv9X/9H20IRcDgiDITUBAQEBA?= =?us-ascii?q?R1XfAcBgzegeodbjFmCChwBCoV6AhqBYjgUAQIBAQEBAQEBXieEYQEBAQMBTis?= =?us-ascii?q?FCwIBCA0EBAEBCx0FAgIfEAEUCQgCBAEHBgEEAQcVBIgVAw8IDph1nSsIiQMNg?= =?us-ascii?q?3IBAQEBAQEBAQEBAQEBAQEBAQEBAQEdig2BBYJHCIFKEQEeNIJKMIIvBZQohSU?= =?us-ascii?q?1hieGSgGFR4dEhXWIZYQUg38PDzYlhFQ7cgEGhj2BIAF/AQEB?= X-IPAS-Result: =?us-ascii?q?A2CEAgDmMv9X/9H20IRcDgiDITUBAQEBAR1XfAcBgzegeod?= =?us-ascii?q?bjFmCChwBCoV6AhqBYjgUAQIBAQEBAQEBXieEYQEBAQMBTisFCwIBCA0EBAEBC?= =?us-ascii?q?x0FAgIfEAEUCQgCBAEHBgEEAQcVBIgVAw8IDph1nSsIiQMNg3IBAQEBAQEBAQE?= =?us-ascii?q?BAQEBAQEBAQEBAQEdig2BBYJHCIFKEQEeNIJKMIIvBZQohSU1hieGSgGFR4dEh?= =?us-ascii?q?XWIZYQUg38PDzYlhFQ7cgEGhj2BIAF/AQEB?= X-IronPort-AV: E=Sophos;i="5.31,339,1473134400"; d="scan'208,217";a="162615393" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.246.209]) by data2.hamecon.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 13 Oct 2016 03:14:32 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.160]) by Message.gst.uqam.ca ([169.254.1.157]) with mapi id 14.02.0387.000; Thu, 13 Oct 2016 03:14:32 -0400 From: =?gb2312?B?Sm95YWwsIEFuZHKopg==?= To: Vladimir Voevodsky , Peter LeFanu Lumsdaine CC: Martin Escardo , "HomotopyT...@googlegroups.com" Subject: RE: [HoTT] Re: Joyal's version of the notion of equivalence Thread-Topic: [HoTT] Re: Joyal's version of the notion of equivalence Thread-Index: AQHSIPWqfQhwWQWowESuICWJpmirZ6Cd9QCAgACq52CAAhgRAP//vsuygAOvM4CAALYMgIAA0gcAgABSq9M= Date: Thu, 13 Oct 2016 07:14:32 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B138BD0019@Pli.gst.uqam.ca> References: <963893a3-bfdf-d9bd-8961-19bab69e0f7c@googlemail.com> <25c7daf7-8c0f-97de-7d3d-34851bf50a98@googlemail.com> <8C57894C7413F04A98DDF5629FEC90B138BCC04E@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B138BCCE8B@Pli.gst.uqam.ca> , In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: multipart/alternative; boundary="_000_8C57894C7413F04A98DDF5629FEC90B138BD0019Pligstuqamca_" MIME-Version: 1.0 --_000_8C57894C7413F04A98DDF5629FEC90B138BD0019Pligstuqamca_ Content-Type: text/plain; charset="gb2312" Content-Transfer-Encoding: base64 RGVhciBWbGFkaW1pciwNCg0KSSBjb21wbGV0ZWx5IGFncmVlIHdpdGggeW91Lg0KDQpBbmRyqKYN Cl9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fDQpGcm9tOiBob21vdG9weXQuLi5AZ29v Z2xlZ3JvdXBzLmNvbSBbaG9tb3RvcHl0Li4uQGdvb2dsZWdyb3Vwcy5jb21dIG9uIGJlaGFsZiBv ZiBWbGFkaW1pciBWb2V2b2Rza3kgW3ZsYWQuLi5AaWFzLmVkdV0NClNlbnQ6IFdlZG5lc2RheSwg T2N0b2JlciAxMiwgMjAxNiA2OjE3IFBNDQpUbzogUGV0ZXIgTGVGYW51IEx1bXNkYWluZQ0KQ2M6 IFByb2YuIFZsYWRpbWlyIFZvZXZvZHNreTsgTWFydGluIEVzY2FyZG87IEpveWFsLCBBbmRyqKY7 IEhvbW90b3B5VC4uLkBnb29nbGVncm91cHMuY29tDQpTdWJqZWN0OiBSZTogW0hvVFRdIFJlOiBK b3lhbCdzIHZlcnNpb24gb2YgdGhlIG5vdGlvbiBvZiBlcXVpdmFsZW5jZQ0KDQpJIHRoaW5rIHRo ZSBjbGVhcmVzdCBmb3JtdWxhdGlvbiBpcyBteSBvcmlnaW5hbCBvbmUgLSBhcyB0aGUgY29uZGl0 aW9uIG9mIGNvbnRyYWN0aWJpbGl0eSBvZiB0aGUgaC1maWJlcnMuDQoNClRoaXMgaXMgYWxzbyB0 aGUgZmlyc3QgZm9ybSBpbiB3aGljaCBpdCB3YXMgaW50cm9kdWNlZCBhbmQgdGhlIGZpcnN0IGV4 cGxpY2l0IGZvcm11bGF0aW9uIGFuZCBwcm9vZiBvZiB0aGUgZmFjdCB0aGF0IGl0IGlzIGEgcHJv cG9zaXRpb24uDQoNClZsYWRpbWlyLg0KDQoNCg0KDQoNCk9uIE9jdCAxMiwgMjAxNiwgYXQgNTo0 NSBBTSwgUGV0ZXIgTGVGYW51IEx1bXNkYWluZSA8cC5sLmx1Li4uQGdtYWlsLmNvbTxtYWlsdG86 cC5sLmx1Li4uQGdtYWlsLmNvbT4+IHdyb3RlOg0KDQo+IEFsdGhvdWdoIEkgY2FuIHNlZSBmb3Jt YWwgcHJvb2ZzIHRoYXQgSm95YWwtZXF1aXZhbGVuY2UgaXMgYSBwcm9wb3NpdGlvbiAob3IgaC1w cm9wb3NpdGlvbiksIEkgYW0gc3RpbGwgdHJ5aW5nIHRvIGZpbmQgdGhlIGJlc3QgZm9ybWFsIHBy b29mIHRoYXQgdW5jb3ZlcnMgdGhlIGVzc2VuY2Ugb2YgdGhpcyBmYWN0LiBUaGlzIGlzIHdoeSBJ IGFza2VkIHRoZSBxdWVzdGlvbiBvZiB3ZXJlIHRoaXMgZm9ybXVsYXRpb24gb2YgZXF1aXZhbGVu Y2UgY29tZXMgZnJvbS4NCg0KTGlrZSBBbmRyqKYgc3VnZ2VzdGVkLCBJIGZlZWwgdGhlIG5pY2Vz dCB2aWV3cG9pbnQgaXMgdGhlIGZhY3QgdGhhdCB0aGUgobBmcmVlICih3iwxKS1jYXRlZ29yeSBv biBhIEpveWFsLWVxdWl2YWxlbmNlobEgaXMgY29udHJhY3RpYmxlLiAgQXQgbGVhc3QgaW4gdGVy bXMgb2YgaW50dWl0aW9uLCB0aGUgY29uY2VwdHVhbGx5IGNsZWFyZXN0IGFyZ3VtZW50IEkga25v dyBmb3IgdGhhdCBpcyBhcyBmb2xsb3dzLg0KDQpMb29rIGF0IHRoZSAqod4tZ3JvdXBvaWRpZmlj YXRpb24qIG9mIHRoaXMgZnJlZSAood4sMSktY2F0ZWdvcnksIGNvbnNpZGVyZWQgYXMgYSBzcGFj ZS4gIFRoaXMgaXMgYSBjZWxsIGNvbXBsZXggd2hpY2ggd2UgY2FuIGVhc2lseSBwaWN0dXJlOiB0 d28gcG9pbnRzIHgsIHksIHRocmVlIHBhdGhzIGYsIGcsIGcnIGJldHdlZW4geCBhbmQgeSwgYW5k IDItY2VsbHMgZ2l2aW5nIGhvbW90b3BpZXMgZiB+IGcsIGYgfiBnJy4gIEl0oa9zIHZlcnkgY2xl YXIgZ2VvbWV0cmljYWxseSB0aGF0IHRoaXMgaXMgY29udHJhY3RpYmxlLg0KDQpCdXQgoaogdGhl IKGwZnJlZSAood4sMSktY2F0ZWdvcnkgb24gYSBKb3lhbCBlcXVpdmFsZW5jZaGxIGlzIGFscmVh ZHkgYW4god4tZ3JvdXBvaWQgoaogYW5kIKHeLWdyb3Vwb2lkaWZpY2F0aW9uIGlzIGlkZW1wb3Rl bnQsIHNpbmNlIGdyb3Vwb2lkcyBhcmUgYSBmdWxsIHN1YmNhdGVnb3J5LiAgU28gdGhlIG9yaWdp bmFsICih3iwxKS1jYXRlZ29yeSBpcyBlcXVpdmFsZW50IHRvIGl0cyBncm91cG9pZGlmaWNhdGlv biwgc28gaXMgY29udHJhY3RpYmxlLg0KDQpUaGUgc2FtZSBhcHByb2FjaCB3b3JrcyBmb3Igc2Vl aW5nIHdoeSBoYWxmLWFkam9pbnQgZXF1aXZhbGVuY2VzIGFyZSBnb29kLCBidXQgbm9uLWFkam9p bnQgYW5kIGJpLWFkam9pbnQgZXF1aXZhbGVuY2VzIGFyZSBub3QuICBTbyBhcyByZWdhcmRzIGlu dHVpdGlvbiwgSSB0aGluayB0aGlzIGlzIHZlcnkgbmljZS4gIEhvd2V2ZXIsIEkgc3VzcGVjdCB0 aGF0IGlmIG9uZSBsb29rcyBhdCBhbGwgdGhlIHdvcmsgdGhhdCBnb2VzIGludG8gc2V0dGluZyB1 cCB0aGUgZnJhbWV3b3JrIG5lZWRlZCwgdGhlbiBzb21ld2hlcmUgb25lIHdpbGwgaGF2ZSBhbHJl YWR5IHVzZWQgc29tZSBmb3JtIG9mIKGwZXF1aXZhbGVuY2UgaXMgYSBwcm9wb3NpdGlvbqGxLiAg U28gdGhpcyBpcyBwZXJoYXBzIGEgbGl0dGxlIHVuc2F0aXNmYWN0b3J5IGZvcm1hbGx5LCBhcyBp dCAoYSkgbmVlZHMgYSBsb3Qgb2YgYmFja2dyb3VuZCwgYW5kIChiKSBtYXkgbmVlZCB0byByZWx5 IG9uIHNvbWUgbW9yZSBlbGVtZW50YXJ5IHByb29mIG9mIHRoZSBzYW1lIGZhY3QuDQoNCg0KVGhl IGVhcmxpZXN0IGV4cGxpY2l0IGRpc2N1c3Npb24gSSBrbm93IG9mIHRoaXMgaXNzdWUgKGkuZS6h sGNvbnRyYWN0aWJpbGl0eSBvZiB0aGUgd2Fsa2luZyBlcXVpdmFsZW5jZSBhcyBhIHF1YWxpdHkg Y3JpdGVyaW9uIGZvciBzdHJ1Y3R1cmVkIG5vdGlvbnMgb2YgZXF1aXZhbGVuY2UpIGlzIGluIFN0 ZXZlIExhY2uhr3MgobBBIFF1aWxsZW4gTW9kZWwgU3RydWN0dXJlIGZvciBCaWNhdGVnb3JpZXOh sSwgZml4aW5nIGFuIGVycm9yIGluIGhpcyBlYXJsaWVyIKGwQSBRdWlsbGVuIE1vZGVsIFN0cnVj dHVyZSBmb3IgMi1jYXRlZ29yaWVzobEsIHdoZXJlIGhlIGhhZCB1c2VkIG5vbi1hZGpvaW50IGVx dWl2YWxlbmNlcyChqiBzZWUgaHR0cDovL21hdGhzLm1xLmVkdS5hdS9+c2xhY2svcGFwZXJzL3Ft YzJjYXQuaHRtbCAgU2luY2UgaXShr3MganVzdCAyLWNhdGVnb3JpY2FsLCBoZaGvcyBhYmxlIHRv IHVzZSBmdWxseSBhZGpvaW50IGVxdWl2YWxlbmNlcyChqiBkb2VzbqGvdCBoYXZlIHRvIHdvcnJ5 IGFib3V0IGhhbGYtYWRqb2ludG5lc3MvY29oZXJlbnQtYWRqb2ludG5lc3MuICBBZGpvaW50IGVx dWl2YWxlbmNlcyBvZiBjb3Vyc2UgZ28gYmFjayBtdWNoIGZ1cnRoZXIgoaogYnV0IEkgZG9uoa90 IGtub3cgYW55d2hlcmUgdGhhdCB0aGlzICpyZWFzb24qIHdoeSB0aGV5oa9yZSBiZXR0ZXIgaXMg YXJ0aWN1bGF0ZWQsIGJlZm9yZSBMYWNrLg0KDQpBbmQgZm9yIEpveWFsLWVxdWl2YWxlbmNlcywg SSBkb26hr3Qga25vdyBhbnl3aGVyZSB0aGV5oa9yZSBleHBsaWNpdGx5IGRpc2N1c3NlZCBhdCBh bGwsIGJlZm9yZSBIb1RULiAgTGlrZSBNYXJ0qKpuLCBJoa9kIGJlIHJlYWxseSBpbnRlcmVzdGVk IGlmIGFueW9uZSBkb2VzIGtub3cgYW55IGVhcmxpZXIgc291cmNlcyBmb3IgdGhlbSENCg0KP0Nw Lg0KDQotLQ0KWW91IHJlY2VpdmVkIHRoaXMgbWVzc2FnZSBiZWNhdXNlIHlvdSBhcmUgc3Vic2Ny aWJlZCB0byB0aGUgR29vZ2xlIEdyb3VwcyAiSG9tb3RvcHkgVHlwZSBUaGVvcnkiIGdyb3VwLg0K VG8gdW5zdWJzY3JpYmUgZnJvbSB0aGlzIGdyb3VwIGFuZCBzdG9wIHJlY2VpdmluZyBlbWFpbHMg ZnJvbSBpdCwgc2VuZCBhbiBlbWFpbCB0byBIb21vdG9weVR5cGVUaGUuLi5AZ29vZ2xlZ3JvdXBz LmNvbTxtYWlsdG86SG9tb3RvcHlUeXBlVGhlLi4uQGdvb2dsZWdyb3Vwcy5jb20+Lg0KRm9yIG1v cmUgb3B0aW9ucywgdmlzaXQgaHR0cHM6Ly9ncm91cHMuZ29vZ2xlLmNvbS9kL29wdG91dC4NCg0K DQotLQ0KWW91IHJlY2VpdmVkIHRoaXMgbWVzc2FnZSBiZWNhdXNlIHlvdSBhcmUgc3Vic2NyaWJl ZCB0byB0aGUgR29vZ2xlIEdyb3VwcyAiSG9tb3RvcHkgVHlwZSBUaGVvcnkiIGdyb3VwLg0KVG8g dW5zdWJzY3JpYmUgZnJvbSB0aGlzIGdyb3VwIGFuZCBzdG9wIHJlY2VpdmluZyBlbWFpbHMgZnJv bSBpdCwgc2VuZCBhbiBlbWFpbCB0byBIb21vdG9weVR5cGVUaGUuLi5AZ29vZ2xlZ3JvdXBzLmNv bTxtYWlsdG86SG9tb3RvcHlUeXBlVGhlLi4uQGdvb2dsZWdyb3Vwcy5jb20+Lg0KRm9yIG1vcmUg b3B0aW9ucywgdmlzaXQgaHR0cHM6Ly9ncm91cHMuZ29vZ2xlLmNvbS9kL29wdG91dC4NCg== --_000_8C57894C7413F04A98DDF5629FEC90B138BD0019Pligstuqamca_ Content-Type: text/html; charset="gb2312" Content-Transfer-Encoding: quoted-printable
Dear Vladimir,

I completely agree with you.

Andr=A8=A6
From: homotopyt...@googlegroups.com [homo= topyt...@googlegroups.com] on behalf of Vladimir Voevodsky [vlad...@ias.edu= ]
Sent: Wednesday, October 12, 2016 6:17 PM
To: Peter LeFanu Lumsdaine
Cc: Prof. Vladimir Voevodsky; Martin Escardo; Joyal, Andr=A8=A6; Hom= otopyT...@googlegroups.com
Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence=

I think the clearest formulation is my original one - as the condition= of contractibility of the h-fibers.

This is also the first form in which it was introduced and = the first explicit formulation and proof of the fact that it is a propositi= on. 

Vladimir.





On Oct 12, 2016, at 5:45 AM, Peter LeFanu Lumsdaine <p.l.lu...@= gmail.com> wrote:

> Although I can see formal proofs that Joyal-equivalenc= e is a proposition (or h-proposition), I am still trying to find the best f= ormal proof that uncovers the essence of this fact. This is why I asked the= question of were this formulation of equivalence comes from.

Like Andr=A8=A6 suggested, I feel the nicest viewpoint is the fact that the= =A1=B0free (=A1=DE,1)-category on a Joyal-equivalence=A1=B1 is contractibl= e.  At least in terms of intuition, the conceptually clearest argument= I know for that is as follows.

Look at the *=A1=DE-groupoidification* of this free (=A1=DE= ,1)-category, considered as a space.  This is a cell complex which we = can easily picture: two points x, y, three paths f, g, g' between x and y, = and 2-cells giving homotopies f ~ g, f ~ g'.  It=A1=AFs very clear geometrically that this is contractible.

But =A1=AA the =A1=B0free (=A1=DE,1)-category on a Joyal eq= uivalence=A1=B1 is already an =A1=DE-groupoid =A1=AA and =A1=DE-groupoidifi= cation is idempotent, since groupoids are a full subcategory.  So the = original (=A1=DE,1)-category is equivalent to its groupoidification, so is = contractible.

The same approach works for seeing why half-adjoint equival= ences are good, but non-adjoint and bi-adjoint equivalences are not.  = So as regards intuition, I think this is very nice.  However, I suspec= t that if one looks at all the work that goes into setting up the framework needed, then somewhere one will have already= used some form of =A1=B0equivalence is a proposition=A1=B1.  So this = is perhaps a little unsatisfactory formally, as it (a) needs a lot of backg= round, and (b) may need to rely on some more elementary proof of the same fact.


The earliest explicit discussion I know of this issue (i.e.= =A1=B0contractibility of the walking equivalence as a quality criterion for= structured notions of equivalence) is in Steve Lack=A1=AFs =A1=B0A Quillen= Model Structure for Bicategories=A1=B1, fixing an error in his earlier =A1=B0A Quillen Model Structure for 2-categories=A1=B1, whe= re he had used non-adjoint equivalences =A1=AA see http://maths.mq.edu.au/~slack/papers/qmc2cat.html  Since it=A1=AFs= just 2-categorical, he=A1=AFs able to use fully adjoint equivalences =A1= =AA doesn=A1=AFt have to worry about half-adjointness/coherent-adjointness.=   Adjoint equivalences of course go back much further =A1=AA but I don=A1=AFt know anywhere that this *reason* why they=A1=AFre better is a= rticulated, before Lack. 

And for Joyal-equivalences, I don=A1=AFt know anywhere they= =A1=AFre explicitly discussed at all, before HoTT.  Like Mart=A8=AAn, = I=A1=AFd be really interested if anyone does know any earlier sources for t= hem!

?Cp.

--
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 HomotopyTypeTheory+unsu...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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 HomotopyTypeTheory+unsu...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--_000_8C57894C7413F04A98DDF5629FEC90B138BD0019Pligstuqamca_--