From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-io1-xd40.google.com (mail-io1-xd40.google.com [IPv6:2607:f8b0:4864:20::d40]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 512223e3 for ; Wed, 27 Nov 2019 00:16:13 +0000 (UTC) Received: by mail-io1-xd40.google.com with SMTP id w19sf14606345iod.20 for ; Tue, 26 Nov 2019 16:16:13 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574813772; cv=pass; d=google.com; s=arc-20160816; b=FtBr3TsElwohVwMCkz7g3l8zB83rKy2Gi0H7fKIASWUHjNSRPuUk7UPuXAibYnC3BJ cd4Yl2hrLBvQW3LqgfycORv/6UaYHPC2CcQuSwxLl9jmTvgiIvaOEzrxlVG3Xh0Hna+i ITjX8IRD+xO/6gPYaks5rY9zXe9YItgO9knPWjM1lHN5JKUgeTS6yszUYxKg4JPzogzF OXKlKcC7GXlF+QeMhhm6VTxz7kNG6ZhujoTnizThca8WBNGwFI5GW8z1tOS17b4xXldf ISvDsDLSeZWRvF4gJGblSO6yhmO64qdFvCKu3BPfvWsCjDznEFO2XcXRprCKIOrYmZBQ rOEg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence: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-phdr :sender:dkim-signature; bh=+TjUzQsQf7/KnM89OGPt/f+HYMpM2sSgvEMqDgSlCO0=; b=Of1YPeIs1xYwWCm3dcv07hkgYPd7cO9THytEAqG0mPBuqIMNhtJQCORYb1eQObLaX/ Z7/dtprp2cc3evTtzYA75Mp4iQy85t26BQainlAX4gV5lYYz05CmNQ+0N43pVtwkFizs OoGTFvs5zTTgJr33UvWUXG8Zt3l8u+Hmlp61Rob/gN5JBeX7tuWYLBHEWTW72y5VOYe6 VJ7Hn2IofxqpDm7Iz7TbXt1Y5VBq3+AwtIyWAL1kB20k7FS66tF8i4/Guj2H46wLT/NN lh4gz2t4OY2qShSJvIlcuErTplPULpFgBDariSYyuBf5Grf6NgieJqlOFoBqSNtTIOnM vFYg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.162 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:ironport-phdr:from:to:cc:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:content-transfer-encoding:mime-version :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+TjUzQsQf7/KnM89OGPt/f+HYMpM2sSgvEMqDgSlCO0=; b=atZes/SFui0B30VKGE7G26ETS0H6KBPRjYI8indmvHejyepTwnLDECmzTO1V0UtL6H vBO2YshUJjv5SdX1kRR8UjDtYPdHNfSDdnTF3W6/3y2HBekD32CKaIPnON9sIsMD6DTo Xfjj+17Si7MavTV6cUO2da2t6LLaWPL0wclojli3P/2qdBMYprblweCNs2V/qh6YoZtY Lkx9GOZaDJYcoV3Lljy5XnwqQAYO8JiSeLvZaxhiMRFWP14bd888HlW2p0vaFKStBIXH 5mx6TxKHDXZ31Yo25fYFgTrXXZb/hOIDsHJ4zg/KMBXTy57/8qLQm3eFxHVZnSihikC2 hzEA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:ironport-phdr:from:to:cc:subject :thread-topic:thread-index:date:message-id:references:in-reply-to :accept-language:content-language:content-transfer-encoding :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-unsubscribe; bh=+TjUzQsQf7/KnM89OGPt/f+HYMpM2sSgvEMqDgSlCO0=; b=SD4oX02SFGZl0yTibV/B/iMgsIwXE2DacVMDO19Tih1+X+jk8xV4kZ5MtE3p1q6xC8 WA+wubfzm03fTxQ2Vebb20/y9sfqzowb/kD4R58mdo3UWW5S3RTGbDMDSo9U4V00lSkh UyQY9WPIYETDXMgxirpjiWbSFf3hsazz1bJkug7q01RGCk2483HZ/dhcA4TRoK6ejGiO Nq0z/EaxJ0CcIYBw8y1saNE48LJtaQy/3zw4nXbcwhgUK5YO53QciNEjD5ZO0TEUVsI7 NFAIYMVP5hagdKZSg9J2hssx29wWiZO9bc340Pj1PTEUrkadTmbIAWvhnL34MtLzWww6 62+A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX8K29N9hsVB2KRYhSDwcnVsFIkAwYTJ6ux4Jst0U2iJa2XVMhL 2K/ulrL15MiovlLJV5MaaBw= X-Google-Smtp-Source: APXvYqyw0A0+U5I6wrM3pRu46gro8Bo6U54Y31+PRlMXXuPJzC8gaR92iN8kCw9ml5KW47QHwuQazA== X-Received: by 2002:a92:5a45:: with SMTP id o66mr26482177ilb.67.1574813771882; Tue, 26 Nov 2019 16:16:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:2908:: with SMTP id l8ls3986873ilg.3.gmail; Tue, 26 Nov 2019 16:16:11 -0800 (PST) X-Received: by 2002:a92:1d9d:: with SMTP id g29mr29290474ile.305.1574813771449; Tue, 26 Nov 2019 16:16:11 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574813771; cv=none; d=google.com; s=arc-20160816; b=czHEWi0XHDOr+JrlxfUKjstmqniQayMcuNaps17MiSFrWlVOkKJ+UDB1EbZEtYRR6Q xxkMQRLy6Wcap0NmBAXHOu54oQahcf44Exusl70X+oJmlHGr2DyrYIH/7UJA8PgrViZP acbOjkOJJNGO8JCMxsezG8Uwbr5oA/cqo1vGH2/N661kC4z1gDQWA90wmNNJFJ1Q2kDu mj4VE134nGTTtIndFyOTELI9N+eIhCobISTZ0SDD+wylRqwfhimEMpxmlbxrnHHJPXkN wLts0afEvYfKawsBDSi6U18FOKRTGYt+UhjtIJxKP6W0mtNa/Loe4OTrZovVR4aFwO21 LH1Q== 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-phdr; bh=KewC0cNy3Gc/frE679PYuy91kLKiqJ30G+ymJc1cDM0=; b=TuDFaSnJfMoihfQsIvO5mnG6azP7ot3TJjxi5cfF2m/MDjQVuHk4JPBFuauQ19RCiz oSRY7DnawAbJhWPk3hDFNqiR/7a7FRzfEzseekAqu4zA8p5Wc5bmEY1ht2qopO8BLdWf VNv5ZfyEJQXDuJVDKhWGFS8kCTueZGqRTNjeKZ+1jER+Qs5v9hJLqJom9msdCTe2msjM QtTj1C6y6hFx0r4viPvWfTRFboK39YqzHEAx7uC/VDcjWf5yZxCMABHsCeVg+hAPSapi xHsQFtA5yC2nebZ79T4WCGoXhfqajfDjJH177AgEwWw7ptQC+FkKqw9hs5NTlxtLJQPb WHaA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.162 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca Received: from data.crochet.telecom.uqam.ca (mail3.uqam.ca. [132.208.246.162]) by gmr-mx.google.com with ESMTP id b74si271589ilb.1.2019.11.26.16.16.11 for ; Tue, 26 Nov 2019 16:16:11 -0800 (PST) Received-SPF: pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.162 as permitted sender) client-ip=132.208.246.162; Received-SPF: None (data2.crochet.telecom.uqam.ca: no sender authenticity information available from domain of joyal.andre@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.crochet.telecom.uqam.ca; envelope-from="joyal.andre@uqam.ca"; x-sender="joyal.andre@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.crochet.telecom.uqam.ca: no sender authenticity information available from domain of postmaster@Message.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.crochet.telecom.uqam.ca; envelope-from="joyal.andre@uqam.ca"; x-sender="postmaster@Message.gst.uqam.ca"; x-conformance=spf_only IronPort-PHdr: =?us-ascii?q?9a23=3ASpS+phC4wdGSNBCXLwyvUyQJP3V1i/DPJgcQr6Ef?= =?us-ascii?q?pfdOf6Ckpc2wGUHE/vxigRnGRpmd9utNjqzduvK4AD1S0dO6qHkHNad0eVoAgM?= =?us-ascii?q?QSkRYnBZ/XFFTyKbjhZn5iEQ=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2BEAwDfvt1d/9H20IRcCQ4OAQEBAQEHA?= =?us-ascii?q?QERAQQEAQGBfoF0LGxVAR8SKgqEGgeRGog2gSV7jnCBEANUCQEBAQEBAQEBAQg?= =?us-ascii?q?YDwUBAgEBhEACF4FfHAY6EwIQAQEFAQEBAQECAwRthGtMDIVSAQEBAQMjERofB?= =?us-ascii?q?QcQAgEIDQQEAQEBAgIGIAICAh8QARUICAIEAQcGAQQBBw0IBIMCgkYDLg+xI3W?= =?us-ascii?q?BMhqEIAGDYQ2BG4EKBoEOKIV+iDGBWIFOSQcuPoIbSQICgSkFAQgKASEFECOCV?= =?us-ascii?q?jKCLASNBIMPnTItQgeCL4cdiiCENI5UA4tGjkiIPIIUj2qBaSI3MHGBQIJsUBG?= =?us-ascii?q?GaBcVbwEOgj2KGDtBATIBAQ51AQEhjBiBIgGBDgEB?= X-IPAS-Result: =?us-ascii?q?A2BEAwDfvt1d/9H20IRcCQ4OAQEBAQEHAQERAQQEAQGBfoF?= =?us-ascii?q?0LGxVAR8SKgqEGgeRGog2gSV7jnCBEANUCQEBAQEBAQEBAQgYDwUBAgEBhEACF?= =?us-ascii?q?4FfHAY6EwIQAQEFAQEBAQECAwRthGtMDIVSAQEBAQMjERofBQcQAgEIDQQEAQE?= =?us-ascii?q?BAgIGIAICAh8QARUICAIEAQcGAQQBBw0IBIMCgkYDLg+xI3WBMhqEIAGDYQ2BG?= =?us-ascii?q?4EKBoEOKIV+iDGBWIFOSQcuPoIbSQICgSkFAQgKASEFECOCVjKCLASNBIMPnTI?= =?us-ascii?q?tQgeCL4cdiiCENI5UA4tGjkiIPIIUj2qBaSI3MHGBQIJsUBGGaBcVbwEOgj2KG?= =?us-ascii?q?DtBATIBAQ51AQEhjBiBIgGBDgEB?= X-IronPort-AV: E=Sophos;i="5.69,247,1571716800"; d="scan'208";a="335982320" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.246.209]) by data2.crochet.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 26 Nov 2019 19:16:09 -0500 Received: from PLI.gst.uqam.ca ([169.254.3.26]) by Message.gst.uqam.ca ([169.254.1.245]) with mapi id 14.03.0439.000; Tue, 26 Nov 2019 19:16:09 -0500 From: =?utf-8?B?Sm95YWwsIEFuZHLDqQ==?= To: Michael Shulman , Kevin Buzzard CC: =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Subject: RE: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Thread-Topic: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? Thread-Index: AQHVjNSjN/nwEFxl2Ei/BdsYtl5YK6du/7MAgAqw6gCAAAPDAIAAezwAgAAJJoCAACwEgIABomcAgB8YCYCAAfrtAIABO4eAgAAKtACAACisAP//yVI5 Date: Wed, 27 Nov 2019 00:16:08 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652BA70E@Pli.gst.uqam.ca> References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> , 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.80] Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Original-Sender: joyal.andre@uqam.ca X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.162 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , Dear Michael, You wrote: <> The notion of canonical isomorphism depends obviously on the context.=20 For example, the "canonical isomorphism" =20 (AxB)xC =3D Ax(BxC) is likely to be the associativity isomorphism. Maybe AI (deep learning) could be trained to recognise the correct canonical isomorphism from the context (=3Dthe proof). It may automatise what is already automatic in our thinking. Best, Andr=C3=A9 ________________________________________ From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.= com] on behalf of Michael Shulman [shulman@sandiego.edu] Sent: Tuesday, November 26, 2019 5:18 PM To: Kevin Buzzard Cc: Mart=C3=ADn H=C3=B6tzel Escard=C3=B3; Homotopy Type Theory Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be = 'impractical'? Personally, I'm doubtful that one can ascribe any precise meaning to "canonical isomorphism", and therefore doubtful that one will be able to implement a computer proof assistant that can distinguish a "canonical isomorphism" from an arbitrary one. It's certainly worth thinking about, but my personal opinion is that instead of designing a proof assistant to match the way mathematicians think about "canonical isomorphisms", mathematicians are going to need to change the way they think. But it's just a question of going all the way down a road that they've already taken one step along. In formal systems like ZFC and Lean, almost no isomorphisms are equalities. Being willing to treat "canonical" isomorphisms as equalities is a first step into the brave new world of homotopy theory and higher category theory, but it's hard to find a place to stand when you've only taken that one step. In trying to make things precise, I think one feels inexorably pulled to the more consistent, and formalizable, position that *all* isomorphisms should be treated as equalities. It's not the same notion of equality, as Martin says, but it's a better replacement for it, which in particular can do everything that the old notion of equality could do when used "correctly" (e.g. equality of numbers and functions). On Tue, Nov 26, 2019 at 11:53 AM Kevin Buzzard wrote: > > Nicolas originally asked > > "So, to put this into one concrete question, how (if at all) is HoTT-Coq > more practical than Mizar for the purpose of formalizing mathematics, > outside the specific realm of synthetic homotopy theory?" > > One issue with this question is that different people mean different thin= gs by "mathematics". As someone who was until recently an outsider to forma= lising but very much a "working mathematician", I think I've made it pretty= clear on this forum and others that for the majority of people in e.g. my = maths department, they would say that none of the systems have really got a= nywhere concerning modern day mathematics, which is the kind of mathematics= that the majority of mathematicians working in maths departments are inter= ested in. This is a dismal state of affairs and one which I would love to h= elp change, but it needs a cultural change within mathematics departments. = The Mizar stuff I've seen has mostly been undergraduate level mathematics. = UniMath seems to be a massive amount of category theory and not much underg= raduate level mathematics at all. On the other hand, "there is a lot more c= ategory theory in the HoTT systems than in Mizar, so maybe Hott-Coq is more= practical than Mizar for category theory" might be an answer to the origin= al question. > > I'm interested in algebraic geometry, and in algebraic geometry there is = this convention (explicitly flagged in Milne's book on etale cohomology) th= at the notation for "canonical isomorphism" (whatever that means) is "=3D".= One can call this "mathematical equality" and it comes with a warning that= it is not well-defined. I think one reason it's a challenge to formalise m= odern algebraic geometry is that none of the systems seem to have this kind= of equality (perhaps because all of the systems demand well-defined defini= tions!). What I meant by my earlier post was that the `=3D` I have run into= in Lean's type theory is too weak (canonically isomorphic things can't be = proved to be equal) but the one I have run into in HoTT seems too strong (n= on-canonically isomorphic things are equal). > > It would not surprise me if different areas of mathematics had different = concepts of equality. Mathematicians seem to use the concept very fluidly. = Maybe it is the case that the areas where "mathematical equality" is closer= to e.g. Lean's `=3D` or Mizar's `=3D` or UniMath's `=3D` or Isabelle/HOL's= `=3D` or whatever, will find that formalising goes more easily in Lean's t= ype theory/Mizar/HoTT/HOL or whatever. The biggest problem with this conjec= ture is that equality is mostly a cut-and-dried thing at undergraduate leve= l, and there is not enough harder maths formalised in any of these systems = (obviously there are several monumental theorems but I'm dreaming about far= greater things) for us to start to check. Note that people like Riemann ha= d no idea about set theory but did a lot of complex analysis, and he really= only needed to worry about equality of complex numbers and equality of fun= ctions from the complexes to the complexes, so I don't think it's a coincid= ence that a whole bunch of complex analysis is done in Isabelle/HOL, which = seems to me to be the "simplest logic" of the lot. Probably all the systems= model this equality well. > > Kevin > > > On Tue, 26 Nov 2019 at 19:14, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: >> >> >> >> On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: >>> >>> HoTT instead expands the notion of "equality" to >>> essentially mean "isomorphism" and requires transporting along it as a >>> nontrivial action. I doubt that that's what you have in mind, but >>> maybe you could explain what you do mean? >> >> >> I think terminology and notation alone cause a lot of confusion (and I >> have said this many times in this list in the past, before Kevin joined = in). >> >> Much of the disagreement is not a real disagreement but a >> misunderstanding. >> >> * In HoTT, or in univalent mathematics, we use the terminology >> "equals" and the notation "=3D" for something that is not the same >> notion as in "traditional mathematics". >> >> * Before the univalence axiom, we had Martin-Loef's identity type. >> >> * It was *intended* to capture equality *as used by mathematicians* >> (constructive or not). >> >> * But it didn't. Hofmann and Streicher proved that. >> >> * The identity type captures something else. >> >> It certainly doesn't capture truth-valued equality by default. >> >> In particular, Voevosdky showed that it captures isomorphism of >> sets, and more generality equivalence of =E2=88=9E-groupoids. >> >> But this is distorting history a bit. >> >> In the initial drafts of his "homotopy lambda calculus", he tried >> come up with a new construction in type theory to capture >> equivalence. >> >> It was only later that he found out that what he needed was >> precisely Martin-Loef's identity type. >> >> * So writing "x =3D y" for the identity type is a bit perverse. >> >> People may say, and they have said "but there is no other sensible >> notion of equality for such type theories. >> >> That may be so, but because, in any case, *it is not the same >> notion of equality*, we should not use the same symbol. >> >> * Similarly, writing "X =E2=89=83 Y" is a bit perverse, too. >> >> In truth-valued mathematics, "X =E2=89=83 Y" is most of the time inte= nded >> to be truth-valued, not set-valued. >> >> (Exception: category theory. E.g. we write a long chain of >> isomorphisms to establish that two objects are isomorphic. Then we >> learn that the author of such a proof was not interested in the >> existence of an isomorphism, but instead to provide an >> example. Such a proof/construction is usually concluded by saying >> something like "by chasing the isomorphism, we see that we can take >> [...] as our desired isomorphism.) >> >> >> * With the above out of the way, we can consider the imprecise slogan >> "isomorphic types are equal". >> >> The one thing that the univalence axiom doesn't say is that >> isomorphic type are equal. >> >> What it does say is that the *identity type* Id X Y is in canonical >> bijection with the type X =E2=89=83 Y of equivalences. >> >> * What is the effect of this? >> >> - That the identity type behaves like isomorphism, rather than like >> equality. >> >> - And that isomorphism behaves a little bit like equality. >> >> The important thing above is "a little bit". >> >> In particular, we cannot *substitute* things by isomorphic >> things. We can only *transport* them (just like things work as >> usual with isomorphisms). >> >> * Usually, the univalence axioms is expressed as a relation between >> equality and isomorphism. >> >> Where by equality we don't mean equality but instead the identity >> type. >> >> A way to avoid these terminological problems is to formulate >> univalence as a property of isomorphisms, or more precisely >> equivalences. >> >> To show that all equivalences satisfy a given property, it is >> enough to prove that all the identity equivalence between any two >> types have this property. >> >> * So, as Mike says above, most of the time we can work with type >> equivalence rather than "type equality". And I do too. >> >> Something that is not well explained at all in the literature is >> when and how the univalence axiom *actually makes a difference*. >> >> (I guess this is not well understood. I used to thing that the >> univalence axioms makes a difference only for types that are not >> sets. But actually, for example, the univalence axiom is needed (in >> the absence of the K axiom) to prove that the type of ordinals is a >> set.) >> >> * One example: object classifiers, subtype classifiers, ... >> >> * Sometimes the univalence axiom may be *convenient* but *not needed*. >> >> I guess that Kevin is, in particular, saying precisely that. In all >> cases where he needs to transport constructions along isomorphisms, >> he is confident that this can be done without univalence. And I >> would agree with this assessment. >> >> Best, >> Martin >> >> >> >> >> -- >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.c= om. > > -- > 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+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/CAH52Xb3ynUB2gTYnnmtijsYFcwpNK84aTxLT0kwd5syASy31Aw%40= mail.gmail.com. -- 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQyAaJnLeJZHCMqWAu3f%2BOb72%2BMSSLmb8MjkBHoH05k_Rw%= 40mail.gmail.com. --=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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652BA70E%40Pli.gst.uqam.= ca.