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=HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,RCVD_IN_MSPIKE_H2, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 4106 invoked from network); 9 Feb 2022 03:09:52 -0000 Received: from mail-yb1-f190.google.com (209.85.219.190) by inbox.vuxu.org with ESMTPUTF8; 9 Feb 2022 03:09:52 -0000 Received: by mail-yb1-f190.google.com with SMTP id 2-20020a251302000000b006118f867dadsf1996425ybt.12 for ; Tue, 08 Feb 2022 19:09:52 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1644376190; cv=pass; d=google.com; s=arc-20160816; b=Q5ozcLHkuK88mol95LRsU8nFnT5OeNsnDdwTZlOIONqWFRqOIS0WZH5xsLDhf+Etkb 4urrEtO95Zwxah8hhsvYA58q8lLOBIB5fEcknnNoLkNZvFkPkUkXSsYGsohK40hlWEDe Gq6JFcddm8kkl8wkbgc6wMjqK4AAVsdD4CEMXtz5UjemNQ0GOQyzwIv+p8CuDRORKdZX 9KbB+Y5dyWPIo9StrngxldfWe0W/7B2WYWaObIDTJpc+vgzHF++qsCtWNgct9ptdPFGW W2QSKk574t2uDYa83wz11WdKTgXFJsBaumvZPi3Fv+VK1pTb9shNYkUHQ2sQPcpkFj1x pRqg== 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:references:to:cc:in-reply-to:date :subject:mime-version:message-id:from:sender; bh=KjUBa9yN+flSOHv6vONDDBd3D6xUdEGx1fzqJrP/AkA=; b=YU9A0kM0wP6MK+8eqOxRPPIgKab7dnQlN8iRJS19dOKBXhEQGDtBYjVFW2AyWgwUIS n5eTLdLzJTTSooKW2SSkl2L4u6dp1+Ptn0ID7X4tHqa0NCUW9E/QFN53wCiexHXakRTj 4uoVcRPGK+9ipK4T+JPP6V0w0cxvnrTPnLbVXaXVW2rITxte404mZ5hO+4m8fad9QAN5 ky1XON478AJc/QL8AwqsTg6Va/FAsZJytobZgKie2wkHdEdtw8Ek52lx4oa7Ida5yS/V CQDdeGR22tPK6Nm2tq8arc6X/qwwRGhqYoI72jNZe39XKrZXPjD4yQIHeBAe+0lhWZMg FE6w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrew.cmu.edu header.s=google-2021 header.b=BBZfwIYr; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=qtNCzPMq; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f36 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:sender:from:message-id:mime-version:subject:date :in-reply-to:cc:to:references: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=KjUBa9yN+flSOHv6vONDDBd3D6xUdEGx1fzqJrP/AkA=; b=WvdUOCxKMTY6A0z5Is0l2eDR4KwAmn1gyZDcpecpBd2UbeMfo1fquZqz8SVLpNnZU5 iJOhnhK75OOa5vmF1FS7glahnX57V0DDe2d6hhQF6OlNFuU96NcQREel6sTFMSZKk+yo bl92H/WESpGNCxZbdCBu4UMljkO9pSrnoRN81KTsnV9hM9QHSAeSSw1ZDAjKSbIDQGdr mzXIz4n2Trv+SPdCecM4MuyJ51HeU6Blp8YhiphGPI33rQXoC+UgLqhetB280Xq0mDgw W9FhzyewJ/7v4g6f39FCTPwXYOGTJy9o5RvOiV8pfs1oRKrncrKYdbdwvlCQWUBQ6dSX td6Q== X-Gm-Message-State: AOAM533/33AFh3/t+zLWYpqGjLsqPFK3Vrv3978+XXqRaf8Gd3mq/e26 C6pxkfv86S7pKxpeFp13Sic= X-Google-Smtp-Source: ABdhPJxHnDGeX5AgRdxXrjyzfQ3j5FjTMm6UP9eLfPVZHLdb6lc8jCbGMtUK9mhTbfDxrJv7K2LOEA== X-Received: by 2002:a0d:ed44:: with SMTP id w65mr218785ywe.473.1644376190333; Tue, 08 Feb 2022 19:09:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:2d44:: with SMTP id t65ls411042ywt.8.gmail; Tue, 08 Feb 2022 19:09:49 -0800 (PST) X-Received: by 2002:a81:ef0a:: with SMTP id o10mr250925ywm.384.1644376188886; Tue, 08 Feb 2022 19:09:48 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1644376188; cv=none; d=google.com; s=arc-20160816; b=ksOzAMoXXT/SeAf/SNVklMtovnH+kzZgf7lheUOX+ee96PEP5+EdX5dkl+DvdDzP1R PESULOOOmgWHTT6rtTzojtAV/417cwg3gcav6xXa/2buTz5iJi5Vo2YYZYhP5jkmrsBt yWAJejewRQy5uVAwunCLzamdg0/9T1kIuZUGPeXSC4DrXg78flvweZhanOLG9gvgJKKM jRT56oGTmFsuKSVW/+yvyzaVR7ZY3rhREmsSbQEUqQfHxKDnj7wIbVJSRTc+VT9K0IM7 j1YTZRBFIA7tdtOemGDORe6onQMvzVugdkIYr0UunV3UFi+ZKjraWOkoojzL6WNSTLZP qNXA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:sender:dkim-signature:dkim-signature; bh=RP811titq4iLSNaz0LWv6KxMVAf0mOv58EVQrETAwnk=; b=ngZb5T0hgp4jyFCOWyF785IoWlUDwrPhiDZbVS9XmsKqqvzmMCBhCWbrnArtXyvtha bIjjzZkMohSAkJFAzQatAXS6Dmlhj0WEpYckAJ4UJsYbSzjAHCvIlq12/RYTEUcw+C1y WRS2ad81e3z/FbO5fbOkxK4elTFigNq1ygyo9jSQT4LtVvwi+A9H1HkHD+3OaHAYZvwa cZKSB6Pc3XHEOLTMNhH5HYH08ZCyD50pCx4IrsS0KcXSZwsXycjz+3SPm6ZFG3wTJ+br at/BQGWJGClIkWF8c9bhKCJiFGOvuX9N147ML+vzwDqymP674v3oPusPqiVuiDC+cfKt yYwA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrew.cmu.edu header.s=google-2021 header.b=BBZfwIYr; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=qtNCzPMq; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f36 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-qv1-xf36.google.com (mail-qv1-xf36.google.com. [2607:f8b0:4864:20::f36]) by gmr-mx.google.com with ESMTPS id j72si108012ybg.4.2022.02.08.19.09.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 08 Feb 2022 19:09:48 -0800 (PST) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f36 as permitted sender) client-ip=2607:f8b0:4864:20::f36; Received: by mail-qv1-xf36.google.com with SMTP id k4so813122qvt.6 for ; Tue, 08 Feb 2022 19:09:48 -0800 (PST) X-Received: by 2002:a05:6214:1c47:: with SMTP id if7mr254698qvb.128.1644376188412; Tue, 08 Feb 2022 19:09:48 -0800 (PST) Received: from smtpclient.apple (pool-100-6-43-241.pitbpa.fios.verizon.net. [100.6.43.241]) by smtp.gmail.com with ESMTPSA id u63sm7783428qkh.43.2022.02.08.19.09.47 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 08 Feb 2022 19:09:47 -0800 (PST) Sender: Steve Awodey From: Steve Awodey Message-Id: <021D547B-986C-4E18-B4F2-A105376DE6EB@gmail.com> Content-Type: multipart/alternative; boundary="Apple-Mail=_AF81A8F2-E8E3-41A1-922B-668490BA1031" Mime-Version: 1.0 (Mac OS X Mail 15.0 \(3693.40.0.1.81\)) Subject: =?UTF-8?B?UmU6IFtIb1RUXSBGb3JtYWxpemF0aW9uIG9mIM+A4oKEKFPCsyniiYXihKQvMuKEpCBpbg==?= =?UTF-8?B?IEN1YmljYWwgQWdkYSBjb21wbGV0ZWQ=?= Date: Tue, 8 Feb 2022 22:09:46 -0500 In-Reply-To: Cc: Homotopy Type Theory To: =?utf-8?B?IkpveWFsLCBBbmRyw6ki?= , Anders Mortberg References: X-Mailer: Apple Mail (2.3693.40.0.1.81) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrew.cmu.edu header.s=google-2021 header.b=BBZfwIYr; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=qtNCzPMq; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f36 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.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: , --Apple-Mail=_AF81A8F2-E8E3-41A1-922B-668490BA1031 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" Someone please correct me if I am wrong,=20 but I believe that this was originally proved by J-P Serre in his 1951 diss= ertation (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= : >=20 > Dear Anders, >=20 > 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 t= heory! > It is an amazing piece of work. > Thanks to all, starting with Guillaume. >=20 > Best wishes, > Andre > De : homotopytypetheory@googlegroups.com > de la part de Anders Mortberg > > 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 > =20 > 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. Most of t= he code has been written by my PhD student Axel Ljungstr=C3=B6m and the pro= of largely follows Guillaume Brunerie's PhD thesis. For details and a summa= ry see: >=20 > https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/= Summary.agda >=20 > The proof involves a lot of synthetic homotopy theory: LES of homotopy gr= oups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey, Z-coh= omology (with graded commutative ring structure), Gysin sequence, the Hopf = invariant, Whitehead product... Most of this was written by Axel under my s= upervision, 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), Evan Cavallo (Freudenthal and lot= s of clever cubical tricks).=20 >=20 > Our proof also deviates from the one in Guillaume's thesis in two major w= ays: >=20 > 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). T= his allows us to completely avoid the use of the James construction of Sect= ion 3 in the thesis (shortening the pen-and-paper proof by ~15 pages), but = the price we pay is a less general final result.=20 >=20 > 2. With Guillaume we have developed a new approach to Z-cohomology in HoT= T, 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 t= he graded commutative ring H*(X;Z), completely avoiding the smash product w= hich 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 ju= st above prop. 4.1.2). This simplification allows us to skip Section 4 of t= he thesis as well, shortening the pen-and-paper proof by another ~15 pages.= This then leads to various further simplifications in Section 5 (Cohomolog= y) and 6 (Gysin sequence). >=20 > With these mathematical simplifications the proof got a lot more formaliz= ation friendly, allowing us to establish an equivalence of groups by a mix = of formal proof and computer computations. In particular, Cubical Agda make= s it possible to discharge several small steps in the proof involving univa= lence and HITs purely by computation. This even reduces some gnarly path al= gebra in the Book HoTT pen-and-paper proof to "refl". Regardless of this, w= e have not been able to reduce the whole proof to a computation as original= ly conjectured by Guillaume. However, if someone would be able to do this a= nd compute that the Brunerie number is indeed 2 purely by computer computat= ion there 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 = involve formalizing (large) parts of what we have managed to do here. Furth= ermore, having a lot of general theory formalized will enable us to prove m= ore results quite easily which would not be possible from just having a ver= y optimized computation of a specific result. >=20 > Best regards,=20 > Anders and Axel > --=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= email toHomotopyTypeTheory+unsubscribe@googlegroups.com . > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%= 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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com . > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/QB1PR01MB29481886234F6ECEB3006C31FD2D9%40QB1PR01MB2948= .CANPRD01.PROD.OUTLOOK.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/021D547B-986C-4E18-B4F2-A105376DE6EB%40gmail.com. --Apple-Mail=_AF81A8F2-E8E3-41A1-922B-668490BA1031 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8" 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!<= /div>

