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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 13197 invoked from network); 9 Feb 2022 04:16:59 -0000 Received: from mail-pf1-x43d.google.com (2607:f8b0:4864:20::43d) by inbox.vuxu.org with ESMTPUTF8; 9 Feb 2022 04:16:59 -0000 Received: by mail-pf1-x43d.google.com with SMTP id 2-20020aa79202000000b004cef2fc59f0sf887461pfo.12 for ; Tue, 08 Feb 2022 20:16:59 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1644380217; cv=pass; d=google.com; s=arc-20160816; b=zO8LOBy9A2f/326omlS0fkG7LgpyxUyrMlmC3aie4Dr/LlxE0f4Swjfrj3NZOVv7ld 3qHGTOzZfclcittyJErf0sBmUJ8U5IfbiHmAB4eejyoLK+c8pZ9SMR+6xQamdHV8M/Jc kxmzeDQhehUvviBNQuWvYFMpl/oWpPrDrTBtnkt0ahl5tiYMDssYTBQnCeey8Ed4n8Wc +/iIHG60GW6jRs9wtsZuW7PgxhN2MCTF3mB/LI8hq5ncbRN5nUK9+YoUafjJhzv5Uys/ VZzFvT58QM9/rqPoBqG9cPfMVPhs1Utc+/QSiEBK0biNeaxJ+4OmB/NIcDN3rP6wtzfY eRHw== 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 :dkim-signature; bh=yvl2BXBqtLWvOqAQ0tu3sr/tGvPeL6ilQ8oGHKmmtbY=; b=JRqb7UjytP4kD4q8UqCwi78hx1M2jVKjVEAMny+30D4B9eKK+RKNLWna1ctdsRcR2m 3q/eYzHCPHIodlSAUcwEjO5GF8PmTwgWx9G5yvES09EsFdPVdvBSKQ5bNyAjtBIyXnnC RH6GXmt4CQouzFlsix82uumbIE0pw3BOOfqFEyDDZiMrmjwjcr909noWhb7NQtvMABVX 6HvLYTH/jTEtl7uNl3Tvmfxs21eXfkRq1pNHnYUWLApfrdnERMokde3mG5HO2GXH2Iaj kMjtT9jUM50fGxSN+SGue+0veINd6l0k8X+7twbB39ePNvyOt7SxBfmJGNVuYciX2pX0 01CA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=lkGFnrW4; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e2a as permitted sender) smtp.mailfrom=nsnyder@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=20210112; 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-subscribe:list-unsubscribe; bh=yvl2BXBqtLWvOqAQ0tu3sr/tGvPeL6ilQ8oGHKmmtbY=; b=hy4tKqGlsKdeb25Qf3tjZSjl1xbHcaajfPHFx84gRYbQ2pHVN8iN4jb9DlTbrUkyse DyzANYxW6zXa8B++wlmNKODfHvVeCC7JnRgg9yoxOuqODZA28NKAk+rIwadpPM7tV5Xi G71e95T4xxKgUYvLMmTFewJoTIFD6I/IealbYypSqcVBG2Iaq6QC5pmno7j/cGYY/RO7 UwzmB3kzRYmg3g8Ij6U84N+hU9upXW9M+5/KCIQKxVgBKKCapmVx877zLOwD4Ws48w6V 7LPPP0eRnkveb9M71n53J0eY5WTBge3dNJoSfiE+QXqiitsz/0wkloUy681PnwFNOVss BASg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; 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-subscribe:list-unsubscribe; bh=yvl2BXBqtLWvOqAQ0tu3sr/tGvPeL6ilQ8oGHKmmtbY=; b=qBzsskbgKNOphAOxbDROWY8JD98OF9NAuBRrq1VZVxg0hnje26M+ArGXD1fdp0RpGT q60FgEaIy/duIz3xjmgp2lzSnQeOSlM7KdZlIIWcgnUQtIV+UwpQ0JbSeDrmrpEWT/+J O8YNXOB14dXV/l1p2uOVZmMRc8bNMlxIXUUCW+VJs3vnWT10T3eHyNTTeYFI3Qa5VL+G VKpxNYM53IjSSHzodHMwH+nTprK2h1cC+mSxgUKtgbigBTjRr8zPcJlRiQlD3GdcUWvD 6bORlN2aKGvmksurM4YBu4dpunSfO6VwrELZYmmK6PVqFFSl91+H77PfKGrvenOdmkq/ R5rg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; 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-subscribe:list-unsubscribe; bh=yvl2BXBqtLWvOqAQ0tu3sr/tGvPeL6ilQ8oGHKmmtbY=; b=L153u0ju2koNonuIuwSTkwNjuoaLvqlTpwfZJox1Fs5NNYeI1HjmjL/7sb9oM+QmsP ojHTgFTh7lxkNdGeQTvWVOeh+OILIaqfvVHQTq7ouMWC0Qx3LbDSNHFAs5b4gxROCgkv p42GhrcPQxt3vxln5GsXZDMf0tyDeuQ9SB6PvzqSJUm3yoeN5hFU0YVqGANCHcAP6vBZ 7kDHEKQmaV2kla+zLWGRq7JzlySCNxNrlGyK18xPJgwTcQVjQZUKXlb/NnPf42r7nyA7 +Q+xVSkEwYlICp+VyjdMCzkfg3z6w53DQlK/HO3OHK4n/kaz+lCVmmpS11brqWvcTs/W snLw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531H8YeBiiwABnxoUSsV5joBvRmtaZStFkQwGtb/2SbvwIHKvKLl bBOL/+QR+1rdNfag8uIbIww= X-Google-Smtp-Source: ABdhPJzzm/vXsBVTFe86CV8Fi15S231qLyyAuxnwmFF5CevHdfHK0uB792/gcZ12maKVSOuOTmpZ9w== X-Received: by 2002:a17:90a:780f:: with SMTP id w15mr506474pjk.139.1644380216706; Tue, 08 Feb 2022 20:16:56 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:4101:: with SMTP id o1ls364976pga.8.gmail; Tue, 08 Feb 2022 20:16:55 -0800 (PST) X-Received: by 2002:a65:4286:: with SMTP id j6mr440982pgp.619.1644380215171; Tue, 08 Feb 2022 20:16:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1644380215; cv=none; d=google.com; s=arc-20160816; b=gF1RoqB8PqQMmmlaifI0EyP0I6L98tehPWI1BSJ/wBLACbT1Rj0FHvlovB8u7vUYqZ FL3Q/LW02XRKB/VGVQBk73bMKFvCMj69fJRUVi82NNmvzTLJNDbCpkm8pf2PrEAztC6x 0lQIm91L4Voxooo9Evhdrh9wUHHYYYYKhYopf6F50j3jWwiIGJZqia7DyhVdFI+tkOOU kaXIyp5AiVdAKY1VhMhPWVGMex+psyOsOjmi97h8G0w0T1ISomXH4n0GWpgMIkkITObQ 8v3mXkOUx/8K2nyeL1ZnI3CZolm+VWk8GsnUMx6oLvhPlUWGdfwt1tXlZz7U0CKy+1lv yhSg== 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=urWeuvZr3lc9Rjkrg1tc9N8eo7FbR60fgaHXeAYimsA=; b=ShnwBhtTAxu7XyFdp7RzSsOURbTHvJDjAcDsPT2n14Ydz2fWCOm1Nzcr7fjOESNkTZ tIthGX9CTH5wUSxBd2Jd7lyscGjk7z6HW0t+2b/Zkwd3tiMowbUJOGzoDVeAMaAOZ9KM DXgg3Yc4XzcCW/6xyuXFfzktv6yZ+NC7uF98cTJSqKnOzGQdiuxyAIC4AupDO82Ojciu maXeQMnprRVxwO8npa9qVg0t6R7PBpJHaVR/8RK402NwGRRLa/qZOyqplCf/OjQ3XxJx OzqOA4hLzPLlUpyoL+j31rKS8+uTMgDI1Izua4ixO+wVRwqaycMMyZ4yYaZuNEQA17mB z2fA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=lkGFnrW4; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e2a as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vs1-xe2a.google.com (mail-vs1-xe2a.google.com. [2607:f8b0:4864:20::e2a]) by gmr-mx.google.com with ESMTPS id b5si265582plh.1.2022.02.08.20.16.55 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 08 Feb 2022 20:16:55 -0800 (PST) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e2a as permitted sender) client-ip=2607:f8b0:4864:20::e2a; Received: by mail-vs1-xe2a.google.com with SMTP id b2so1241589vso.9 for ; Tue, 08 Feb 2022 20:16:55 -0800 (PST) X-Received: by 2002:a67:fd55:: with SMTP id g21mr138941vsr.86.1644380214062; Tue, 08 Feb 2022 20:16:54 -0800 (PST) MIME-Version: 1.0 References: <021D547B-986C-4E18-B4F2-A105376DE6EB@gmail.com> In-Reply-To: <021D547B-986C-4E18-B4F2-A105376DE6EB@gmail.com> From: Noah Snyder Date: Tue, 8 Feb 2022 23:16:43 -0500 Message-ID: Subject: =?UTF-8?B?UmU6IFtIb1RUXSBGb3JtYWxpemF0aW9uIG9mIM+A4oKEKFPCsyniiYXihKQvMuKEpCBpbg==?= =?UTF-8?B?IEN1YmljYWwgQWdkYSBjb21wbGV0ZWQ=?= To: Steve Awodey Cc: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , Anders Mortberg , Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000088f38805d78e1a8f" X-Original-Sender: nsnyder@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=lkGFnrW4; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e2a as permitted sender) smtp.mailfrom=nsnyder@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: , List-Unsubscribe: , --00000000000088f38805d78e1a8f Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I think it goes back to Pontryagin from the late 1930s, though with a rather different argument. The history is a bit confusing because Pontryagin famously made a mistake in computing \pi_4(S^2). But his calculation of \pi_4(S^3) was fine. See Theorem 2' and 2'' of https://people.math.rochester.edu/faculty/doug/otherpapers/pont2.pdf which I found at this webpage that has more history: https://people.math.rochester.edu/faculty/doug/AKpapers.html#2-stem Best, Noah On Tue, Feb 8, 2022 at 10:09 PM Steve Awodey wrote: > Someone please correct me if I am wrong, > but I believe that this was originally proved by J-P Serre in his 1951 > dissertation (using spectral sequences). > So we are about 70 years behind - but catching up fast! > > Congratulations to all who contributed to this milestone! > > Univalent regards, > > Steve > > > On Feb 8, 2022, at 6:24 PM, Joyal, Andr=C3=A9 wrote= : > > Dear Anders, > > Congratulation to you and Axel for doing this! > It was a problem for many years! > We can now honestly say that cubical Agda is a serious tool in homotopy > theory! > It is an amazing piece of work. > Thanks to all, starting with Guillaume. > > Best wishes, > Andre > ------------------------------ > *De :* homotopytypetheory@googlegroups.com < > homotopytypetheory@googlegroups.com> de la part de Anders Mortberg < > andersmortberg@gmail.com> > *Envoy=C3=A9 :* 8 f=C3=A9vrier 2022 15:19 > *=C3=80 :* Homotopy Type Theory > *Objet :* [HoTT] Formalization of =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84= =A4/2=E2=84=A4 in Cubical Agda completed > > We are happy to announce that we have finished a formalization of > =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/2=E2=84=A4 in Cubical Agda. M= ost of the code has been written by my PhD > student Axel Ljungstr=C3=B6m and the proof largely follows Guillaume Brun= erie's > PhD thesis. For details and a summary see: > > > https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/= Summary.agda > > The proof involves a lot of synthetic homotopy theory: LES of homotopy > groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey, > Z-cohomology (with graded commutative ring structure), Gysin sequence, th= e > Hopf invariant, Whitehead product... Most of this was written by Axel und= er > my supervision, but some results are due to other contributors to the > library, in particular Lo=C3=AFc Pujet (3x3 lemma for pushouts, total spa= ce of > Hopf fibration), KANG Rongji (Blakers-Massey), Evan Cavallo (Freudenthal > and lots of clever cubical tricks). > > Our proof also deviates from the one in Guillaume's thesis in two major > ways: > > 1. We found a direct encode-decode proof of a special case of corollary > 3.2.3 and proposition 3.2.11 which is needed for =CF=80=E2=82=84(S=C2=B3)= . This allows us to > completely avoid the use of the James construction of Section 3 in the > thesis (shortening the pen-and-paper proof by ~15 pages), but the price w= e > pay is a less general final result. > > 2. With Guillaume we have developed a new approach to Z-cohomology in > HoTT, in particular to the cup product and cohomology ring (see > https://drops.dagstuhl.de/opus/volltexte/2022/15731/). This allows us to > give fairly direct construction of the graded commutative ring H*(X;Z), > completely avoiding the smash product which has proved very hard to work > with formally (and also informally on pen-and-paper as can be seen by the > remark in Guillaume's thesis on page 90 just above prop. 4.1.2). This > simplification allows us to skip Section 4 of the thesis as well, > shortening the pen-and-paper proof by another ~15 pages. This then leads = to > various further simplifications in Section 5 (Cohomology) and 6 (Gysin > sequence). > > With these mathematical simplifications the proof got a lot more > formalization friendly, allowing us to establish an equivalence of groups > by a mix of formal proof and computer computations. In particular, Cubica= l > Agda makes it possible to discharge several small steps in the proof > involving univalence and HITs purely by computation. This even reduces so= me > gnarly path algebra in the Book HoTT pen-and-paper proof to "refl". > Regardless of this, we have not been able to reduce the whole proof to a > computation as originally conjectured by Guillaume. However, if someone > would be able to do this and compute that the Brunerie number is indeed 2 > purely by computer computation there would still be the question what thi= s > has to do with =CF=80=E2=82=84(S=C2=B3). Establishing this connection for= mally would then > most likely involve formalizing (large) parts of what we have managed to = do > here. Furthermore, having a lot of general theory formalized will enable = us > to prove more results quite easily which would not be possible from just > having a very optimized computation of a specific result. > > Best regards, > Anders and Axel > > -- > 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 toHomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2= USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%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/QB1PR01MB29481886234= F6ECEB3006C31FD2D9%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.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/021D547B-986C-4E18-B= 4F2-A105376DE6EB%40gmail.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/CAO0tDg5V2dMm71XbqR4dt%2BK2jCZpE-myseR7385H%3DZGbpoWytQ%= 40mail.gmail.com. --00000000000088f38805d78e1a8f Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I think it goes back to Pontryagin from the late 1930s, th= ough with a rather different argument. The history is a bit confusing becau= se Pontryagin famously made a mistake in computing \pi_4(S^2). But his calc= ulation of \pi_4(S^3) was fine.=C2=A0 See Theorem 2' and 2'' of= =C2=A0https://people.math.rochester.edu/faculty/doug/otherpapers/pont= 2.pdf which I found at this webpage that has more history:=C2=A0ht= tps://people.math.rochester.edu/faculty/doug/AKpapers.html#2-stem
<= br>
Best,

