Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Anders Mortberg <andersmortberg@gmail.com>
To: Nicolai Kraus <nicolai.kraus@gmail.com>
Cc: "Homotopy Type Theory" <homotopytypetheory@googlegroups.com>,
	"Axel Ljungström" <axel.ljungstrom@math.su.se>
Subject: Re: [HoTT] The Brunerie number is -2
Date: Mon, 23 May 2022 22:59:39 +0200	[thread overview]
Message-ID: <CAMWCppmqhhiHkpgHPqoSMvdyQUsT=hFevG-LJ8FPhtrLpNtdbQ@mail.gmail.com> (raw)
In-Reply-To: <CA+AZBBohg=XFpJTDiVMaUaNU9O3uA_Q8uqSTGgcJmZD4-oKvUA@mail.gmail.com>

[-- Attachment #1: Type: text/plain, Size: 4712 bytes --]

Thanks Nicolai! And yes, our β' is a different definition of the order of
pi_4(S^3). In fact, the number β 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 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 = 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)   :-)


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

> 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 β (in the Summary.agda file you linked), and not to β'.
> In any case, that's a fantastic result!
> Best,
> Nicolai
> On Mon, May 23, 2022 at 8:30 PM Anders Mortberg <andersmortberg@gmail.com>
> 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) = Z/2Z by Axel Ljungström. This new proof involves a series of
>> new Brunerie numbers (i.e. numbers n : Z such that pi_4(S^3) = Z/nZ) and we
>> got the one called β' 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) = Z / β' 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 the
>> 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 β', 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
>> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com
>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .

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/CAMWCppmqhhiHkpgHPqoSMvdyQUsT%3DhFevG-LJ8FPhtrLpNtdbQ%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 6510 bytes --]

  reply	other threads:[~2022-05-23 21:00 UTC|newest]

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-05-23 19:30 Anders Mortberg
2022-05-23 19:38 ` Steve Awodey
2022-05-23 20:22 ` Nicolai Kraus
2022-05-23 20:59   ` Anders Mortberg [this message]
2022-05-24  9:46     ` Anders Mörtberg
2022-05-24  9:49       ` Anders Mörtberg

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAMWCppmqhhiHkpgHPqoSMvdyQUsT=hFevG-LJ8FPhtrLpNtdbQ@mail.gmail.com' \
    --to=andersmortberg@gmail.com \
    --cc=axel.ljungstrom@math.su.se \
    --cc=homotopytypetheory@googlegroups.com \
    --cc=nicolai.kraus@gmail.com \
    --subject='Re: [HoTT] The Brunerie number is -2' \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).