Congratulations t= o all who contributed to this milestone!

Univalent regards,

Steve


On Feb 8, 2022, at 6:24 PM, Joyal, Andr=C3=A9 <joyal.andre@uqam.ca> wrote:

Dear Anders,

Congratulation to you and Axel for doing this!
It was a problem for many years!<= /div>
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.

<= div style=3D"font-size: 12pt; font-style: normal; font-variant-caps: normal= ; font-weight: normal; letter-spacing: normal; text-align: start; text-inde= nt: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -web= kit-text-stroke-width: 0px; text-decoration: none; font-family: Calibri, Ar= ial, Helvetica, sans-serif;" class=3D"">Best wishes,
Andre
De : homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> de la part de A= nders Mortberg <a= ndersmortberg@gmail.com>
Envoy=C3=A9 : 8 f=C3=A9vrier 2022 15= :19
=C3=80 : Homotopy Type Theory <homotopytypetheory@googlegroups.com= >
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
&nb= sp;
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 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/mast= er/Cubical/Homotopy/Group/Pi4S3/Summary.agda

The proof involves a lot of synthetic homotopy theory: L= ES of homotopy groups, Hopf fibration, Freudenthal suspension theorem, Blak= ers-Massey, Z-cohomology (with graded commutative ring structure), Gysin se= quence, the Hopf invariant, Whitehead product... Most of this was written b= y 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, tot= al space of Hopf fibration), KANG Rongji (Blakers-Massey), Evan Cavallo (Fr= eudenthal and lots of clever cubical tricks). 