Noah

On Tue, Feb 8, 2022 = at 10:09 PM Steve Awodey <awodey@cmu.e= du> wrote:
Someone please correct me if I am wrong,= =C2=A0
but I believe that this was originally proved by J-P Serre in hi= s 1951 dissertation (using spectral sequences).
So we are about 7= 0 years behind - but catching up fast!

Congratulat= ions to all who contributed to this milestone!

Uni= valent regards,

Steve


On Feb 8, 2022, at 6:24 PM, Joyal, Andr=C3=A9 <<= a href=3D"mailto:joyal.andre@uqam.ca" target=3D"_blank">joyal.andre@uqam.ca= > wrote:

Dear Anders,

=
Congratulation to you and Axe= l for doing this!
It was= a problem for many years!
We can now honestly say that cubical Agda is a serious tool in homotopy = theory!
It is an amazing= piece of work.
Thanks t= o all, starting with Guillaume.

Best wi= shes,
Andre
=
De :=C2=A0homo= topytypetheory@googlegroups.com=C2=A0<homotopytypetheory@= googlegroups.com> de la part de Anders Mortberg <andersmortberg@gmail.com&= gt;
Envoy=C3=A9 :=C2=A08 f=C3=A9vrier 2022 15:19
= =C3=80 :=C2=A0Homotopy Type Theory <homotopytypetheory= @googlegroups.com>
Objet :=C2=A0[HoTT] Formal= ization of =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/2=E2=84=A4 in Cubical= Agda completed
=C2=A0
We are happy to announce that we have finished a formalization = of=C2=A0 =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/2=E2=84=A4=C2=A0 in Cub= ical Agda. Most of the code has been written by my PhD student Axel Ljungst= r=C3=B6m and the proof largely follows Guillaume Brunerie's PhD thesis.= For details and a summary see:

