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 18151 invoked from network); 11 Feb 2022 11:30:18 -0000 Received: from mail-pj1-x103e.google.com (2607:f8b0:4864:20::103e) by inbox.vuxu.org with ESMTPUTF8; 11 Feb 2022 11:30:18 -0000 Received: by mail-pj1-x103e.google.com with SMTP id gj12-20020a17090b108c00b001b89b5f3dd4sf8073349pjb.6 for ; Fri, 11 Feb 2022 03:30:18 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1644579016; cv=pass; d=google.com; s=arc-20160816; b=DMf65XD2jMoBVkRT6S/kCGRoOF8V7q94B83w9k7UtHBPJ31db3FeyYVOC15MLdl+DK jHku9xcMEPvP5OPp33emIgkd7lVvlkXRZnoT4wSno/Ahvw89lK+lk13TjqHe5FqXQ3mO SnfnAQ4S7y/K5AUFZwU2lcMHuOu0+iBnIHWSrGaQS5Mkn1qO2fSeBJgCnOelw9CVB7jI IB8m/nRFDBoa4EYSpjcLYjmEDvTfHS7quf0JUOuGPE3ykspBV4tOsSfVrjBdiuS+1ijC /OVzZX8hEs4vxkszqBgW+yvcbqjp6vq/6W7gTrD8NewiI7C+VjWuM7lQ3pYN37eHkU6u sJLw== 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=D4Wbw6L5KjRHEzAPCfUvZHpgK2W85yv7HR0CAq1wxN4=; b=a0y9vbztzElHjDw6BUPAQlYjKkUL3mR7njHE0/1nTyK1yNGohFl5N/esvsPn839dEW fn3KnrgBRibtfon8SFMQfO6nwOYBD1hE0LK4v1v6emhJjx0Gssw3yRqQ+R+pd3f4ZIwm SWmrcmjOF8MAnzLwSWWvYjYXl5dyR+i1+H8FR6Z7PGeJJbRvCiAeJs4LL43sw3BD8NMq lYhgfjcnLeLRDcJKj5g6PQv/Va95SLOOkUDX8yx7SLYA0WaOQTN7ccRrJesErEyvuSQb O7CG0osvdikQQtNKakssOVtaRb7oYKx0bL+A3oLFUEQC/nzVHMV+LwAJ9IVeKSPhNEc1 Gk3A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Zr+Jlo6q; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2c as permitted sender) smtp.mailfrom=andersmortberg@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=D4Wbw6L5KjRHEzAPCfUvZHpgK2W85yv7HR0CAq1wxN4=; b=NG/dj5iYCpRl0VImQHEFzMzsExrbIACT/eB1d/5hepPtRzTXRdvnFS1wd0OCvf7Z+W iLriKo9kqzjWIx3hKKyKGBs1YfLVZe4PuLKrozWSKPCQ19lpBQZAqCkseCGxfKE4+1vv rp1hrnn8RYPTtD73mHqQnfAFoKxf6dLcY1cUKO8yXjA1/ftAOZdOWzmB5iRK3azBh1Ap sHrE27unOdXEe3m7BbQ9ivoPGMqmVTJwWi+JCCugqL5ObbpoDoh0KiEoFkAeAtxWllcC O7ZbtylSYxBQsVKDO1e0JX9FtE0bgPltA6KyviLN0CIj8jcDfkRWLmO97F27nb3WU52H 25gg== 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=D4Wbw6L5KjRHEzAPCfUvZHpgK2W85yv7HR0CAq1wxN4=; b=M+5PFziAlk66Qvjg5/NfNkQ/VpE5KI+IRnS3nfHwu16BPEg6xUMQ9aBm2hyo9Mx8dS IwQ3ErX4Rmo7UJtmpMHrilXvPw7qYhne+NW3zAXryn9E/oUG9nr8fTEEzPRuDRLPvUl1 KaaKx6zT3m01uJalG1Z2LG/BrGJ5aV/etRKw8piFPZTSoFbG60rHvz7HU3eQ7Ms30FhM Zpm1dfflPSi1cHcVMezNrrAMFy7qcTpH/H+BxxQtnC8CxtIPc8L/HyMTAjn3FkhGSveW ef9+73FuQthgLubasRM5nTen1mk6d9/b35gVhekU7jyhh3pV7Ty1kYREcd8ubZM1Y1MZ Vzxw== 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=D4Wbw6L5KjRHEzAPCfUvZHpgK2W85yv7HR0CAq1wxN4=; b=rLyAM3vO4gEPHfugaUnqIVhujc6bdE9F1B+Ztzj7Glo3m4+75iiOxK1hs71xByiy+9 ELAN85L11fYpLrK1VYzmY8vqXJl1nYHboYFxwV8VYXVonm0SPNSxKQVEVc1272a5mDOo o8npfmWB4yF9NEdSQodcUCrV1a+Lqwk3kv7XSv36+MiuCt0smJIVL4twqVvcxgjE1Rtc t8VIKjoV2vx6fUM0SiR7kC7PAOb2epy6TEYGDnmNwixJvDg6io8LoDLpFjFksoYMUVDw vuEA6F/hE4D6BvyOis7F/q6KDCfm4Xxm4DD3+f3yOcfT57abdhewJFtUt/yr9yPShUtv 2JEg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5318G9copT8sxXmZwNqXaO9WazJ8qHcQtdn1SR+WCIvNJwNQLGSc aWkoJzq1u+n5XJr0632zA4U= X-Google-Smtp-Source: ABdhPJwKOh+D0QvwSlmANrb5Aj14f0Fd3eLg+PDhxoyaxLFiMXMN+ACk+yfh90TqPOszh1B3guMVYA== X-Received: by 2002:a62:7653:: with SMTP id r80mr1239923pfc.63.1644579016534; Fri, 11 Feb 2022 03:30:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:ecc1:: with SMTP id a1ls5846766plh.5.gmail; Fri, 11 Feb 2022 03:30:15 -0800 (PST) X-Received: by 2002:a17:90b:98:: with SMTP id bb24mr2060537pjb.175.1644579015108; Fri, 11 Feb 2022 03:30:15 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1644579015; cv=none; d=google.com; s=arc-20160816; b=H8h14Q8QyLHhBb++0gOAUfsNNsj7AEs0b7rhB+I92n3zPuaa0Jf/uRhuDr5chP8Guw IYyWdhgf2tOPy7DiuC/C+6dVTnqaqkmW3YQWy3uIuttiOoqYQLpgl+TKTLLwUtEp2OV2 DwByViw48rtBr11p2Sx7jiki9kfTf/4EZF1RIFqtWM3Z/hz4imO9t7LZIE2fgQhVlfze Buco/gFBpDEmPMeSNQ2n6CAiIvSOMunN66NOux7iNf8CxSQlJ298iKUfHW/ECk/AdNtb EUCOCMrF5TqI7DF54GVSx+Y/EKRPW7Upv7Tk0x58gHFeDCPplpV3F8N7pR0fdNzrNRBP z3mA== 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=x3bWytDXYnMCsnG5e2k9XOtIpbfQE/71Sx7dMZBDIsE=; b=bpIlQL1JQ2YFvA9gFBdZOGNpTOj3rO0RR0UhGa16SCzMtI3pCR9QcDvRvp1ZstCAH3 a/efm4Gpu08U5C+NJS3pUV6nZmuZAiiWpgK9WojgOceIy7ImHWa14HI+d3FgH36vUd5V 2Yqp/kyKel4k91I/Lf31WfNWjX6vP/26FQbcRE6uCNQybGwcolUKUj+ak7tbvAH72jAP kcmGoSnj2OKgbmFl0c0L0SvzWflqPUW5Ggnj2mnGo/A/H5p98w3tjsneLgAYLAKEeprd VZFt0UpsC98Gi63u+6VjP0vZOK8lgGXZCpJXbjWKGd/AFvzylwdUHFx78m+LfK6EHIKq vfVA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Zr+Jlo6q; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2c as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vs1-xe2c.google.com (mail-vs1-xe2c.google.com. [2607:f8b0:4864:20::e2c]) by gmr-mx.google.com with ESMTPS id e18si204113plo.3.2022.02.11.03.30.15 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 11 Feb 2022 03:30:15 -0800 (PST) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2c as permitted sender) client-ip=2607:f8b0:4864:20::e2c; Received: by mail-vs1-xe2c.google.com with SMTP id w6so9446612vsf.3 for ; Fri, 11 Feb 2022 03:30:14 -0800 (PST) X-Received: by 2002:a67:d299:: with SMTP id z25mr327022vsi.83.1644579013918; Fri, 11 Feb 2022 03:30:13 -0800 (PST) MIME-Version: 1.0 References: <021D547B-986C-4E18-B4F2-A105376DE6EB@gmail.com> In-Reply-To: From: Anders Mortberg Date: Fri, 11 Feb 2022 12:29:37 +0100 Message-ID: Subject: =?UTF-8?B?UmU6IFtIb1RUXSBGb3JtYWxpemF0aW9uIG9mIM+A4oKEKFPCsyniiYXihKQvMuKEpCBpbg==?= =?UTF-8?B?IEN1YmljYWwgQWdkYSBjb21wbGV0ZWQ=?= To: Homotopy Type Theory Cc: Steve Awodey , =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , Urs Schreiber Content-Type: multipart/alternative; boundary="000000000000ee038105d7bc6328" X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Zr+Jlo6q; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2c as permitted sender) smtp.mailfrom=andersmortberg@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: , --000000000000ee038105d7bc6328 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks a lot to Andr=C3=A9, Steve and everyone else that wrote to us privat= ely for your kind words and congratulations! It's very nice to be 100% sure that the Brunerie number is indeed 2 after spending far too much time and computer power on trying to compute it :-) I agree with Andr=C3=A9 that this shows that Cubical Agda is a great tool f= or developing a lot of homotopy theory, however there are two issues that I should mention: 1. It's unknown if Cubical Agda has a model in spaces (i.e. Kan sSet). 2. It's unknown if any cubical type theory has models in some wide class of infty-categories/topoi. I find 1 less interesting than 2 as =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84= =A4/2=E2=84=A4 is a very well established result in spaces (thanks to Noah and Urs for the references!). Furthermore, I expect there to be no problem to translate the proof to cartesian cubical type theory which can then be interpreted in spaces (using the equivariant cartesian model of Awodey-Cavallo-Coquand-Riehl-Sattler). It would of course be a lot of engineering work to change Cubical Agda to be based on cartesian ctt and to rewrite the proof, so I would much rather see some kind of conservativity result relating the two type theories... For problem 2 I really hope someone who knows more about infty-categories can make some progress or for someone to prove a conservativity result relating cubical type theory to HoTT (for which the situation is much clearer thanks to Shulman). I guess I could also mention that the Coquand-Huber-Sattler ( https://arxiv.org/abs/1902.06572) results don't apply to our proof even if we would remove all reversals. As we still manage to reduce many goals to computations involving univalence our proof would not go through in a cubical type theory where one drops the computation rules for composition/transp/hcomp. Despite these problems I'm still very pleased that we managed to formalize the result and develop all of this theory formally. I'm also hopeful that we'll find some solutions to the problems above and that we'll one day have a system which has the good computational properties of cubical type theory combined with a lot of interesting models like HoTT. Best, Anders On Wed, Feb 9, 2022 at 5:44 AM Urs Schreiber wrote: > Just to add that Pontrjagin had announced the result > (on the second stem) already at the ICM in 1936: > > ncatlab.org/nlab/files/PontrjaginSurLesTransformationDesSpheres.pdf > ncatlab.org/nlab/show/second+stable+homotopy+group+of+spheres#reference= s > > and that the method he used was, of course, his theorem > on identifying Cohomotopy with Cobordism: > > ncatlab.org/nlab/show/Pontryagin+theorem > > Two decades later Thom would make a splash by re-inventing (and > generalizing) > this method, and it was only then that Pontryagin bothered to write more = of > an exposition of his method (references behind the above link). > > Best wishes, > urs > > On Wed, Feb 9, 2022 at 8:16 AM Noah Snyder wrote: > > > > 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 wr= ote: > >> > >> 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 homotop= y > 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 majo= r > ways: > >> > >> 1. We found a direct encode-decode proof of a special case of corollar= y > 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 > . > > > > -- > > 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/CAO0tDg5V2dMm71XbqR4= dt%2BK2jCZpE-myseR7385H%3DZGbpoWytQ%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/CAMWCpp%3Da8uKYsNFS%3D0wzYNyOT411zSpEzYD2V1FRe4KuU%2Bgjy= w%40mail.gmail.com. --000000000000ee038105d7bc6328 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks a lot to Andr=C3=A9, Steve an= d everyone else that wrote to us privately for your kind words and congratu= lations! It's very nice to be 100% sure that the Brunerie number is ind= eed 2 after spending far too much time and computer power on trying to comp= ute it :-)


