From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,PDS_BTC_ID, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 6683 invoked from network); 28 Apr 2023 18:00:03 -0000 Received: from mail-ot1-x33d.google.com (2607:f8b0:4864:20::33d) by inbox.vuxu.org with ESMTPUTF8; 28 Apr 2023 18:00:03 -0000 Received: by mail-ot1-x33d.google.com with SMTP id 46e09a7af769-6a65be5d5e1sf49057a34.0 for ; Fri, 28 Apr 2023 11:00:03 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682704802; cv=pass; d=google.com; s=arc-20160816; b=AeqBK+Oc1Wz07/OEf34we4EQfrrDxRIUOA0nlw8MIzWPeFPxWBPNlCCHfQqQpKsZ8J 6OMM2qgb+psay3/2C78oe9eduowby1naO1EW8kjHsv4yXs26UWUQavD5gz5NtWBj8dZt T85iD+IVFEcifnOh1VBA2aqdLnqV1onngVUhx4xcpn97kwHPmo4+qR3hyiQvK1oVCFHq KK2v7Bl0g00g3dvO1Fkn0e62rSWN/u45Her01e5uzkuLrb7bl7kNKEVg0ITohHQgMKmv IAeao/Y22dwU+DyckG2RSvv2tpgRRKXWgS5wxdFWkXbG7XmBHC2reu/YsU+bIzb0hF5m 6iWQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe: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; bh=h5tXXBomaMyU3hA64jONN45+XITk+xnvNR1IiOdBv00=; b=IHM7hT3mZICvgGfHaGZk9zFHmXu0k9FO3U46DWaf52OJk96P19Ghgq7w4zysHz6+vS pHO7GQHpp0SPYaH7l3LYAmyLPiWEPWm8C2ZopM0gECI+yT4rRFvQtLGJfvKPhN+Dzwsi XxjUNaDwDUFUEmywRxH6IL45blsKsX3ZLl7EYlSW3xLpXxTSM6ZsDlpW+KWFe+VbB6JQ LpbrdktAb/7RSfSeTqNp1JvV267mEE18K0MKG0JG2ZzjW/LWheAjEVDql8zXXyU057u7 quVxlwnCfx3acuKxADvKQTItSbugkoVIe3gbJFshfVxTC/myc7nRGTduSVPULDCUsVdj gc+w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=RZ6p2JYq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112c as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682704802; x=1685296802; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=h5tXXBomaMyU3hA64jONN45+XITk+xnvNR1IiOdBv00=; b=Pe2SXaOUDpbOhRnlkzqXlMbMMCsiNGBtkRfuDshmAJQzHOz/q0JWitB01UmqQsw3Ge aLhxbxTeFAx7Yzv+oMlleP3S7pzEK40wB+5v3CizRGyPts1KUm9O+4uCDjvwZkx/27Na W9dOIEzb1xftr53DpdE0Gjgw1tVB8DRhBZb+qGIx06JAuSy2DwqZIV1CFExftYGFvFAc 2i8vQTrG9P0IYbNuQv4+eFXr9fJKTWH9W7YtIiV1Of4gRs8bks1UFSy1IOmiU0K/XuyH qfUqASmHCvneVVQWfGnrTaLVcvP4EmDTQB2PhidTQ7CvcZde7luG/SkEChQFrBQWzNbX LSGA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682704802; x=1685296802; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=h5tXXBomaMyU3hA64jONN45+XITk+xnvNR1IiOdBv00=; b=l32Z1QNEbhT3fWDmjF9Krnd+/hGzYbQUVMWd0FYlRJpxn0XuNsHm4iU4yzsJLaBQCd QVxsg0frEVmVixTtDz/TYwb1XcdYsISzYEc9oqz5G79vCPyLMsk6deA4gczndUEwgJwi my92YKhWI1LeZ0zUzgcfjCgkcPDdXAhDxWfo+MEP+1mwt/RvrutcHvBsv799ec4aZDM7 /aef1yAzb2/HV3s66f55mp7wvb7H2W30EQ08J5f5XTPgK8BmzRhp/pu0JL7pOXrnFimE nvgUBEAte/U1s32hQeY0Xhlvl2JcryzA1VvA7JYiL9RmH/w9E5M+yRqMrtenWuwFnw6W q/Ig== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDw0fDM+LwsbrgWsA5DAVnfbww5251dGEypaRWaXfpyCUQacvuSd vB0CmtlMShyb+yjQTrwCZjo= X-Google-Smtp-Source: ACHHUZ42pLPxuLVMMjcF1C3ZVaFUGcGJ50h5yXIPKiY0o0Hfc4/LcDm2HbJ0Po0mJzZ1nlH8urgbVQ== X-Received: by 2002:a9d:470d:0:b0:6a4:16ad:bf70 with SMTP id a13-20020a9d470d000000b006a416adbf70mr1531659otf.0.1682704801503; Fri, 28 Apr 2023 11:00:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:d7d5:0:b0:38d:dff8:142 with SMTP id o204-20020acad7d5000000b0038ddff80142ls1362211oig.1.-pod-prod-gmail; Fri, 28 Apr 2023 11:00:00 -0700 (PDT) X-Received: by 2002:a05:6808:4285:b0:38e:545:d0ec with SMTP id dq5-20020a056808428500b0038e0545d0ecmr2715146oib.26.1682704800255; Fri, 28 Apr 2023 11:00:00 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682704800; cv=none; d=google.com; s=arc-20160816; b=Gxj2stcN8OSHZsqOvMNSlNf5nC6giPB0gQ+k0ChcWRBuGiW6/aCSRN42Ez6+WUdiS1 g7v9ZG5GSnbOor6znRVH4nxLL0e0K+IPyic/ehTONWYfhjjOgHpidm1SlZn7a5XPF8Xo pfIeqI5a5+43TSocomUfWCx0xf8tJ8DSVW0V48233Hj/c/8pWXtsM7m2F0NFlMpTiEaY WK+8IzuQ9IbVYEETG4T2QpgXBVbSqR7jitsqmOwo4haj1IR029Rnhq2i8H7CYriIpMOp BlxJ7YaA9I+LAokWNCrPMKJA5wQ1j+Smd2NuFXjm4yrD/jnyI61jO3eRH14QTNVzh2j9 10Fw== 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=l53VD2RSeqjQO+avS+gyAnpxbwAHCuDxMOffB2DF/Pw=; b=k311n3P6OG29qFvZm9q1sagcxDzqVp447z+qDaEHFhi3ZNFzzMv7tU42FMj5bxAkI1 ht7xnUD8+u5xz93dzgUSqL5vh5lIh3cZ4VLzHcD19kRkj5xAqajucVLcdcjr9Ek3STJS 2TW5tMz4353XI0WGFv2MvNJvSNTheQ6E8sLg8YlgXU75QCTZYibMuJiqR7DD2KbhmO4O YwyOyr6+eI/Jvp0TLojNmOsFIrm/lCeC6UipdhIs1jwkylipgM8RVwIA7uz/5DneQ3Fk 12VfGX9MpCWQY50QVF3NlcXg93XBqyTB44KpApZk6Bw0ov/VnT8dQvlSqV08JlpSC9v/ na4g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=RZ6p2JYq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112c as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yw1-x112c.google.com (mail-yw1-x112c.google.com. [2607:f8b0:4864:20::112c]) by gmr-mx.google.com with ESMTPS id k81-20020acaba54000000b0038c2f0e920bsi1116366oif.4.2023.04.28.11.00.00 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 28 Apr 2023 11:00:00 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112c as permitted sender) client-ip=2607:f8b0:4864:20::112c; Received: by mail-yw1-x112c.google.com with SMTP id 00721157ae682-54f8af6dfa9so2512797b3.2 for ; Fri, 28 Apr 2023 11:00:00 -0700 (PDT) X-Received: by 2002:a0d:e254:0:b0:552:c9b2:b546 with SMTP id l81-20020a0de254000000b00552c9b2b546mr4613732ywe.52.1682704799778; Fri, 28 Apr 2023 10:59:59 -0700 (PDT) MIME-Version: 1.0 References: <87leigyeya.fsf@uwo.ca> In-Reply-To: <87leigyeya.fsf@uwo.ca> From: Michael Shulman Date: Fri, 28 Apr 2023 10:59:48 -0700 Message-ID: Subject: Re: [HoTT] Free higher groups To: Dan Christensen Cc: "homotopytypetheory@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000da742405fa693da8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=RZ6p2JYq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::112c as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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: , List-Unsubscribe: , --000000000000da742405fa693da8 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable The existence of hypercompletion is a good suggestion. Also I realized there are set-level statements that are already known to be true in all Grothendieck 1-toposes but not all elementary 1-toposes, such as WISC and Freyd's theorem that a small complete category is a preorder. So those will be true in any Grothendieck oo-topos too, and can be presumed to fail in HoTT. But it's nice to have one that involves higher types too. On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen wrote: > A not-so-interesting answer to Mike's question is the type of deloopings > of S^3. The reason this isn't so interesting is that it's in the image > of the natural functor from Spaces to any oo-topos, so it's true just > because it is true for Spaces. Similarly, a statement asserting that > pi_42(S^17) =3D (insert what it is) is true in any oo-topos. Another > reason these aren't interesting is that I expect that they are provable > in HoTT with enough work. > > So, I'll second Mike's question, with the extra condition that it would > be good to have a type for which there is some reason to doubt that it > is provably inhabited in HoTT. > > Oh, what about whether the hypercomplete objects are the modal objects > for a modality? I'm throwing this out there without much thought... > > Dan > > On Apr 24, 2023, Michael Shulman wrote: > > > This is fantastic, especially the simplicity of the construction. As > > Peter said, a wonderful way to commemorate the 10th anniversary of the > > special year and the release of the HoTT Book. > > > > Relatedly to Nicolai's question, this question also has an easy proof > > in any Grothendieck infinity-topos. Now that we know it also has a > > proof in HoTT, do we know of any type in HoTT whose interpretation in > > any Grothendieck infinity-topos is known to be inhabited, but which > > isn't known to be inhabited in HoTT? > > > > On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus > > wrote: > > > > Hi David, > > > > Congratulations (again)! I find it very interesting that this > > question has a positive answer. I had suspected that it might > > separate HoTT from Voevodsky's HTS (aka 2LTT with a fibrancy > > assumption on strict Nat). Since this isn't the case, do we know > > of another type in HoTT that is inhabited in HTS, while we don't > > know whether we can construct an inhabitant in HoTT? > > > > Best, > > Nicolai > > > > On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterling > > wrote: > > > > Dear David, > > > > Congratulations on your beautiful result; I'm looking forward > > to understanding the details. Recently I had been wondering if > > anyone had proved this, and I am delighted to see that it is > > now done. > > > > Best wishes, > > Jon > > > > On 21 Apr 2023, at 12:04, David W=C3=A4rn wrote: > > > > > Dear all, > > > > > > I'm happy to announce a solution to one of the oldest open > > problems in synthetic homotopy theory: the free higher group > > on a set is a set. > > > > > > The proof proceeds by describing path types of pushouts as > > sequential colimits of pushouts, much like the James > > construction. This description should be useful also in many > > other applications. For example it gives a straightforward > > proof of Blakers-Massey. > > > > > > Best wishes, > > > David > > > > > > -- > > > 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/f2af459c-53a6-e7b9-7= 7db-5cbf56da17f3%40gmail.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 email to > > HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit > > > https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A= 70A-51CB84BE4B6F%40jonmsterling.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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit > > > https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV= 0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.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 > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo= .ca > . > --=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/CADYavpxy1Qh97%2BPZ1%3DDaaKFH3RXo9wTwDhqbcoUFw5ZDP4oUrQ%= 40mail.gmail.com. --000000000000da742405fa693da8 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The existence of hypercompletion is a good suggestion= .

