Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed
* [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
@ 2022-02-08 20:19 Anders Mortberg
2022-02-08 23:24  Joyal, André
From: Anders Mortberg @ 2022-02-08 20:19 UTC (permalink / raw)
To: Homotopy Type Theory

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

We are happy to announce that we have finished a formalization of
π₄(S³)≅ℤ/2ℤ  in Cubical Agda. Most of the code has been written by my PhD
student Axel Ljungström 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 homotopy
groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey,
Z-cohomology (with graded commutative ring structure), Gysin sequence, the
Hopf invariant, Whitehead product... Most of this was written by Axel under
my supervision, but some results are due to other contributors to the
library, in particular Loïc Pujet (3x3 lemma for pushouts, total space 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 major
ways:

1. We found a direct encode-decode proof of a special case of corollary
3.2.3 and proposition 3.2.11 which is needed for π₄(S³). 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 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, Cubical
Agda makes it possible to discharge several small steps in the proof
involving univalence and HITs purely by computation. This even reduces some
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 this
has to do with π₄(S³). 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 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 to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%40mail.gmail.com.

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

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
2022-02-08 20:19 [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed Anders Mortberg
@ 2022-02-08 23:24  Joyal, André
2022-02-09  3:09    Steve Awodey
From: Joyal, André @ 2022-02-08 23:24 UTC (permalink / raw)
To: Anders Mortberg, Homotopy Type Theory

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

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 homotopy theory!
It is an amazing piece of work.
Thanks to all, starting with Guillaume.

Best wishes,
Andre
________________________________
Envoyé : 8 février 2022 15:19
À : Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Objet : [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed

We are happy to announce that we have finished a formalization of  π₄(S³)≅ℤ/2ℤ  in Cubical Agda. Most of the code has been written by my PhD student Axel Ljungström 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 homotopy groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey, Z-cohomology (with graded commutative ring structure), Gysin sequence, the Hopf invariant, Whitehead product... Most of this was written by Axel under my supervision, but some results are due to other contributors to the library, in particular Loïc Pujet (3x3 lemma for pushouts, total space 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 major ways:

1. We found a direct encode-decode proof of a special case of corollary 3.2.3 and proposition 3.2.11 which is needed for π₄(S³). 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 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, Cubical Agda makes it possible to discharge several small steps in the proof involving univalence and HITs purely by computation. This even reduces some 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 this has to do with π₄(S³). 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 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 to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.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/QB1PR01MB29481886234F6ECEB3006C31FD2D9%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM.

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

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
2022-02-08 23:24  Joyal, André
@ 2022-02-09  3:09    Steve Awodey
2022-02-09  4:16      Noah Snyder
From: Steve Awodey @ 2022-02-09  3:09 UTC (permalink / raw)
To: "Joyal, André", Anders Mortberg; +Cc: Homotopy Type Theory

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

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é <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 homotopy theory!
> It is an amazing piece of work.
> Thanks to all, starting with Guillaume.
>
> Best wishes,
> Andre
> Envoyé : 8 février 2022 15:19
> Objet : [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
>
> We are happy to announce that we have finished a formalization of  π₄(S³)≅ℤ/2ℤ  in Cubical Agda. Most of the code has been written by my PhD student Axel Ljungström 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 <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, the Hopf invariant, Whitehead product... Most of this was written by Axel under my supervision, but some results are due to other contributors to the library, in particular Loïc Pujet (3x3 lemma for pushouts, total space 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 major ways:
>
> 1. We found a direct encode-decode proof of a special case of corollary 3.2.3 and proposition 3.2.11 which is needed for π₄(S³). 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/ <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, Cubical Agda makes it possible to discharge several small steps in the proof involving univalence and HITs purely by computation. This even reduces some 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 this has to do with π₄(S³). 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 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 <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.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 <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.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-B4F2-A105376DE6EB%40gmail.com.

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

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
2022-02-09  3:09    Steve Awodey
@ 2022-02-09  4:16      Noah Snyder
2022-02-09  4:44        'Urs Schreiber' via Homotopy Type Theory
From: Noah Snyder @ 2022-02-09  4:16 UTC (permalink / raw)
To: Steve Awodey; +Cc: Joyal, André, Anders Mortberg, Homotopy Type Theory

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

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 <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é <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 homotopy
> theory!
> It is an amazing piece of work.
> Thanks to all, starting with Guillaume.
>
> Best wishes,
> Andre
> ------------------------------
> homotopytypetheory@googlegroups.com> de la part de Anders Mortberg <
> andersmortberg@gmail.com>
> *Envoyé :* 8 février 2022 15:19
> *À :* Homotopy Type Theory <homotopytypetheory@googlegroups.com>
> *Objet :* [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
>
> We are happy to announce that we have finished a formalization of
> π₄(S³)≅ℤ/2ℤ  in Cubical Agda. Most of the code has been written by my PhD
> student Axel Ljungström 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 homotopy
> groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey,
> Z-cohomology (with graded commutative ring structure), Gysin sequence, the
> Hopf invariant, Whitehead product... Most of this was written by Axel under
> my supervision, but some results are due to other contributors to the
> library, in particular Loïc Pujet (3x3 lemma for pushouts, total space 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 major
> ways:
>
> 1. We found a direct encode-decode proof of a special case of corollary
> 3.2.3 and proposition 3.2.11 which is needed for π₄(S³). 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 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, Cubical
> Agda makes it possible to discharge several small steps in the proof
> involving univalence and HITs purely by computation. This even reduces some
> 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 this
> has to do with π₄(S³). 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 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
> To view this discussion on the web visit
> .
>
> --
> 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
> To view this discussion on the web visit
> .
>
>
> --
> 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
> To view this discussion on the web visit
> .
>

--
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/CAO0tDg5V2dMm71XbqR4dt%2BK2jCZpE-myseR7385H%3DZGbpoWytQ%40mail.gmail.com.

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

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
2022-02-09  4:16      Noah Snyder
@ 2022-02-09  4:44        'Urs Schreiber' via Homotopy Type Theory
2022-02-11 11:29          Anders Mortberg
From: 'Urs Schreiber' via Homotopy Type Theory @ 2022-02-09  4:44 UTC (permalink / raw)
To: Homotopy Type Theory; +Cc: Steve Awodey, Joyal, André, Anders Mortberg

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

(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#references

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 <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 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 <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é <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 homotopy 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é : 8 février 2022 15:19
>> À : Homotopy Type Theory <homotopytypetheory@googlegroups.com>
>> Objet : [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
>>
>> We are happy to announce that we have finished a formalization of  π₄(S³)≅ℤ/2ℤ  in Cubical Agda. Most of the code has been written by my PhD student Axel Ljungström 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 homotopy groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey, Z-cohomology (with graded commutative ring structure), Gysin sequence, the Hopf invariant, Whitehead product... Most of this was written by Axel under my supervision, but some results are due to other contributors to the library, in particular Loïc Pujet (3x3 lemma for pushouts, total space 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 major ways:
>>
>> 1. We found a direct encode-decode proof of a special case of corollary 3.2.3 and proposition 3.2.11 which is needed for π₄(S³). 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 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, Cubical Agda makes it possible to discharge several small steps in the proof involving univalence and HITs purely by computation. This even reduces some 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 this has to do with π₄(S³). 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 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_2USKH9dAigFGx0GBrcG3XQQaqZmkr-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/QB1PR01MB29481886234F6ECEB3006C31FD2D9%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-B4F2-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/CAO0tDg5V2dMm71XbqR4dt%2BK2jCZpE-myseR7385H%3DZGbpoWytQ%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/CA%2BKbugc-fn9wupcbxTekp4z8aJn3B-OOWc1-1Gpp%3DGYk9LrmbQ%40mail.gmail.com.

[-- Attachment #2: SurLes.PNG --]
[-- Type: image/png, Size: 60479 bytes --]

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
2022-02-09  4:44        'Urs Schreiber' via Homotopy Type Theory
@ 2022-02-11 11:29          Anders Mortberg
0 siblings, 0 replies; 6+ messages in thread
From: Anders Mortberg @ 2022-02-11 11:29 UTC (permalink / raw)
To: Homotopy Type Theory; +Cc: Steve Awodey, Joyal, André, Urs Schreiber

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

Thanks a lot to André, Steve and everyone else that wrote to us privately
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é that this shows that Cubical Agda is a great tool for
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 π₄(S³)≅ℤ/2ℤ 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 <urs.schreiber@googlemail.com>
wrote:

> (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#references
>
> 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 <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
> 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 <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é <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 homotopy
> 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é : 8 février 2022 15:19
> >> À : Homotopy Type Theory <homotopytypetheory@googlegroups.com>
> >> Objet : [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed
> >>
> >> We are happy to announce that we have finished a formalization of
> π₄(S³)≅ℤ/2ℤ  in Cubical Agda. Most of the code has been written by my PhD
> student Axel Ljungström 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 homotopy
> groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey,
> Z-cohomology (with graded commutative ring structure), Gysin sequence, the
> Hopf invariant, Whitehead product... Most of this was written by Axel under
> my supervision, but some results are due to other contributors to the
> library, in particular Loïc Pujet (3x3 lemma for pushouts, total space 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 major
> ways:
> >>
> >> 1. We found a direct encode-decode proof of a special case of corollary
> 3.2.3 and proposition 3.2.11 which is needed for π₄(S³). 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 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, Cubical
> Agda makes it possible to discharge several small steps in the proof
> involving univalence and HITs purely by computation. This even reduces some
> 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 this
> has to do with π₄(S³). 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 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
> >> To view this discussion on the web visit
> .
> >>
> >> --
> >> 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
> >> To view this discussion on the web visit
> .
> >>
> >>
> >> --
> >> 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
> >> To view this discussion on the web visit
> .
> >
> > --
> > 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
> > To view this discussion on the web visit
> .
>

--
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/CAMWCpp%3Da8uKYsNFS%3D0wzYNyOT411zSpEzYD2V1FRe4KuU%2Bgjyw%40mail.gmail.com.

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

^ permalink raw reply	[flat|nested] 6+ messages in thread

end of thread, other threads:[~2022-02-11 11:30 UTC | newest]

2022-02-09  3:09    Steve Awodey
2022-02-09  4:44        'Urs Schreiber' via Homotopy Type Theory

This is a public inbox, see mirroring instructions
as well as URLs for NNTP newsgroup(s).`