https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4= S3/Summary.agda

The proof involves a lot of synthetic homot= opy theory: LES of homotopy groups, Hopf fibration, Freudenthal suspension = theorem, Blakers-Massey, Z-cohomology (with graded commutative ring structu= re), Gysin sequence, the Hopf invariant, Whitehead product... Most of this = was written by Axel under my supervision, but some results are due to other= contributors to the library, in particular Lo=C3=AFc Pujet (3x3 lemma for = pushouts, total space of Hopf fibration), KANG Rongji (Blakers-Massey), Eva= n Cavallo (Freudenthal and lots of clever cubical tricks).=C2=A0

Our proof also deviates from the one in Gui= llaume's thesis in two major ways:

1. We found a direct encode= -decode proof of a special case of corollary 3.2.3 and proposition 3.2.11 w= hich is needed for =CF=80=E2=82=84(S=C2=B3). This allows us to completely a= void the use of the James construction of Section 3 in the thesis (shorteni= ng the pen-and-paper proof by ~15 pages), but the price we pay is a less ge= neral final result.=C2=A0

2. With Guillaume we have dev= eloped a new approach to Z-cohomology in HoTT, in particular to the cup pro= duct and cohomology ring (see=C2=A0https://drops.dagst= uhl.de/opus/volltexte/2022/15731/). This allows us to give fairly direc= t construction of the graded commutative ring H*(X;Z), completely avoiding = the smash product which has proved very hard to work with formally (and als= o informally on pen-and-paper as can be seen by the remark in Guillaume'= ;s thesis on page 90 just above prop. 4.1.2). This simplification allows us= to skip Section 4 of the thesis as well, shortening the pen-and-paper proo= f by another ~15 pages. This then leads to various further simplifications = in Section 5 (Cohomology) and 6 (Gysin sequence).

With these ma= thematical simplifications the proof got a lot more formalization friendly,= allowing us to establish an equivalence of groups by a mix of formal proof= and computer computations. In particular, Cubical Agda makes it possible t= o discharge several small steps in the proof involving univalence and HITs = purely by computation. This even reduces some gnarly path algebra in the Bo= ok HoTT pen-and-paper proof to "refl". Regardless of this, we hav= e not been able to reduce the whole proof to a computation as originally co= njectured by Guillaume. However, if someone would be able to do this and co= mpute that the Brunerie number is indeed 2 purely by computer computation t= here would still be the question what this has to do with =CF=80=E2=82=84(S= =C2=B3). Establishing this connection formally would then most likely invol= ve formalizing (large) parts of what we have managed to do here. Furthermor= e, having a lot of general theory formalized will enable us to prove more r= esults quite easily which would not be possible from just having a very opt= imized computation of a specific result.

Best regards,=C2=A0
Anders and Axel

--=C2=A0
You received this message becaus= e 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 toHomotopyTypeTheory+unsubscribe@googlegroups.com<= /a>.
To view this discussion on the web visit=C2=A0https://groups.google.com/d/msgid/H= omotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%40m= ail.gmail.com.

--= =C2=A0
You received this message because you are subscribed t= o the Google Groups "Homotopy Type Theory" group.
To unsub= scribe from this group and stop receiving emails from it, send an email to<= span>=C2=A0HomotopyTypeTheory+unsubscribe@googlegrou= ps.com.
To v= iew this discussion on the web visit=C2=A0https://groups.google.com/d/msgi= d/HomotopyTypeTheory/QB1PR01MB29481886234F6ECEB3006C31FD2D9%40QB1PR01MB2948= .CANPRD01.PROD.OUTLOOK.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://g= roups.google.com/d/msgid/HomotopyTypeTheory/021D547B-986C-4E18-B4F2-A105376= DE6EB%40gmail.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/CAO0tDg5V2dMm71XbqR4dt%2BK2jC= ZpE-myseR7385H%3DZGbpoWytQ%40mail.gmail.com.
--00000000000088f38805d78e1a8f--