Also I realized there are set-level statements t= hat are already known to be true in all Grothendieck 1-toposes but not all = elementary 1-toposes, such as WISC and Freyd's theorem that a small com= plete category is a preorder.=C2=A0 So those will be true in any Grothendie= ck oo-topos too, and can be presumed to fail in HoTT.=C2=A0 But it's ni= ce to have one that involves higher types too.

On Mon, Apr 24, 202= 3 at 5:37=E2=80=AFPM Dan Christensen <jdc@= uwo.ca> wrote:
A not-so-interesting answer to Mike's question is the type of del= oopings
of S^3.=C2=A0 The reason this isn't so interesting is that it's in = the image
of the natural functor from Spaces to any oo-topos, so it's true just because it is true for Spaces.=C2=A0 Similarly, a statement asserting that<= br> pi_42(S^17) =3D (insert what it is) is true in any oo-topos.=C2=A0 Another<= br> reason these aren't interesting is that I expect that they are provable=
in HoTT with enough work.

So, I'll second Mike's question, with the extra condition that it w= ould
be good to have a type for which there is some reason to doubt that it
is provably inhabited in HoTT.

Oh, what about whether the hypercomplete objects are the modal objects
for a modality?=C2=A0 I'm throwing this out there without much thought.= ..

Dan

