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 14873 invoked from network); 24 May 2022 09:46:39 -0000 Received: from mail-yb1-xb40.google.com (2607:f8b0:4864:20::b40) by inbox.vuxu.org with ESMTPUTF8; 24 May 2022 09:46:39 -0000 Received: by mail-yb1-xb40.google.com with SMTP id j11-20020a05690212cb00b006454988d225sf15237713ybu.10 for ; Tue, 24 May 2022 02:46:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=8LhY5xvQkG2TJ00UiEM6IZe5G/ekHyrJqmZN2iTLoJo=; b=XiM7NkUF5ytiW49qXtw0E/zOyot46Qh/G7bzYrNg0MQmQR82zDkGp0hqPkVonQtJs1 9RRSaAAJ1Iz9JLBICk02q1dsyzFYmxY6idWdUZfNIIO3TX/GOEH7Vn2dwNJ/Te/2vA4e 8S9k6xCSeQRug028oZjb6C0A6pYUbUZF0gmZndc+ZnuK1aOeNUmDZJAzZerJNJoG/yKM Lno6aapftOHmu/X8Z2QsjY6MSAKfTO7U+7JOZjJ9lebesS+NzRcsi85lObtlY19Vb6wP oul5lYRttCpLAd0h8RErF+ygWuildG1oYiFHh4QlEOB5bniifMnxMlYdwKw/lQlYV2s9 G7JQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-subscribe:list-unsubscribe; bh=8LhY5xvQkG2TJ00UiEM6IZe5G/ekHyrJqmZN2iTLoJo=; b=RjU3F7Hw0gysVV+WZC5EnV4rJ/G/McCqwrW3rmfsHbUEsqMjUp8ZbWkcTTrOAh35lj 959H8ZEufoYIUvVIbU8DSp5ItiBi/C3GHUs9pJXsXWFMdewnGRBLeeFjckDwILkyV+lP ox1mojLwBmsKGH3OMF0igKyQMlduvcgViyXA0YQDpMPVZUIhaiH/VlYfCTH16Ma8yq48 4+P/pSnRfNvdxUynHV2b6ckYhDZH0tizUBzesytQBQ8zD01Axd1oP9qNgpAFJ/UaixaG x6mcVYj6MsKT4a8mTLDZic60qMQN3Pdo4GCNM+KtA3RKlzb9l90iRIDH0cxNEFMKq8Yh WknA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=8LhY5xvQkG2TJ00UiEM6IZe5G/ekHyrJqmZN2iTLoJo=; b=YuCc/8lranawguTR9n2Obm8k6w1viWAeRKfRRsbqYQovGy47kDQKYVx9ERWIH6rDwI oqQZt8o0/lUAwyyo50muf61frUk5DT+B4brrb0fHSd7OAe174kG2S+INGwP1QzT2Ettz wiu5I+GrKpZfvA90vvr5BqWhdlDARXLJ1CzW/KdiG2GmjStCFtwTKDJNhhQO5KYHpVnI 7kTt7mVX0aFzsXgpLCCZBd613FvVJRpDUESfUcobD4mjEe5ed870ShN1TVvc+8zXTBOV MiVP6/n89Vn0iPaD3+L2jCtSTXpnOPPCRYEY7AvZ/o9U2eXHz9zA4+N7N62bNK1QTOrE ceRg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533HAdr4uSOA6+QT3T7M2qrbuw3X7M/8Fn6zFi84u0X2uZbknmyH R838ezbri5TLKTwM+C9ZCbA= X-Google-Smtp-Source: ABdhPJyg2SyLJUcsY5yMHVsssYsWhAvn3y7939xMEF+AXoVV2R7QjZ8Fv7oY6615GQY/IDTOcF3SVw== X-Received: by 2002:a0d:e446:0:b0:2fb:9452:5c89 with SMTP id n67-20020a0de446000000b002fb94525c89mr27052201ywe.390.1653385597203; Tue, 24 May 2022 02:46:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6902:721:b0:64a:b88e:63c8 with SMTP id l1-20020a056902072100b0064ab88e63c8ls10129255ybt.11.gmail; Tue, 24 May 2022 02:46:36 -0700 (PDT) X-Received: by 2002:a25:d3d2:0:b0:64f:7190:a7d8 with SMTP id e201-20020a25d3d2000000b0064f7190a7d8mr17719578ybf.12.1653385595933; Tue, 24 May 2022 02:46:35 -0700 (PDT) Date: Tue, 24 May 2022 02:46:35 -0700 (PDT) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: <36c1e828-af3a-49c2-840b-1fae9897eeban@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] The Brunerie number is -2 MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_512_343870225.1653385595287" X-Original-Sender: andersmortberg@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: , ------=_Part_512_343870225.1653385595287 Content-Type: multipart/alternative; boundary="----=_Part_513_812432203.1653385595287" ------=_Part_513_812432203.1653385595287 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I did some digging and found the first commit with an attempt to compute=20 the number written by Guillaume Brunerie, Thierry Coquand and Simon Huber= =20 already in December 2014: https://github.com/simhu/cubical/commit/6e6278c6a626a9034789ab11cdd6bfb0bc8= 550be This code is written for the predecessor of cubicaltt called "cubical" and= =20 Thierry reminded me that it was based on the buggy regularity evaluator=20 which we eventually fixed in cubicaltt. I also think this cubical code is= =20 what became Appendix B in Guillaume's thesis (or maybe Guillaume already=20 had a draft at the time, I don't remember). Anyway, Guillaume gave a nice= =20 talk in 2017 with an overview of the attempts up to then and the problems= =20 we had encountered: https://guillaumebrunerie.github.io/pdf/cubicalexperiments.pdf This was before Cubical Agda was invented and there are some tricks in=20 Cubical Agda that might make a difference compared to cubicaltt (in=20 particular the "ghcomp" trick which I learned about from=20 Angiuli-Favonia-Harper and which eliminates empty systems in hcomps). Now= =20 that we have a computation that actually terminates I'm looking forward to= =20 seeing if any of these tricks actually were necessary or if it was "just" a= =20 matter of simplifying the definition of the number.=20 Best, Anders On Monday, May 23, 2022 at 11:00:17 PM UTC+2 Anders M=C3=B6rtberg wrote: > Thanks Nicolai! And yes, our =CE=B2' is a different definition of the ord= er of=20 > pi_4(S^3). In fact, the number =CE=B2 in the Summary file is not exactly = the=20 > same number as in Guillaume's Appendix B either for various reasons. For= =20 > instance, Guillaume only uses 1-HITs while we are quite liberal in using= =20 > higher HITs as they are not much harder to work with in Cubical Agda than= =20 > 1-HITs. Also Guillaume of course defines everything with path-induction= =20 > while we use cubical primitives and the maps in appendix B are quite=20 > unnecessarily complex from a cubical point of view (for instance, the=20 > equivalence S^3 =3D S^1 * S^1 can be written quite directly in Cubical Ag= da=20 > while in Book HoTT it's a bit more involved and Guillaume uses a chain of= =20 > equivalences to define it). > > One could of course define the number exactly like Guillaume does and try= =20 > to compute it, but I don't find that very interesting now that we have a= =20 > much simpler definition which is fast to compute. However, we have come u= p=20 > with various other interesting numbers that we can't get Cubical Agda to= =20 > compute, so there's definitely room to make cubical evaluation faster.=20 > Surprisingly enough though, one doesn't need to do this in order to get= =20 > Cubical Agda to compute the order of pi_4(S^3) :-) > > -- > Anders > > > On Mon, May 23, 2022 at 10:23 PM Nicolai Kraus =20 > wrote: > >> Congratulations! It's great that this number finally computes in practic= e=20 >> and not just in theory, after all these years. :-) >> And it's impressive how short the new proof is! But this still doesn't= =20 >> mean that Cubical Agda passes the test that Guillaume formulates in=20 >> Appendix B of his thesis, right? Because this test refers to the Bruneri= e=20 >> number =CE=B2 (in the Summary.agda file you linked), and not to =CE=B2'. >> In any case, that's a fantastic result! >> Best, >> Nicolai >> >> >> >> >> >> >> >> On Mon, May 23, 2022 at 8:30 PM Anders Mortberg = =20 >> wrote: >> >>> We're very happy to announce that we have finally managed to compute th= e=20 >>> Brunerie number using Cubical Agda... and the result is -2!=20 >>> >>> >>> https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S= 3/Summary.agda#L129 >>> >>> The computation was made possible by a new direct synthetic proof that= =20 >>> pi_4(S^3) =3D Z/2Z by Axel Ljungstr=C3=B6m. This new proof involves a s= eries of=20 >>> new Brunerie numbers (i.e. numbers n : Z such that pi_4(S^3) =3D Z/nZ) = and we=20 >>> got the one called =CE=B2' in the file above to reduce to -2 in just a = few=20 >>> seconds. With some work we then managed to prove that pi_4(S^3) =3D Z /= =CE=B2'=20 >>> Z, leading to a proof by normalization of the number as conjectured in= =20 >>> Brunerie's thesis. >>> >>> Axel's new proof is very direct and completely avoids chapters 4-6 in= =20 >>> Brunerie's thesis (so no cohomology theory!), but it relies on chapters= 1-3=20 >>> to define the number. It also does not rely on any special features of= =20 >>> cubical type theory and should be possible to formalize also in systems= =20 >>> based on Book HoTT. For a proof sketch as well as the formalization of = the=20 >>> new proof in just ~700 lines (not counting what is needed from chapters= =20 >>> 1-3) see:=20 >>> >>> >>> https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S= 3/DirectProof.agda >>> >>> So to summarize we now have both a new direct HoTT proof, not relying o= n=20 >>> cubical computations, as well as a cubical proof by computation. >>> >>> Univalent regards, >>> Anders and Axel >>> >>> PS: the minus sign is actually not very significant and we can get +2 b= y=20 >>> slightly modifying =CE=B2', but it's quite funny that we ended up getti= ng -2=20 >>> when we finally got a definition which terminates! >>> >>> --=20 >>> You received this message because you are subscribed to the Google=20 >>> Groups "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, send= =20 >>> an email to HomotopyTypeThe...@googlegroups.com. >>> To view this discussion on the web visit=20 >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sP= gLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com=20 >>> >>> . >>> >> --=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/36c1e828-af3a-49c2-840b-1fae9897eeban%40googlegroups.com= . ------=_Part_513_812432203.1653385595287 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I did some digging and found the first commit with an attempt to compu= te the number written by Guillaume Brunerie, Thierry Coquand and Simon Hube= r already in December 2014:

https://github.com= /simhu/cubical/commit/6e6278c6a626a9034789ab11cdd6bfb0bc8550be
This code is written for the predecessor of cubicaltt called "= cubical" and Thierry reminded me that it was based on the buggy regularity = evaluator which we eventually fixed in cubicaltt. I also think this cubical= code is what became Appendix B in Guillaume's thesis (or maybe Guillaume a= lready had a draft at the time, I don't remember). Anyway, Guillaume gave a= nice talk in 2017 with an overview of the attempts up to then and the prob= lems we had encountered:

https://guillaumebrun= erie.github.io/pdf/cubicalexperiments.pdf

This was= before Cubical Agda was invented and there are some tricks in Cubical Agda= that might make a difference compared to cubicaltt (in particular the "ghc= omp" trick which I learned about from Angiuli-Favonia-Harper and which elim= inates empty systems in hcomps). Now that we have a computation that actual= ly terminates I'm looking forward to seeing if any of these tricks actually= were necessary or if it was "just" a matter of simplifying the definition = of the number.

Best,
Anders

On = Monday, May 23, 2022 at 11:00:17 PM UTC+2 Anders M=C3=B6rtberg wrote:
Thanks Nicolai! And yes, our =CE=B2' is a different definition of the or= der of pi_4(S^3). In fact, the number =CE=B2 in the Summary file is not exa= ctly the same number as in Guillaume's Appendix B either for various reason= s. For instance, Guillaume only uses 1-HITs while we are quite liberal in u= sing higher HITs as they are not much harder to work with in Cubical Agda t= han 1-HITs. Also Guillaume of course defines everything with path-induction= while we use cubical primitives and the maps in appendix B are quite unnec= essarily complex from a cubical point of view (for instance, the equivalenc= e S^3 =3D S^1 * S^1 can be written quite directly in Cubical Agda while in = Book HoTT it's a bit more involved and Guillaume uses a chain of equivalenc= es to define it).

One could of course define t= he number exactly like Guillaume does and try to compute it, but I don't fi= nd that very interesting now that we have a much simpler definition which i= s fast to compute. However, we have come up with various other interesting= numbers that we can't get Cubical Agda to compute, so there's definitely r= oom to make cubical evaluation faster. Surprisingly enough though, one does= n't need to do this in order to get Cubical Agda to compute the order of pi= _4(S^3)   :-)