I agree with Andr=C3=A9 = that this shows that Cubical Agda is a great tool for developing a lot of h= omotopy theory, however there are two issues that I should mention:

1. It's unknown if Cubical Agda has a model in spaces= (i.e. Kan sSet).

2. It's unknown if any cubic= al type theory has models in some wide class of infty-categories/topoi.

I find 1 less interesting than 2 as =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2= =84=A4/2=E2=84=A4 is a very well established result in space= s (thanks to Noah and Urs for the references!). Furthermore, I expect there= to be no problem to translate the proof to cartesian cubical type theory w= hich can then be interpreted in spaces (using the equivariant cartesian mod= el of Awodey-Cavallo-Coquand-Riehl-Sattler). It would of course be a lot of= engineering work to change Cubical Agda to be based on cartesian ctt and t= o rewrite the proof, so I would much rather see some kind of conservativity= result relating the two type theories... For problem 2 I really hope someo= ne who knows more about infty-categories can make some progress or for some= one to prove a conservativity result relating cubical type theory to HoTT (= for which the situation is much clearer thanks to Shulman). I guess I could= also mention that the Coquand-Huber-Sattler (https://arxiv.org/abs/1902.06572) results don't app= ly to our proof even if we would remove all reversals. As we still manage t= o reduce many goals to computations involving univalence our proof would no= t go through in a cubical type theory where one drops the computation rules= for composition/transp/hcomp.

Despite these = problems I'm still very pleased that we managed to formalize the result= and develop all of this theory formally. I'm also hopeful that we'= ll find some solutions to the problems above and that we'll one day hav= e a system which has the good computational properties of cubical type theo= ry combined with a lot of interesting models like HoTT.

<= /div>
Best,
Anders


On Wed, Feb 9, 2022 at 5:44 AM Urs= Schreiber <urs.schreiber@googlemail.com> wrote:
Just to add that Pontrjagin had announced= the result
(on the second stem) already at the ICM in 1936:

=C2=A0 ncatlab.org/nlab/fi= les/PontrjaginSurLesTransformationDesSpheres.pdf
=C2=A0 ncatlab.org/nl= ab/show/second+stable+homotopy+group+of+spheres#references

and that the method he used was, of course, his theorem
on identifying Cohomotopy with Cobordism:

=C2=A0ncatlab.org/nlab/show/Pontryagin+theorem
Two decades later Thom would make a splash by re-inventing (and generalizin= g)
this method, and it was only then that Pontryagin bothered to write more of=
an exposition of his method (references behind the above link).

Best wishes,
urs

On Wed, Feb 9, 2022 at 8:16 AM Noah Snyder <nsnyder@gmail.com> wrote:
>
> I think it goes back to Pontryagin from the late 1930s, though with a = rather different argument. The history is a bit confusing because Pontryagi= n famously made a mistake in computing \pi_4(S^2). But his calculation of \= pi_4(S^3) was fine.=C2=A0 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.roc= hester.edu/faculty/doug/AKpapers.html#2-stem
>
> Best,
>
> Noah
>
> On Tue, Feb 8, 2022 at 10:09 PM Steve Awodey <awodey@cmu.edu> 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 <joyal.andre@uqam.ca> 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 hom= otopy theory!
>> It is an amazing piece of work.
>> Thanks to all, starting with Guillaume.
>>
>> Best wishes,
>> Andre
>> ________________________________
>> De : homotopytypetheory@googlegroups.com <homotopytypetheory@go= oglegroups.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 <homotopytypetheory@googlegroups.co= m>
>> 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= =C2=A0 =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/2=E2=84=A4=C2=A0 in Cubic= al Agda. Most of the code has been written by my PhD student Axel Ljungstr= =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/Pi4S3/Summary.= agda
>>
>> The proof involves a lot of synthetic homotopy theory: LES of homo= topy 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 li= brary, in particular Lo=C3=AFc Pujet (3x3 lemma for pushouts, total space o= f 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 coro= llary 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 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 https://drops.dagstuhl.de/opus/volltexte/2022/15731/). This allows us to give fairly direct construction of the graded commuta= tive ring H*(X;Z), completely avoiding the smash product which has proved v= ery 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 le= ads to various further simplifications in Section 5 (Cohomology) and 6 (Gys= in sequence).
>>
>> With these mathematical simplifications the proof got a lot more f= ormalization friendly, allowing us to establish an equivalence of groups by= a mix of formal proof and computer computations. In particular, Cubical Ag= da makes it possible to discharge several small steps in the proof involvin= g univalence and HITs purely by computation. This even reduces some gnarly = path algebra in the Book HoTT pen-and-paper proof to "refl". Rega= rdless of this, we have not been able to reduce the whole proof to a comput= ation 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 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. Furthermore, having a lot of general theory formalized will ena= ble 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.c= om.
>> To view this discussion on the web visit ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2USKH= 9dAigFGx0GBrcG3XQQaqZmkr-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.co= m.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/QB1PR01MB29481= 886234F6ECEB3006C31FD2D9%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.co= m.
>> To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/021D547B-986C-4E18-B4F2-A105376DE6EB%40gmail.c= om.
>
> --
> You received this message because you are subscribed to the Google Gro= ups "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 http= s://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg5V2dMm71XbqR4dt%2BK= 2jCZpE-myseR7385H%3DZGbpoWytQ%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/CAMWCpp%3Da8uKYsNFS%3D0wzYN= yOT411zSpEzYD2V1FRe4KuU%2Bgjyw%40mail.gmail.com.
--000000000000ee038105d7bc6328--