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 17694 invoked from network); 23 May 2022 21:00:18 -0000 Received: from mail-ot1-x340.google.com (2607:f8b0:4864:20::340) by inbox.vuxu.org with ESMTPUTF8; 23 May 2022 21:00:18 -0000 Received: by mail-ot1-x340.google.com with SMTP id j14-20020a9d190e000000b0060b0b788bf7sf2145534ota.18 for ; Mon, 23 May 2022 14:00:18 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1653339618; cv=pass; d=google.com; s=arc-20160816; b=t+4HXKUUze3M/4CfqlOwbQfTqqQXIVxKoQJYBfcz6FPZ4f7p2GIbk40jtVn+2X6oks 2CdEbsOCMs3pLKCRSobSzH0Y8zFuRJgMtSQP7maSvbI/Y891CwmuBIc8bCpkdF5fdjTV Ky5FhnRj4CF5+J2ps74vDmddK7C2nHmO2B8gjQ1AHm/CwyLBnkpPtaQUmgmXiM1MdbsD te7f3HrNDMOA/vd5SQ5FarJbp5VxEqtMvBjujdddF/aXBrVvOA6yFJZtwRf0E/CqeLYu GiFPC0QTxNgrOlzVLlVyNgJvfxrDQ/H+tPUPnZlbOj6Hzkml3TvaVtafQNfJrOZTdrUB aOFg== 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=pHxqdu1mVltxJCfWkrfMvTM13fCnEpNCvQ/+AxfwXwA=; b=DEpk5jbnbY0XYr7DgQFvcYRAdFTOWmRzB6mqkNK8FnSL8AdUCZw0MLvGTuhS8zmYwh oTV/H20CICDq2VJlHVuf8u5pJbRnTFEGSeyw5n7HyUsp1C3fW3hF4QUVw4TAjK3Gh4eD wOOrvy/LP2JS1Ae+PCS9wQL4QsclKp/ewMJFr2LjrYPsWIOO/583DMUs5/FtY1ltf3VL W8Sqnq2CPeKITruKjlYaei4H/02bylKZN8grrl5YJluy6swWJf0ldYBOM4eio0ZZNyCs qaAPmmdBBPeQr9yL7IJx2Ua18ckwDOvS0cP9lZ7cHTx2C8Nmq/es4VG5SLlFkhFXR/Nk gnww== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=PUZwpP1N; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2f 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=pHxqdu1mVltxJCfWkrfMvTM13fCnEpNCvQ/+AxfwXwA=; b=LNnnhgMGd+lhuFtX1Xvb9xv2bSI07YdTU5c9gThwHeUPto+5gli/4+kOb9M+sk3ecz eusU11297Q0OUrWT6rmkSISUaM/zovwxehv1arsRuZb499c9/olhfWz9EbR9dZ+0lk70 +2tCGsv8a+d5xaU9Lvf8YK4B/h8j5EAQBwSFsiZ5NtLaO5Yvqz71hgHT11ojf1pYqOXN 4fAYzfOtZx4P6UvZfUPLRjyDrpEFvp6alExKMylWnUuLVbzv3v744FsQThfUfTaTXdfd ejEEGnRv/e1xz2GiWD6wT44hH+VYPqDVlmNcRlNP8XC5cNR30pmVqzKp/1DHfUKaU20a cBHA== 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=pHxqdu1mVltxJCfWkrfMvTM13fCnEpNCvQ/+AxfwXwA=; b=bvw949j1iTfFY1uQ1la2iEHTcm5REhXh1lZjzm9rxaemtjnRXJ5Vv5/ASIEs/jLDDh MCjFyY0n1Wcdz/IJUz3G/QDdVS1OCt7N+u370p4Wrq/b/cxxJErctg9G2zHzO/2DQ775 k81/jqE7rbsOP3FHzN/dUh2MphlneG3XzcVDTuOFn0U6vYRjxouPCtLM0awvO98vxuKa kzqaOmqOa9K+MJmkDPFR6adcLs4iJaiBm5zBWib3mw77VbsAhJz7/AGQ0mOJjEbDYmNn UYClgu+w78XwWIs5h7Dyk6V+GK7nj5Utkf9QR00AHZHFTDxoC8il2f6AbGe6EJdPrxF/ PMag== 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=pHxqdu1mVltxJCfWkrfMvTM13fCnEpNCvQ/+AxfwXwA=; b=Lh5WWxvtw0mES208kRxv+yQafiP3Ay2rbZ2AnOUuM/SrXJeY4BH9z9S8gvd+1sT2I3 wsN3eJ/Gw0olJHG/hpg7CmPkwNBKQG2Dfqg6t3mJ/ipmZHFCPhF0VoVM4ZnBEEhcAVke AVi9YJ3UnetL6YtZ4QUQt93GnYaTVee643VdhMpxl3kU5lSlpOA1IAvWs4jd+K2A1Ids psmzlCK5vojUSuMcWLpV8OVFjUNZgOOIDdWa9bqC/xFy15I6ZHkkUPUIXSaUy/obE2+9 iFtddPBG3a0vQkzcDNiw7oPY5mbwt+q5UWlpPui9lHwdglNo0qfr6az2K4pvObXShigx 34PA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532dk5zkQWzCQqRTGPtiThjeHzwgliMs43n5iZTkmpw/2rlay0Du c006hWlfG6xXfSiiZqz9oTo= X-Google-Smtp-Source: ABdhPJwjuyBb1tTJxrTCo/eEX1Yi8pR3bdhrXd6x90fb3joWZAYm/JO/pdiniA3QUIzOVFjBerirMw== X-Received: by 2002:a9d:5e8c:0:b0:605:f4ca:bc2d with SMTP id f12-20020a9d5e8c000000b00605f4cabc2dmr9489250otl.86.1653339617782; Mon, 23 May 2022 14:00:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6870:13cd:b0:de:c1c1:ac0e with SMTP id 13-20020a05687013cd00b000dec1c1ac0els5638401oat.8.gmail; Mon, 23 May 2022 14:00:16 -0700 (PDT) X-Received: by 2002:a05:6870:b60e:b0:e9:35aa:3cb8 with SMTP id cm14-20020a056870b60e00b000e935aa3cb8mr497832oab.249.1653339616468; Mon, 23 May 2022 14:00:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1653339616; cv=none; d=google.com; s=arc-20160816; b=k4ZtEvM+TesLHr0oWzXj56QFtJ5r0HNXIrOL2a7Onaaa25pNGzlm4ZOroBKYVf5lo0 IXLopEw/1iirQIph1H3VZU9anAtAeo+wTYipiC2T5AK0bm7KYnCC0gbb9lzlQswSRp21 a6D1JjJD/K3Vm4yvV+jh2qwKRBi8Ge56bMuPcWnFNTbdg2cOmBycULa9X24+RhH2mVCo ezwDWxpXGAZnARJaFKyHHrMZbDOTg/oW+H5fSeKLAR1dIcH9xP++NyR20aCwnOZQxNGa 47IxNmHQIaNQ31twvRaI/GeL49FwOnLHV+sdbjksSX2EiICn86GW3RTR0hrWIlFUTynN 3dpw== 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=SLrE7s+cFjP8K+kP+uUw3Y+wcwyCqgApz7iKuL7+sLQ=; b=Sfx5+lE4vMF7oP7+R93h0KBnFHNxev8Cuo3P5ds0GqI30u9szUWJCIJfurpjrIGjG4 rjHsVeDs2N8/MQHrQAob0MpyWSOMdLnOch14dRnU2DO1Njp3PPTXVOWtawh5scSn5CDV PAY3SI8Xl5tgf16zvbF+2GIcDOXaM6ap7wKBgJuRkDEASYn28I2c51hv6vEANp1J/2qh DbYBkWrcOUUr5HHW8xWyxpoaSwNfs9W8va/Rz/d+1CuxjdHppBe68EJPionezakfTenD qvTdtlmRRRzIPRCI6KJ59emW5v0qX8/Hj/tSH+XmqsIjDtMyJ5u8EY44CQXbC17gj85P LKkQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=PUZwpP1N; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2f as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vs1-xe2f.google.com (mail-vs1-xe2f.google.com. [2607:f8b0:4864:20::e2f]) by gmr-mx.google.com with ESMTPS id w24-20020a4a9d18000000b0035f627c29easi1328612ooj.1.2022.05.23.14.00.16 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 23 May 2022 14:00:16 -0700 (PDT) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2f as permitted sender) client-ip=2607:f8b0:4864:20::e2f; Received: by mail-vs1-xe2f.google.com with SMTP id c62so16293549vsc.10 for ; Mon, 23 May 2022 14:00:16 -0700 (PDT) X-Received: by 2002:a67:8c4:0:b0:32d:51e4:c6fe with SMTP id 187-20020a6708c4000000b0032d51e4c6femr10306171vsi.66.1653339615933; Mon, 23 May 2022 14:00:15 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Anders Mortberg Date: Mon, 23 May 2022 22:59:39 +0200 Message-ID: Subject: Re: [HoTT] The Brunerie number is -2 To: Nicolai Kraus Cc: Homotopy Type Theory , =?UTF-8?Q?Axel_Ljungstr=C3=B6m?= Content-Type: multipart/alternative; boundary="00000000000080397d05dfb4201f" 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=PUZwpP1N; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2f 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: , --00000000000080397d05dfb4201f Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks Nicolai! And yes, our =CE=B2' is a different definition of the order= of pi_4(S^3). In fact, the number =CE=B2 in the Summary file is not exactly th= e same number as in Guillaume's Appendix B either for various reasons. For instance, Guillaume only uses 1-HITs while 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 everything with path-induction while we use cubical primitives and the maps in appendix B are quite unnecessarily complex from a cubical point of view (for instance, the equivalence 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 equivalences to define it). One could of course define the number exactly like Guillaume does and try to compute it, but I don't find that very interesting now that we have a much simpler definition which is 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 room to make cubical evaluation faster. Surprisingly enough though, one doesn'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 wrote: > 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 passes 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.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 > wrote: > >> We're very happy to announce that we have finally managed to compute the >> Brunerie number using Cubical Agda... and the result is -2! >> >> >> https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3= /Summary.agda#L129 >> >> The computation was made possible by a new direct synthetic proof that >> pi_4(S^3) =3D Z/2Z by Axel Ljungstr=C3=B6m. This new proof involves a se= ries of >> new Brunerie numbers (i.e. numbers n : Z such that pi_4(S^3) =3D Z/nZ) a= nd we >> got the one called =CE=B2' in the file above to reduce to -2 in just a f= ew >> 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's new proof is very direct and completely 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 on any special features of >> cubical type theory and should be possible to formalize also in systems >> based on Book HoTT. For a proof sketch as well as the formalization of t= he >> new proof in just ~700 lines (not counting what is needed from chapters >> 1-3) see: >> >> >> https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3= /DirectProof.agda >> >> So to summarize we now have both a new direct HoTT proof, not relying on >> 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 by >> slightly modifying =CE=B2', but it's quite funny that we ended up gettin= g -2 >> when we finally got a definition which terminates! >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPg= LaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%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/CAMWCppmqhhiHkpgHPqoSMvdyQUsT%3DhFevG-LJ8FPhtrLpNtdbQ%40= mail.gmail.com. --00000000000080397d05dfb4201f Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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).

One could of course define the number exactly like Guillaume does and tr= y to compute it, but I don't find that very interesting now that we hav= e a much simpler definition which is fast to compute. However, we have come= up with various other interesting numbers that we can't get Cubical A= gda to compute, so there's definitely room to make cubical evaluation f= aster. Surprisingly enough though, one doesn't need to do this in order= to get Cubical Agda to compute the order of pi_4(S^3) =C2=A0 :-)
=

--
Anders
<= br>

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 Axel

PS: 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--