--
Anders


On Mon, May 23, 2022 at 10:23 PM Nicolai Kraus <nicola...@gmail.com> wrote:<= br>
Congratulations! It's great that this number finally computes in practice = and not just in theory, after all these years. :-)
And it's impressive = how short the new proof is! But this still doesn't mean that Cubical Agda p= asses the test that Guillaume formulates in Appendix B of his thesis, right= ? Because this test refers to the Brunerie number =CE=B2 (in the Summary.ag= da file you linked), and not to =CE=B2'.
In any case, that's a fa= ntastic result!
Best,
Nicolai






On Mon, May 23, 2022 at 8:30 PM Anders Mortberg <andersm...@gmail.com= > wrote:
We're very happy to announce that we have finally managed= to=20 compute the Brunerie number using Cubical Agda... and the result is -2!


The computation was made possible by a new direct synthetic proof that=20 pi_4(S^3) =3D Z/2Z by Axel Ljungstr=C3=B6m. This new proof involves a seri= es=20 of new Brunerie=20 numbers (i.e. numbers n : Z such that pi_4(S^3) =3D Z/nZ) and we got the= =20 one called =CE=B2' in the file above to reduce to -2 in just a= few seconds. With some work we then managed to prove that pi_4(S^3) =3D = Z / =CE=B2' Z, leading to a proof by normalization of the numb= er as conjectured in Brunerie's thesis.

Axel's new proof is very direct and completely=20 avoids chapters 4-6 in Brunerie's thesis (so no cohomology theory!), but it relies on chapters 1-3 to define the number. It also does not rely=20 on any special features of cubical type theory=20 and should be possible to formalize also in systems based on Book HoTT.=20 For a proof sketch as well as the formalization of the new proof in just=20 ~700 lines (not counting what is needed from chapters 1-3) see:
<= div>
=
So to summarize we now have both a new direct HoTT proof, not relying on=20 cubical computations, as well as a cubical proof by computation.
<= div>
Univalent regards,
A= nders and Axel

PS: the minus sign is a= ctually not very significant and we can get +2 by slightly modifying <= span>=CE=B2', but it's quite funny that we ended up getting -2 when = we finally got a definition which terminates!

--
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 HomotopyTypeTh= e...@googlegroups.com.
To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUw= Gu179XXw%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.c= om/d/msgid/HomotopyTypeTheory/36c1e828-af3a-49c2-840b-1fae9897eeban%40googl= egroups.com.
------=_Part_513_812432203.1653385595287-- ------=_Part_512_343870225.1653385595287--