Our proof also deviates from the one in Guillaume's the= sis in two major ways:

1. We found a direct encode-deco= de 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 th= e pen-and-paper proof by ~15 pages), but the price we 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 h= ttps://drops.dagstuhl.de/opus/volltexte/2022/15731/). This allows us to= give fairly direct construction of the graded commutative ring H*(X;Z), co= mpletely 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 remar= k in Guillaume's thesis on page 90 just above prop. 4.1.2). This simplifica= tion 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 si= mplifications in Section 5 (Cohomology) and 6 (Gysin sequence).

With these mathematical simplifications t= he 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 to discharge several small st= eps in the proof involving univalence and HITs purely by computation. This = even reduces some 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 pr= oof to a computation as originally conjectured by Guillaume. However, if so= meone would be able to do this and compute that the Brunerie number is inde= ed 2 purely by computer computation there 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 involve formalizing (large) parts of what w= e have managed to do here. Furthermore, having a lot of general theory form= alized will enable us to prove more results quite easily which would not be= possible from just having a very optimized computation of a specific resul= t.

Best regards, 
Anders and Axel

-- 
You received this me= ssage because you are subscribed to the Google Groups "Homotopy Type Theory= " group.
To unsubscribe from this group and stop receiving em= ails from it, send an email toHomotopyTypeTheory+unsubscribe@googlegroup= s.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmb%2BAt_B= wp_2USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%40mail.gmail.com.
<= /div>

-- 
You received= this message because you are subscribed to the Google Groups "Homotopy Typ= e Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyTypeTheory+unsubscribe@googlegro= ups.com.
To view this discussion on the web visit https://groups.google.com/d/m= sgid/HomotopyTypeTheory/QB1PR01MB29481886234F6ECEB3006C31FD2D9%40QB1PR01MB2= 948.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://groups.google.com/d/msg= id/HomotopyTypeTheory/021D547B-986C-4E18-B4F2-A105376DE6EB%40gmail.com.=
--Apple-Mail=_AF81A8F2-E8E3-41A1-922B-668490BA1031--