Thanks Nicolai! And yes, our =CE=B2' is a differe=
nt definition of the order of pi_4(S^3). In fact, the number =CE=B2 in the =
Summary file is not exactly the same number as in Guillaume's Appendix =
B either for various reasons. For instance, Guillaume only uses 1-HITs whil=
e we are quite liberal in using higher HITs as they are not much harder to =
work with in Cubical Agda than 1-HITs. Also Guillaume of course defines eve=
rything with path-induction while we use cubical primitives and the maps in=
appendix B are quite unnecessarily complex from a cubical point of view (f=
or instance, the equivalence S^3 =3D S^1 * S^1 can be written quite directl=
y in Cubical Agda while in Book HoTT it's a bit more involved and Guill=
aume uses a chain of equivalences to define it).

--

Anders

On Mon, May 23, 2022 at 10:23 PM Nicolai Kraus <nicolai.kraus@gmail.com> wrote:

Congrat= ulations! 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 Ag= da passes the test that Guillaume formulates in Appendix B of his thesis, r= ight? Because this test refers to the Brunerie number =CE=B2 (in the Summar= y.agda file you linked), and not to =CE=B2'.In any case, tha= t's a fantastic result!Best,Nicolai

<= /div><= br>On Mon, May 23, 2022 at 8:30 PM Anders Mor= tberg <and= ersmortberg@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 ju= st 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 number as conjectured in Brunerie's thesis.Axel&= #39;s new proof is very direct and completely=20 avoids chapters 4-6 in Brunerie's thesis (so no cohomology theory!), bu= t 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 AxelPS: the minus sign is a= ctually not very significant and we can get=C2=A0+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 &= 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/CAMWCppkF= 0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmqhhiHkpgHPqoSMvdyQUsT%3= DhFevG-LJ8FPhtrLpNtdbQ%40mail.gmail.com.

--00000000000080397d05dfb4201f--