On Apr 24, 2023, Michael Shulman <shulman@sandiego.edu> wrote:

> This is fantastic, especially the simplicity of the construction.=C2= =A0 As
> Peter said, a wonderful way to commemorate the 10th anniversary of the=
> special year and the release of the HoTT Book.
>
> Relatedly to Nicolai's question, this question also has an easy pr= oof
> in any Grothendieck infinity-topos.=C2=A0 Now that we know it also has= a
> proof in HoTT, do we know of any type in HoTT whose interpretation in<= br> > any Grothendieck infinity-topos is known to be inhabited, but which > isn't known to be inhabited in HoTT?
>
> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus
> <nicol= ai.kraus@gmail.com> wrote:
>
>=C2=A0 =C2=A0 =C2=A0Hi David,
>
>=C2=A0 =C2=A0 =C2=A0Congratulations (again)! I find it very interesting= that this
>=C2=A0 =C2=A0 =C2=A0question has a positive answer. I had suspected tha= t it might
>=C2=A0 =C2=A0 =C2=A0separate HoTT from Voevodsky's HTS (aka 2LTT wi= th a fibrancy
>=C2=A0 =C2=A0 =C2=A0assumption on strict Nat). Since this isn't the= case, do we know
>=C2=A0 =C2=A0 =C2=A0of another type in HoTT that is inhabited in HTS, w= hile we don't
>=C2=A0 =C2=A0 =C2=A0know whether we can construct an inhabitant in HoTT= ?
>
>=C2=A0 =C2=A0 =C2=A0Best,
>=C2=A0 =C2=A0 =C2=A0Nicolai
>
>=C2=A0 =C2=A0 =C2=A0On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterlin= g
>=C2=A0 =C2=A0 =C2=A0<jon@jonmsterling.com> wrote:
>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Dear David,
>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Congratulations on your beautiful res= ult; I'm looking forward
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0to understanding the details. Recentl= y I had been wondering if
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0anyone had proved this, and I am deli= ghted to see that it is
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0now done.
>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Best wishes,
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Jon
>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0On 21 Apr 2023, at 12:04, David W=C3= =A4rn wrote:
>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> Dear all,
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> I'm happy to announce a solu= tion to one of the oldest open
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0problems in synthetic homotopy theory= : the free higher group
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0on a set is a set.
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> The proof proceeds by describing= path types of pushouts as
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0sequential colimits of pushouts, much= like the James
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0construction. This description should= be useful also in many
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0other applications. For example it gi= ves a straightforward
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0proof of Blakers-Massey.
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> Best wishes,
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> David
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> --
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> You received this message becaus= e you are subscribed to the
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Google Groups "Homotopy Type The= ory" group.
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> To unsubscribe from this group a= nd stop receiving emails
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0from it, send an email to
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0HomotopyTypeTheory+unsubs= cribe@googlegroups.com.
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0> To view this discussion on the w= eb visit
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0https://groups.google.com/d/msgid/Ho= motopyTypeTheory/f2af459c-53a6-e7b9-77db-5cbf56da17f3%40gmail.com.
>
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0--
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0You received this message because you= are subscribed to the
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Google Groups "Homotopy Type The= ory" group.
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0To unsubscribe from this group and st= op receiving emails from
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0it, send an email to
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0HomotopyTypeTheory+unsubs= cribe@googlegroups.com.
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0To view this discussion on the web vi= sit
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0https://groups.google.com/d/m= sgid/HomotopyTypeTheory/D102F774-D134-46B9-A70A-51CB84BE4B6F%40jonmsterling= .com.
>
>=C2=A0 =C2=A0 =C2=A0--
>=C2=A0 =C2=A0 =C2=A0You received this message because you are subscribe= d to the Google
>=C2=A0 =C2=A0 =C2=A0Groups "Homotopy Type Theory" group.
>=C2=A0 =C2=A0 =C2=A0To unsubscribe from this group and stop receiving e= mails from it,
>=C2=A0 =C2=A0 =C2=A0send an email to HomotopyTypeTheory+uns= ubscribe@googlegroups.com.
>=C2=A0 =C2=A0 =C2=A0To view this discussion on the web visit
>=C2=A0 =C2=A0 =C2=A0https://groups.google.com/= d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV0fgJFd8Mzqfchskc4-%2B-FXT42W= QkzmC9w%40mail.gmail.com.

--
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/87lei= gyeya.fsf%40uwo.ca.

--
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/CADYavpxy1Qh97%2BPZ1%3DDaaKFH= 3RXo9wTwDhqbcoUFw5ZDP4oUrQ%40mail.gmail.com.
--000000000000da742405fa693da8--