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.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pg1-x53d.google.com (mail-pg1-x53d.google.com [IPv6:2607:f8b0:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b116ebab for ; Thu, 20 Jun 2019 16:48:20 +0000 (UTC) Received: by mail-pg1-x53d.google.com with SMTP id k19sf1784715pgl.0 for ; Thu, 20 Jun 2019 09:48:19 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1561049299; cv=pass; d=google.com; s=arc-20160816; b=B+YEu7voGhEN1ON7OIc41QbUXeePQWCugobT63uHsbYCAB/5mJZ1F4ozJahZwjVDK1 noapsDSbO5fpXnIku8x+RXec0O8p/H0ZylLAer8ClHWUzrpeBp5ri6A4g8VPKVU6DqHu NSltwMy6+WVeFhG2L0psulS3jTbEQT/H3l2nk2bvZZkjT4bUukhUF4OrQyZZZ0S9B18L hNdrPPlxbLmt8nP+fKFk62VlQN4EPLZKFHJ7bMdm6nfvEeUGQ6FZIsVfprQIqSt9Pz0e JgqkhM/sb327MeJ1UJ+bMYvKNm8zb/bl30wepILrPilAo30Ef1kQshXmQ2AFxPdqaNdz /N7g== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=kKUJmi/nKQxT9qOOuy1BruCeOZXgC3IC1WXmJ2zY8Nk=; b=k65yix3X6x/nOnh4YCDHPZxBYVY/+5B2WdVxdtBLtgVNLry4A7612NZzj4hHPHa+0L 7pRoUQSuxYSB/0MQ2TpO9rqpjh+LNw88bbmLjlmTjs7jPJ8O/GjmJvWzvAAJaUwNBOXV 0kFh+DHk5W5Ui4Da2B/XQkYobneUmLG5fbuEX+TFV1SVRjHonecFrU1O5Tg0OBDvsEyh jlE36J1BXz/BZWiciUKXNTLNxH0NQp4Wb9ZPraYqBPXKaLR/39rnoqAFdjWVp57nmwNr /j0gLATJwJ2F6o5gFIyjpl25q/MiZG9Tb1LWQWFVNhG+m/WN3okSdHITalfnoDo/Xyy5 iSbw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VBWt+QBp; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::531 as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kKUJmi/nKQxT9qOOuy1BruCeOZXgC3IC1WXmJ2zY8Nk=; b=nTDfkA/fvHtqG6MAMC+Rus4v5h/0dIA8Jy7+oVbr/a/Ohe9q4jikRTUOdoSWzxaJqU F77zlcGSQhdVpgRdRUagD2QRtJmAGaYg6DYDoFPzs4ya9PSbog1QYD4xOWO2X0k78zOa QUpDSkyUWu4rsBZXpzrq8qaqZZZ/ORmJWoyYUmAD79B2jFx5O1ew/mwcv+5ymEKWYGPP dHae3quOxpjuN5XCoRLq85v9dWpYbnQLia3oyjeLzuwh2dZfuQ3YxIWbKsrFKU4hkdL0 kdvP1y6ZbOC5WBxtogwYNT0cNodh2/AvpIDMzg1oNeaWcHrtMC/NmfpEqq2aSC+AEpSV vXbQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kKUJmi/nKQxT9qOOuy1BruCeOZXgC3IC1WXmJ2zY8Nk=; b=hy3sLB6r2alDN+tIL9sP2HzS0nHe8m4QRXK8emo/DFvvWUUWvYZEdYVA1DhQTIcCI/ QCyXoXY6IFJVpHGarNySuNgj7XgYjWZ1NecM4Fn+3i2hg73Nhd0nT08vSiBUFgO6mKTg +uZ6WpmNrujfUbxjzkgGaIbZm6PgpS9ore2zC/kwSpYGgNwFBrp1SbDV7Otqx5bMGT4w NT163CyuJ0PZYedi+T0bYPFGptR3ggrkokYEmaisHiHy9ER12hC/g+l1PXqiZbim/Kum gpFwXu3kAm7aErN/APK0r5HVXml1tLnwyTO3qwt+3DfZOm/KxuguuURsKZAboMhH/gbM OAeA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=kKUJmi/nKQxT9qOOuy1BruCeOZXgC3IC1WXmJ2zY8Nk=; b=t+ryoBzyq4j94efTHz751AWgZ1oVEpN3vsk3OYou4WjLiujKLCJegICVF/vLtuNrW8 3/nYieZXAfaE2PHWFM/dy2/dis0ttHgEFPR/JByhnKLAqfVhHolwGl0p72EwlWjZeL0O ugM15yDIM+BkyjXxWFSmKTxuFERfXpCd23G9fUy+fKuKXw2xkDSZw4qndy5PgOS8BFOH Tv/x4d/EWvgfQBC/ZlxbPx+u0PTiPFeM3W2jQfduIwc/S4Qeh73ZBm8eLCHZ70IVqlvL wbtj5Ep+Q5Rju4W6wjsxxmjrFzv6+sFOUpIWRatyIiJ4Z2pbOXmJ3P6NwVmji3RX6X0V RNsA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWOkEvWm5R7dtEiZmP2Aj2gvPgEovaZtIslbijX0qVGJ72kPpRA VIPD8jxlnN9mB3P/UyKmgPg= X-Google-Smtp-Source: APXvYqyMLe3SkawI8cu2cf+0mWOz9sFKhJxouRd7+GXMSDlLS4Db0PVRfbMVFyu/R4r61vBmT6Enmw== X-Received: by 2002:a17:90a:3463:: with SMTP id o90mr604494pjb.15.1561049298727; Thu, 20 Jun 2019 09:48:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:1021:: with SMTP id b30ls1492568pla.1.gmail; Thu, 20 Jun 2019 09:48:18 -0700 (PDT) X-Received: by 2002:a17:902:f095:: with SMTP id go21mr51699557plb.58.1561049298322; Thu, 20 Jun 2019 09:48:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1561049298; cv=none; d=google.com; s=arc-20160816; b=WKaz90yQS21tKDZ0TvoFI0PzlGOilL2pg6rw1imtE3gsPlTju9ef7J7hqVDX6+ICXU v+zx+oKqv2/JbWkP6BV220yhi8Ywnb94XxKUu4KKJnVzFYO7CI/9DjYT/HFKyneF5rl4 uqN4m/+jsOTa/po1E8ANZ5F8njwkP6O1xW01auIzcPs22QGU9gfDigHchZpJf4amXhwP cIQUfQEa28pvmePL6dE/pcl5sfAe10LTYAZ+bMrHQj/80lGh82c4XSRRlC/btiQuHzjz m79c6LLJY/MRZjsKxb1RB9UBjgKFPxdIbpAEgEBBN6Z65/IFhKXNa/uJx9nJ65TMjNBf 2Dkg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=+glZjWHGUFp60OcHNQeNxaPtXIJV8MKcHtcToiUs4to=; b=jKys40f7FYvEn0cx4F0gg2cEj3313+B64PkfSF5tF0YG0quP+KDmk6Gps+JY04AAgQ SyH77WVwLVMAUt+nhmRPhbNWT1uhRlANxcYRyZK8SxKU4JbNhRyfrrp15b5X9eVZEERF kCyol+MxMNtLhPjm3LnZNrOp9Ci+WO95+HIJrvPK8C7ekKTPHZHsEYX4bB5oGcwKsA/j snD7r3xeqfDVRTTzmLDpTAlCub12hU4iadP4zeS2rIMX++6JZ/gB4tudHyKFExm3i7jI khBK6ir4P+bEkvV17LYKuvgBtrzwDjNg7hgcEst008bM2ztaSkiqpTAzcpv6xJKIUepC Qmww== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VBWt+QBp; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::531 as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pg1-x531.google.com (mail-pg1-x531.google.com. [2607:f8b0:4864:20::531]) by gmr-mx.google.com with ESMTPS id s60si1802pjc.2.2019.06.20.09.48.18 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 09:48:18 -0700 (PDT) Received-SPF: pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::531 as permitted sender) client-ip=2607:f8b0:4864:20::531; Received: by mail-pg1-x531.google.com with SMTP id 145so1879588pgh.4 for ; Thu, 20 Jun 2019 09:48:18 -0700 (PDT) X-Received: by 2002:a65:5889:: with SMTP id d9mr1298598pgu.39.1561049297624; Thu, 20 Jun 2019 09:48:17 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Ali Caglayan Date: Thu, 20 Jun 2019 17:48:06 +0100 Message-ID: Subject: Re: [HoTT] my first 3 questions about HoTT To: Nathan Carter Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000dca320058bc41c77" X-Original-Sender: alizter@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=VBWt+QBp; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::531 as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --000000000000dca320058bc41c77 Content-Type: text/plain; charset="UTF-8" 1. There are at least two ways in which types are not sets. Firstly, when reasoning classically, we have a membership relation whereby we can postulate the membership of elements in a given set. It may seem similar to a : A but in this case writing a : B would make no sense, whereas in set theory membership can be disproven. This is quite a subtle notion and is closely related to the difference between structural and material set theories which Mike Shulman wrote a nice paper on https://arxiv.org/pdf/1808.05204.pdf. But I am sure someone else here will do a better job at explain that. The second difference is what I think Harper was referring to, which is that sets are types which satisfy what is called Uniqueness of identity proofs (UIP). This means that given a : A and b : A, we can form the identity type Id(a, b). If we wish to show there is an equality between a and b we construct a term p : Id(a, b). But what if we can construct another equality q : Id(a, b)? UIP (a.k.a axiom K) ensures that there is always a term r : Id(p, q). Which in English means: Any two proofs of equality between elements of a set are themselves equal. Why does this matter? Well because in Martin-Lof type theory (with univalent universes) (the type theory that HoTT is based on), you can construct seperate proofs of the same thing. Take for example the type 2. It has two terms 1_2 : 2 and 2_2 : 2. If we consider the ways in which 2 can be equal to itself, i.e. terms of Id(2, 2), we see that (with univalence) there are two possible ways. The first is just reflexivity and the second is "an equality" which swaps 1_2 with 2_2. These are both proofs of Id(2, 2) but they are definitely not the same. And in fact can't be shown to be the same without assuming UIP. 2. One heuristic way to see that judgemental equality can be decided is by "completely computing" a given term, i.e. beta reduce it all the way down. Theorems such as Church-Rosser guarantee that the order of reductions does not matter. There are more properties such as "canonicity" which roughly state that fully reduced terms are identical. I am not an expert on these properties however but there are many experts on this list. Checking whether two terms are judgementally equal is a commonly studied problem in type theory. There are ways to test equality without fully reducing down such as the one detailed here: https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4 3. Simply typed lambda calculus has "natural numbers" via the Church-encoding. The key difference between this and regular arithmetic is that you can't really define a function out of the type of such things. Or in other words, there is no recursion principle for the natural numbers. Adding such a rule would give you something like Godels system T. Universes only need a sucessor structure, and not really the full arithmetic capabilities of the natural numbers themselves. These are just some of my thoughts on your questions, hopefully it will help. Ali Caglayan On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter wrote: > > Hello, HoTT community. > > I've learned a bit about HoTT in bits of spare time over the past few > years, and have come up with some questions I can't answer on my own. It > was suggested that I ask them on this list. I will start with a few small > questions, and if anyone in the community here has time to answer them, > then I'll continue with others as needed. Thank you in advance for any > help you can give. > > (Where I'm coming from: I'm a mathematician; my dissertation was on > intermediate logics, but I haven't focused on logic much for the past 15 > years, instead doing mathematical software and some applied mathematics. I > have a passion for clear exposition, so as I learn about HoTT, I process it > by writing detailed notes to myself, explaining it as clearly as I can. > When I can't explain something clearly, I flag it as a question. I'm > bringing those questions here.) > > Here are three to start. > > 1. Very early in the HoTT book, it talks about the difference between > types and sets, and says that HoTT encourages us to see sets as spaces. > Yet in a set of lecture videos Robert Harper did that I watched on YouTube > (which also seem to have disappeared, so I cannot link to them here), he > said that Extensional Type Theory takes Intuitionistic Type Theory in a > different direction than HoTT does, formalizing the idea that types are > sets. Why does the HoTT book not mention this possibility? Why does ETT > not seem to get as much press as HoTT? > 2. When that same text introduces judgmental equality, it claims that > it is a decidable relation. It does not seem to prove this, and so I > suspected that perhaps the evidence was in Appendix A, where things are > done more formally (twice, even). The first of these two formalisms places > some restrictions on how one can introduce new judgmental equalities, which > seem sufficient to guarantee its decidability, but at no point is an > algorithm for deciding it given. Is the algorithm simply to apply the only > applicable rule over and over to reduce each side, and then compare for > exact syntactic equality? > 3. One of my favorite things about HoTT as a foundation for > mathematics actually comes just from DTT: Once you've formalized pi types, > you can define all of logic and (lots of) mathematics. But then the > hierarchy of type universes seem to require that we understand the natural > numbers, which is way more complicated than just pi types, and thus highly > disappointing to have to bring in at a foundational level. Am I right to > be disappointed about that or am I missing something? > > Thanks in advance for any help you have time and interest to provide! > > Nathan Carter > > -- > 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/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com > > . > For more options, visit https://groups.google.com/d/optout. > -- 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/msgid/HomotopyTypeTheory/CAB17i%3DjRvovt%2BA7RWi2y5ocgV6H%2BKY5YX6bULWyrTQ0fuEYSxg%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --000000000000dca320058bc41c77 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
1. There are at least two ways in which types are not= sets. Firstly, when reasoning classically, we have a membership relation w= hereby we can postulate the membership of elements in a given set. It may s= eem similar to a : A but in this case writing a : B would make no sense, wh= ereas in set theory membership can be disproven. This is quite a subtle not= ion and is closely related to the difference between structural and materia= l set theories which Mike Shulman wrote a nice paper on=C2=A0https://arxiv.org/pdf/1808.05204.pdf= .=C2=A0But I am sure someone else here will do a better job at explain that= .

The second difference is what I think Harper was= referring to, which is that sets are types which satisfy what is called Un= iqueness of identity proofs (UIP). This means that given a : A and b : A, w= e can form the identity type Id(a, b). If we wish to show there is an equal= ity between a and b we construct a term p : Id(a, b). But what if we can co= nstruct another equality q : Id(a, b)? UIP (a.k.a axiom K) ensures that the= re is always a term r : Id(p, q). Which in English means: Any two proofs of= equality between elements of a set are themselves equal.

Why does this matter? Well because in Martin-Lof type theory (with = univalent universes) (the type theory that HoTT is based on), you can const= ruct seperate proofs of the same thing. Take for example the type 2. It has= two terms 1_2 : 2 and 2_2 : 2. If we consider the ways in which 2 can be e= qual to itself, i.e. terms of Id(2, 2), we see that (with univalence) there= are two possible ways. The first is just reflexivity and the second is &qu= ot;an equality" which swaps 1_2 with 2_2. These are both proofs of Id(= 2, 2) but they are definitely not the same. And in fact can't be shown = to be the same without assuming UIP.=C2=A0
=C2=A0
2. One heu= ristic way to see that judgemental equality can be decided is by "comp= letely computing" a given term, i.e. beta reduce it all the way down. = Theorems such as Church-Rosser guarantee that the order of reductions does = not matter. There are more properties such as "canonicity" which = roughly state that fully reduced terms are identical. I am not an expert on= these properties however but there are many experts on this list.

=
Checking whether two terms are judgementally equal is a commonly= studied problem in type theory. There are ways to test equality without fu= lly reducing down such as the one detailed here:

3. Simply typed lambda calculus has "natural numbers" via the = Church-encoding. The key difference between this and regular arithmetic is = that you can't really define a function out of the type of such things.= Or in other words, there is no recursion principle for the natural numbers= . Adding such a rule would give you something like Godels system T. Univers= es only need a sucessor structure, and not really the full arithmetic capab= ilities of the natural numbers themselves.

These a= re just some of my thoughts on your questions, hopefully it will help.

Ali Caglayan

On Thu, Jun 20, 2019 at 5:16 PM Nath= an Carter <nathancarter5@gmai= l.com> wrote:

Hello, HoTT community.
=
I've learned a bit about HoTT in bits of spare time over= the past few years, and have come up with some questions I can't answe= r on my own.=C2=A0 It was suggested that I ask them on this list.=C2=A0 I w= ill start with a few small questions, and if anyone in the community here h= as time to answer them, then I'll continue with others as needed.=C2=A0= Thank you in advance for any help you can give.

(= Where I'm coming from:=C2=A0 I'm a mathematician; my dissertation w= as on intermediate logics, but I haven't focused on logic much for the = past 15 years, instead doing mathematical software and some applied mathema= tics.=C2=A0 I have a passion for clear exposition, so as I learn about HoTT= , I process it by writing detailed notes to myself, explaining it as clearl= y as I can.=C2=A0 When I can't explain something clearly, I flag it as = a question.=C2=A0 I'm bringing those questions here.)

Here are three to start.
  1. Very early in the HoTT b= ook, it talks about the difference between types and sets, and says that Ho= TT encourages us to see sets as spaces.=C2=A0 Yet in a set of lecture video= s Robert Harper did that I watched on YouTube (which also seem to have disa= ppeared, so I cannot link to them here), he said that Extensional Type Theo= ry takes Intuitionistic Type Theory in a different direction than HoTT does= , formalizing the idea that types are sets.=C2=A0 Why does the HoTT book no= t mention this possibility?=C2=A0 Why does ETT not seem to get as much pres= s as HoTT?
  2. When that same text introduces judgmental equality, it c= laims that it is a decidable relation.=C2=A0 It does not seem to prove this= , and so I suspected that perhaps the evidence was in Appendix A, where thi= ngs are done more formally (twice, even).=C2=A0 The first of these two form= alisms places some restrictions on how one can introduce new judgmental equ= alities, which seem sufficient to guarantee its decidability, but at no poi= nt is an algorithm for deciding it given.=C2=A0 Is the algorithm simply to = apply the only applicable rule over and over to reduce each side, and then = compare for exact syntactic equality?
  3. One of my favorite things abo= ut HoTT as a foundation for mathematics actually comes just from DTT:=C2=A0= Once you've formalized pi types, you can define all of logic and (lots= of) mathematics.=C2=A0 But then the hierarchy of type universes seem to re= quire that we understand the natural numbers, which is way more complicated= than just pi types, and thus highly disappointing to have to bring in at a= foundational level.=C2=A0 Am I right to be disappointed about that or am I= missing something?
Thanks in advance for any help you = have time and interest to provide!

Nathan Carter

--
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-= aa1cce32bcb2%40googlegroups.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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https= ://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjRvovt%2BA7RWi2y5o= cgV6H%2BKY5YX6bULWyrTQ0fuEYSxg%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000dca320058bc41c77--