Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed
* [HoTT] Syllepsis in HoTT
@ 2021-03-05 18:27 Kristina Sojakova
2021-03-05 18:40  Jamie Vicary
2021-03-07 18:00  Noah Snyder
0 siblings, 2 replies; 19+ messages in thread
From: Kristina Sojakova @ 2021-03-05 18:27 UTC (permalink / raw)
To: homotopytypetheory

Dear all,

Ali told me that apparently the following problem could be of interest
to some people (https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s):

Given two higher paths p, q : 1_x = 1_x, Eckmann-Hilton gives us a path
EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) = 1_{p@q=q_p}.

I just established the above in HoTT and am thinking of formalizing it,
unless someone already did it.

Thanks,

Kristina

--
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/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com.

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-05 18:27 [HoTT] Syllepsis in HoTT Kristina Sojakova
@ 2021-03-05 18:40  Jamie Vicary
2021-03-05 19:18    Noah Snyder
2021-03-07 18:00  Noah Snyder
1 sibling, 1 reply; 19+ messages in thread
From: Jamie Vicary @ 2021-03-05 18:40 UTC (permalink / raw)
To: Kristina Sojakova; +Cc: Homotopy Type Theory

Hi Kristina, that's great. I don't know that anyone's done this before.

> Given two higher paths p, q : 1_x = 1_x

I guess you mean p,q:1_(1_x) = 1_(1_x) ?

Best wishes,
Jamie

--
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/CANr23v3E%2BkaPKgL-So_s_h95KUwSM5i1vPSqzQyEmKa%3D_D46iQ%40mail.gmail.com.

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-05 18:40  Jamie Vicary
@ 2021-03-05 19:18    Noah Snyder
0 siblings, 0 replies; 19+ messages in thread
From: Noah Snyder @ 2021-03-05 19:18 UTC (permalink / raw)
To: Jamie Vicary; +Cc: Kristina Sojakova, Homotopy Type Theory

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

It'd be great to see this done!  I've been wanting to see this for a while,
but haven't gotten anyone to do it.

One remark on that part of the video: the syllepsis gives the proof that
the "Brunerie number" is 1 or 2, but it doesn't immediately let you exclude
the possibility that it's 1.  I think my student Nachiket Karnick and I do
understand how to show that the number is 2 (with a much more direct
calculation than what's in the second half of Brunerie's thesis, but still
using the James construction).  I have an outline of an even more direct
proof, but the syllepsis is one of the calculations required to make this
more direct approach work.  Which is all to say that I'm very interested in
seeing this result, especially if it meant that related calculations of
similar difficulty could be done thereby giving much more direct
calculations of the small homotopy groups of spheres.

Best,

Noah

On Fri, Mar 5, 2021 at 1:40 PM Jamie Vicary <jamievicary@gmail.com> wrote:

> Hi Kristina, that's great. I don't know that anyone's done this before.
>
> > Given two higher paths p, q : 1_x = 1_x
>
> I guess you mean p,q:1_(1_x) = 1_(1_x) ?
>
> Best wishes,
> Jamie
>
> --
> 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
> .
>

--
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/CAO0tDg4oCaZ--OuOVDynT5sXK5jQh1%2BOTM2FNzpx-QLEUg73Ng%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-05 18:27 [HoTT] Syllepsis in HoTT Kristina Sojakova
2021-03-05 18:40  Jamie Vicary
@ 2021-03-07 18:00  Noah Snyder
2021-03-08  8:44    Egbert Rijke
1 sibling, 1 reply; 19+ messages in thread
From: Noah Snyder @ 2021-03-07 18:00 UTC (permalink / raw)
To: Kristina Sojakova; +Cc: Homotopy Type Theory

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

On the subject of formalization and the syllepsis, has it ever been
formalized that Eckman-Hilton gives the generator of \pi_3(S^2)?  That is,
we can build a 3-loop for S^2 by refl_refl_base --> surf \circ surf^{-1}
--EH--> surf^{-1} \circ surf -->  refl_refl_base, and we want to show that
under the equivalence \pi_3(S^2) --> Z constructed in the book that this
3-loop maps to \pm 1 (which sign you end up getting will depend on
conventions).

There's another explicit way to construct a generating a 3-loop on S^2,
namely refl_refl_base --> surf \circ surf \circ \surf^-1 \circ surf^-1 --EH
whiskered refl refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -->
refl_refl_base, where I've suppressed a lot of associators and other
details.  One could also ask whether this generator is the same as the one
in my first paragraph.  This should be of comparable difficulty to the
syllepsis (perhaps easier), but is another good example of something that's
"easy" with string diagrams but a lot of work to translate into formalized
HoTT.

Best,

Noah

On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova <
sojakova.kristina@gmail.com> wrote:

> Dear all,
>
> Ali told me that apparently the following problem could be of interest
> to some people (https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s):
>
> Given two higher paths p, q : 1_x = 1_x, Eckmann-Hilton gives us a path
> EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) = 1_{p@q=q_p}.
>
> I just established the above in HoTT and am thinking of formalizing it,
> unless someone already did it.
>
> Thanks,
>
> Kristina
>
> --
> 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
> .
>

--
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/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-07 18:00  Noah Snyder
@ 2021-03-08  8:44    Egbert Rijke
2021-03-08  8:53      Egbert Rijke
0 siblings, 1 reply; 19+ messages in thread
From: Egbert Rijke @ 2021-03-08  8:44 UTC (permalink / raw)
To: Noah Snyder; +Cc: Kristina Sojakova, Homotopy Type Theory

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

Hi Kristina,

I've been on it already, because I was in that talk, and while my
formalization isn't yet finished, I do have all the pseudocode already.

Best wishes,
Egbert

On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder <nsnyder@gmail.com> wrote:

> On the subject of formalization and the syllepsis, has it ever been
> formalized that Eckman-Hilton gives the generator of \pi_3(S^2)?  That is,
> we can build a 3-loop for S^2 by refl_refl_base --> surf \circ surf^{-1}
> --EH--> surf^{-1} \circ surf -->  refl_refl_base, and we want to show that
> under the equivalence \pi_3(S^2) --> Z constructed in the book that this
> 3-loop maps to \pm 1 (which sign you end up getting will depend on
> conventions).
>
> There's another explicit way to construct a generating a 3-loop on S^2,
> namely refl_refl_base --> surf \circ surf \circ \surf^-1 \circ surf^-1 --EH
> whiskered refl refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -->
> refl_refl_base, where I've suppressed a lot of associators and other
> details.  One could also ask whether this generator is the same as the one
> in my first paragraph.  This should be of comparable difficulty to the
> syllepsis (perhaps easier), but is another good example of something that's
> "easy" with string diagrams but a lot of work to translate into formalized
> HoTT.
>
> Best,
>
> Noah
>
> On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova <
> sojakova.kristina@gmail.com> wrote:
>
>> Dear all,
>>
>> Ali told me that apparently the following problem could be of interest
>> to some people (https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s):
>>
>> Given two higher paths p, q : 1_x = 1_x, Eckmann-Hilton gives us a path
>> EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) = 1_{p@q=q_p}.
>>
>> I just established the above in HoTT and am thinking of formalizing it,
>> unless someone already did it.
>>
>> Thanks,
>>
>> Kristina
>>
>> --
>> 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
>> .
>>
> --
> 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
> .
>

--
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/CAGqv1OBJ7iSeng_MY3f%3DY1k3EWgm9Q6VpyU5-EH-j68H0BYC9w%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08  8:44    Egbert Rijke
@ 2021-03-08  8:53      Egbert Rijke
2021-03-08 13:38        Noah Snyder
0 siblings, 1 reply; 19+ messages in thread
From: Egbert Rijke @ 2021-03-08  8:53 UTC (permalink / raw)
To: Noah Snyder; +Cc: Kristina Sojakova, Homotopy Type Theory

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

Dear Noah,

I don't think that your claim that syllepsis gives a proof that Brunerie's
number is 1 or 2 is accurate. Syllepsis gives you that a certain element of
pi_4(S^3) has order 1 or 2, but it is an entirely different matter to show
that this element generates the group. There could be many elements of
order 2.

Best wishes,
Egbert

On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke <e.m.rijke@gmail.com> wrote:

> Hi Kristina,
>
> I've been on it already, because I was in that talk, and while my
> formalization isn't yet finished, I do have all the pseudocode already.
>
> Best wishes,
> Egbert
>
> On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder <nsnyder@gmail.com> wrote:
>
>> On the subject of formalization and the syllepsis, has it ever been
>> formalized that Eckman-Hilton gives the generator of \pi_3(S^2)?  That is,
>> we can build a 3-loop for S^2 by refl_refl_base --> surf \circ surf^{-1}
>> --EH--> surf^{-1} \circ surf -->  refl_refl_base, and we want to show that
>> under the equivalence \pi_3(S^2) --> Z constructed in the book that this
>> 3-loop maps to \pm 1 (which sign you end up getting will depend on
>> conventions).
>>
>> There's another explicit way to construct a generating a 3-loop on S^2,
>> namely refl_refl_base --> surf \circ surf \circ \surf^-1 \circ surf^-1 --EH
>> whiskered refl refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -->
>> refl_refl_base, where I've suppressed a lot of associators and other
>> details.  One could also ask whether this generator is the same as the one
>> in my first paragraph.  This should be of comparable difficulty to the
>> syllepsis (perhaps easier), but is another good example of something that's
>> "easy" with string diagrams but a lot of work to translate into formalized
>> HoTT.
>>
>> Best,
>>
>> Noah
>>
>> On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova <
>> sojakova.kristina@gmail.com> wrote:
>>
>>> Dear all,
>>>
>>> Ali told me that apparently the following problem could be of interest
>>> to some people (https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s):
>>>
>>> Given two higher paths p, q : 1_x = 1_x, Eckmann-Hilton gives us a path
>>> EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) = 1_{p@q=q_p}.
>>>
>>> I just established the above in HoTT and am thinking of formalizing it,
>>> unless someone already did it.
>>>
>>> Thanks,
>>>
>>> Kristina
>>>
>>> --
>>> 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
>>> .
>>>
>> --
>> 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
>> .
>>
>

--
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/CAGqv1ODR04M-4HB0-HvUsn%3Dmpe4PTR5osJUvFR6021xnCsd1sQ%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08  8:53      Egbert Rijke
@ 2021-03-08 13:38        Noah Snyder
2021-03-08 14:31          Kristina Sojakova
0 siblings, 1 reply; 19+ messages in thread
From: Noah Snyder @ 2021-03-08 13:38 UTC (permalink / raw)
To: Egbert Rijke; +Cc: Homotopy Type Theory, Kristina Sojakova

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

The generator of \pi_4(S^3) is the image of the generator of \pi_3(S^2)
under stabilization.  This is just the surjective the part of Freudenthal.
So to see that this generator has order dividing 2 one needs exactly two
things: the syllepsis, and my follow-up question about EH giving the
generator of \pi_3(S^2).  This is why I asked the follow-up question.

Note that putting formalization aside, that EH gives the generator of
\pi_4(S^3) and the syllepsis the proof that it has order 2, are well-known
among mathematicians via framed bordism theory (already Pontryagin knew
these two facts almost a hundred years ago).  So informally it’s clear to
mathematicians that the syllepsis shows this number is 1 or 2.  Formalizing
this well-known result remains an interesting question of course.

Best,

Noah

On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com> wrote:

> Dear Noah,
>
> I don't think that your claim that syllepsis gives a proof that Brunerie's
> number is 1 or 2 is accurate. Syllepsis gives you that a certain element of
> pi_4(S^3) has order 1 or 2, but it is an entirely different matter to show
> that this element generates the group. There could be many elements of
> order 2.
>
> Best wishes,
> Egbert
>
> On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke <e.m.rijke@gmail.com> wrote:
>
>> Hi Kristina,
>>
>> I've been on it already, because I was in that talk, and while my
>> formalization isn't yet finished, I do have all the pseudocode already.
>>
>> Best wishes,
>> Egbert
>>
>> On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder <nsnyder@gmail.com> wrote:
>>
>>> On the subject of formalization and the syllepsis, has it ever been
>>> formalized that Eckman-Hilton gives the generator of \pi_3(S^2)?  That is,
>>> we can build a 3-loop for S^2 by refl_refl_base --> surf \circ surf^{-1}
>>> --EH--> surf^{-1} \circ surf -->  refl_refl_base, and we want to show that
>>> under the equivalence \pi_3(S^2) --> Z constructed in the book that this
>>> 3-loop maps to \pm 1 (which sign you end up getting will depend on
>>> conventions).
>>>
>>> There's another explicit way to construct a generating a 3-loop on S^2,
>>> namely refl_refl_base --> surf \circ surf \circ \surf^-1 \circ surf^-1 --EH
>>> whiskered refl refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -->
>>> refl_refl_base, where I've suppressed a lot of associators and other
>>> details.  One could also ask whether this generator is the same as the one
>>> in my first paragraph.  This should be of comparable difficulty to the
>>> syllepsis (perhaps easier), but is another good example of something that's
>>> "easy" with string diagrams but a lot of work to translate into formalized
>>> HoTT.
>>>
>>> Best,
>>>
>>> Noah
>>>
>>> On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova <
>>> sojakova.kristina@gmail.com> wrote:
>>>
>>>> Dear all,
>>>>
>>>> Ali told me that apparently the following problem could be of interest
>>>> to some people (https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s):
>>>>
>>>> Given two higher paths p, q : 1_x = 1_x, Eckmann-Hilton gives us a path
>>>> EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) = 1_{p@q=q_p}.
>>>>
>>>> I just established the above in HoTT and am thinking of formalizing it,
>>>> unless someone already did it.
>>>>
>>>> Thanks,
>>>>
>>>> Kristina
>>>>
>>>> --
>>>> 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
>>>> .
>>>>
>>> --
>>> 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
>>> .
>>>
>>

--
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/CAO0tDg5AjiFOxBf%2BG6g8iW5ui30gXmQsgbEH31CCxSY%3DQVLybw%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 13:38        Noah Snyder
@ 2021-03-08 14:31          Kristina Sojakova
2021-03-08 15:10            Dan Christensen
0 siblings, 1 reply; 19+ messages in thread
From: Kristina Sojakova @ 2021-03-08 14:31 UTC (permalink / raw)
To: homotopytypetheory

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

Dear all,

I formalized my proof of syllepsis in Coq:
https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v

I am looking forward to see how it compares to the argument Egbert has
been working on.

Best,

Kristina

On 3/8/2021 2:38 PM, Noah Snyder wrote:
> The generator of \pi_4(S^3) is the image of the generator of
> \pi_3(S^2) under stabilization.  This is just the surjective the part
> of Freudenthal.  So to see that this generator has order dividing 2
> one needs exactly two things: the syllepsis, and my follow-up question
> about EH giving the generator of \pi_3(S^2).  This is why I asked the
> follow-up question.
>
> Note that putting formalization aside, that EH gives the generator of
> \pi_4(S^3) and the syllepsis the proof that it has order 2, are
> well-known among mathematicians via framed bordism theory (already
> Pontryagin knew these two facts almost a hundred years ago).  So
> informally it’s clear to mathematicians that the syllepsis shows this
> number is 1 or 2. Formalizing this well-known result remains an
> interesting question of course.
>
> Best,
>
> Noah
>
>
> On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com
> <mailto:e.m.rijke@gmail.com>> wrote:
>
>     Dear Noah,
>
>     I don't think that your claim that syllepsis gives a proof that
>     Brunerie's number is 1 or 2 is accurate. Syllepsis gives you that
>     a certain element of pi_4(S^3) has order 1 or 2, but it is an
>     entirely different matter to show that this element generates the
>     group. There could be many elements of order 2.
>
>     Best wishes,
>     Egbert
>
>     On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke <e.m.rijke@gmail.com
>     <mailto:e.m.rijke@gmail.com>> wrote:
>
>         Hi Kristina,
>
>         I've been on it already, because I was in that talk, and while
>         my formalization isn't yet finished, I do have all the
>
>         Best wishes,
>         Egbert
>
>         On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder <nsnyder@gmail.com
>         <mailto:nsnyder@gmail.com>> wrote:
>
>             On the subject of formalization and the syllepsis, has it
>             ever been formalized that Eckman-Hilton gives the
>             generator of \pi_3(S^2)? That is, we can build a 3-loop
>             for S^2 by refl_refl_base --> surf \circ surf^{-1} --EH-->
>             surf^{-1} \circ surf -->  refl_refl_base, and we want to
>             show that under the equivalence \pi_3(S^2) --> Z
>             constructed in the book that this 3-loop maps to \pm 1
>             (which sign you end up getting will depend on conventions).
>
>             There's another explicit way to construct a generating a
>             3-loop on S^2, namely refl_refl_base --> surf \circ surf
>             \circ \surf^-1 \circ surf^-1 --EH whiskered refl refl-->
>             surf \circ surf \circ surf^-1 \circ surf^-1 -->
>             refl_refl_base, where I've suppressed a lot of associators
>             and other details.  One could also ask whether this
>             generator is the same as the one in my first paragraph.
>             This should be of comparable difficulty to the syllepsis
>             (perhaps easier), but is another good example of something
>             that's "easy" with string diagrams but a lot of work to
>             translate into formalized HoTT.
>
>             Best,
>
>             Noah
>
>             On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>             <sojakova.kristina@gmail.com
>             <mailto:sojakova.kristina@gmail.com>> wrote:
>
>                 Dear all,
>
>                 Ali told me that apparently the following problem
>                 could be of interest
>                 to some people
>
>                 Given two higher paths p, q : 1_x = 1_x,
>                 Eckmann-Hilton gives us a path
>                 EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) =
>                 1_{p@q=q_p}.
>
>                 I just established the above in HoTT and am thinking
>                 of formalizing it,
>                 unless someone already did it.
>
>                 Thanks,
>
>                 Kristina
>
>                 --
>                 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
>                 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
>             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/7d4b6fd7-3035-e0b9-c966-97dd89d8b457%40gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 14:31          Kristina Sojakova
@ 2021-03-08 15:10            Dan Christensen
2021-03-08 15:15              Kristina Sojakova
2021-03-08 16:38              Kristina Sojakova
0 siblings, 2 replies; 19+ messages in thread
From: Dan Christensen @ 2021-03-08 15:10 UTC (permalink / raw)
To: homotopytypetheory

It's great to see this proved!

As a tangential remark, I mentioned after Jamie's talk that I had a
very short proof of Eckmann-Hilton, so I thought I should share it.
Kristina's proof is slightly different and is probably designed to
make the proof of syllepsis go through more easily, but here is mine.

Dan

Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p = 1) (k : 1 = q)
: h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
Proof.
by induction k; revert p h; rapply paths_ind_r.
Defined.

Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h : p = 1) (k : 1 = q)
: h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
Proof.
by induction k; revert p h; rapply paths_ind_r.
Defined.

Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x)) : h @ k = k @ h
:= (horizontal_vertical h k) @ (horizontal_vertical' k h)^.

On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> wrote:

> Dear all,
>
> I formalized my proof of syllepsis in Coq:
> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
>
>
> I am looking forward to see how it compares to the argument Egbert has
> been working on.
>
> Best,
>
> Kristina
>
> On 3/8/2021 2:38 PM, Noah Snyder wrote:
>
>     The generator of \pi_4(S^3) is the image of the generator of \pi_3
>     (S^2) under stabilization.  This is just the surjective the part
>     of Freudenthal.  So to see that this generator has order dividing
>     2 one needs exactly two things: the syllepsis, and my follow-up
>     question about EH giving the generator of \pi_3(S^2).  This is why
>     I asked the follow-up question.
>
>     Note that putting formalization aside, that EH gives the generator
>     of \pi_4(S^3) and the syllepsis the proof that it has order 2, are
>     well-known among mathematicians via framed bordism theory (already
>     Pontryagin knew these two facts almost a hundred years ago).  So
>     informally it’s clear to mathematicians that the syllepsis shows
>     this number is 1 or 2.  Formalizing this well-known result remains
>     an interesting question of course.
>
>     Best,
>
>     Noah
>
>     On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com>
>     wrote:
>
>         Dear Noah,
>
>         I don't think that your claim that syllepsis gives a proof
>         that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
>         you that a certain element of pi_4(S^3) has order 1 or 2, but
>         it is an entirely different matter to show that this element
>         generates the group. There could be many elements of order 2.
>
>         Best wishes,
>         Egbert
>
>         On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
>         <e.m.rijke@gmail.com> wrote:
>
>             Hi Kristina,
>
>             I've been on it already, because I was in that talk, and
>             while my formalization isn't yet finished, I do have all
>             the pseudocode already.
>
>             Best wishes,
>             Egbert
>
>             On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
>             <nsnyder@gmail.com> wrote:
>
>                 On the subject of formalization and the syllepsis, has
>                 it ever been formalized that Eckman-Hilton gives the
>                 generator of \pi_3(S^2)?  That is, we can build a
>                 3-loop for S^2 by refl_refl_base --> surf \circ surf^
>                 {-1} --EH--> surf^{-1} \circ surf -->  refl_refl_base,
>                 and we want to show that under the equivalence \pi_3
>                 (S^2) --> Z constructed in the book that this 3-loop
>                 maps to \pm 1 (which sign you end up getting will
>                 depend on conventions).
>
>                 There's another explicit way to construct a generating
>                 a 3-loop on S^2, namely refl_refl_base --> surf \circ
>                 surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>                 refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
>                 -> refl_refl_base, where I've suppressed a lot of
>                 associators and other details.  One could also ask
>                 whether this generator is the same as the one in my
>                 first paragraph.  This should be of comparable
>                 difficulty to the syllepsis (perhaps easier), but is
>                 another good example of something that's "easy" with
>                 string diagrams but a lot of work to translate into
>                 formalized HoTT.
>
>                 Best,
>
>                 Noah
>
>                 On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>                 <sojakova.kristina@gmail.com> wrote:
>
>                     Dear all,
>
>                     Ali told me that apparently the following problem
>                     could be of interest
>                     to some people
>
>
>                     Given two higher paths p, q : 1_x = 1_x,
>                     Eckmann-Hilton gives us a path
>                     EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p)
>                     = 1_{p@q=q_p}.
>
>                     I just established the above in HoTT and am
>                     thinking of formalizing it,
>                     unless someone already did it.
>
>                     Thanks,
>
>                     Kristina
>
>                     --
>                     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
>                     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
>                 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/87blbtk7ey.fsf%40uwo.ca.

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 15:10            Dan Christensen
@ 2021-03-08 15:15              Kristina Sojakova
2021-03-08 15:23                Noah Snyder
2021-03-08 16:38              Kristina Sojakova
1 sibling, 1 reply; 19+ messages in thread
From: Kristina Sojakova @ 2021-03-08 15:15 UTC (permalink / raw)
To: HomotopyTypeTheory

Thanks Dan! I think we should have no trouble showing that what I used
is equal to your proof but packaged a bit differently.

On 3/8/21 4:10 PM, Dan Christensen wrote:
> It's great to see this proved!
>
> As a tangential remark, I mentioned after Jamie's talk that I had a
> very short proof of Eckmann-Hilton, so I thought I should share it.
> Kristina's proof is slightly different and is probably designed to
> make the proof of syllepsis go through more easily, but here is mine.
>
> Dan
>
>
> Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p = 1) (k : 1 = q)
>    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
> Proof.
>    by induction k; revert p h; rapply paths_ind_r.
> Defined.
>
> Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h : p = 1) (k : 1 = q)
>    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
> Proof.
>    by induction k; revert p h; rapply paths_ind_r.
> Defined.
>
> Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x)) : h @ k = k @ h
>    := (horizontal_vertical h k) @ (horizontal_vertical' k h)^.
>
>
>
> On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
>
>> Dear all,
>>
>> I formalized my proof of syllepsis in Coq:
>> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
>>
>>
>> I am looking forward to see how it compares to the argument Egbert has
>> been working on.
>>
>> Best,
>>
>> Kristina
>>
>> On 3/8/2021 2:38 PM, Noah Snyder wrote:
>>
>>      The generator of \pi_4(S^3) is the image of the generator of \pi_3
>>      (S^2) under stabilization.  This is just the surjective the part
>>      of Freudenthal.  So to see that this generator has order dividing
>>      2 one needs exactly two things: the syllepsis, and my follow-up
>>      question about EH giving the generator of \pi_3(S^2).  This is why
>>      I asked the follow-up question.
>>
>>      Note that putting formalization aside, that EH gives the generator
>>      of \pi_4(S^3) and the syllepsis the proof that it has order 2, are
>>      well-known among mathematicians via framed bordism theory (already
>>      Pontryagin knew these two facts almost a hundred years ago).  So
>>      informally it’s clear to mathematicians that the syllepsis shows
>>      this number is 1 or 2.  Formalizing this well-known result remains
>>      an interesting question of course.
>>
>>      Best,
>>
>>      Noah
>>
>>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com>
>>      wrote:
>>
>>          Dear Noah,
>>
>>          I don't think that your claim that syllepsis gives a proof
>>          that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
>>          you that a certain element of pi_4(S^3) has order 1 or 2, but
>>          it is an entirely different matter to show that this element
>>          generates the group. There could be many elements of order 2.
>>
>>          Best wishes,
>>          Egbert
>>
>>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
>>          <e.m.rijke@gmail.com> wrote:
>>
>>              Hi Kristina,
>>
>>              I've been on it already, because I was in that talk, and
>>              while my formalization isn't yet finished, I do have all
>>              the pseudocode already.
>>
>>              Best wishes,
>>              Egbert
>>
>>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
>>              <nsnyder@gmail.com> wrote:
>>
>>                  On the subject of formalization and the syllepsis, has
>>                  it ever been formalized that Eckman-Hilton gives the
>>                  generator of \pi_3(S^2)?  That is, we can build a
>>                  3-loop for S^2 by refl_refl_base --> surf \circ surf^
>>                  {-1} --EH--> surf^{-1} \circ surf -->  refl_refl_base,
>>                  and we want to show that under the equivalence \pi_3
>>                  (S^2) --> Z constructed in the book that this 3-loop
>>                  maps to \pm 1 (which sign you end up getting will
>>                  depend on conventions).
>>
>>                  There's another explicit way to construct a generating
>>                  a 3-loop on S^2, namely refl_refl_base --> surf \circ
>>                  surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>>                  refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
>>                  -> refl_refl_base, where I've suppressed a lot of
>>                  associators and other details.  One could also ask
>>                  whether this generator is the same as the one in my
>>                  first paragraph.  This should be of comparable
>>                  difficulty to the syllepsis (perhaps easier), but is
>>                  another good example of something that's "easy" with
>>                  string diagrams but a lot of work to translate into
>>                  formalized HoTT.
>>
>>                  Best,
>>
>>                  Noah
>>
>>                  On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>>                  <sojakova.kristina@gmail.com> wrote:
>>
>>                      Dear all,
>>
>>                      Ali told me that apparently the following problem
>>                      could be of interest
>>                      to some people
>>
>>
>>                      Given two higher paths p, q : 1_x = 1_x,
>>                      Eckmann-Hilton gives us a path
>>                      EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p)
>>                      = 1_{p@q=q_p}.
>>
>>                      I just established the above in HoTT and am
>>                      thinking of formalizing it,
>>                      unless someone already did it.
>>
>>                      Thanks,
>>
>>                      Kristina
>>
>>                      --
>>                      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
>>                      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
>>                  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/1f7bbcb8-ee50-0c24-174e-d3852e52bbee%40gmail.com.

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 15:15              Kristina Sojakova
@ 2021-03-08 15:23                Noah Snyder
2021-03-08 15:35                  Noah Snyder
0 siblings, 1 reply; 19+ messages in thread
From: Noah Snyder @ 2021-03-08 15:23 UTC (permalink / raw)
To: Kristina Sojakova; +Cc: HomotopyTypeTheory

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

One funny remark, that \pi_3(S^2) = Z exactly tells you that any proof of
Eckman-Hilton is given by repeatedly applying either the standard proof or
its inverse.

In a sense there are exactly two “good” proofs of EH (the standard one and
it’s inverse).  In principle it’s not so automatic to see that a given
proof is one of the good two, but in practice it’d be hard to give a bad
one accidentally.  By contrast, put two people in two separate rooms and
there’s a good chance they’ll produce the two different good proofs (ie the
clockwise proof and the counterclockwise proof).  Best,

Noah

On Mon, Mar 8, 2021 at 10:15 AM Kristina Sojakova <
sojakova.kristina@gmail.com> wrote:

> Thanks Dan! I think we should have no trouble showing that what I used
> is equal to your proof but packaged a bit differently.
>
> On 3/8/21 4:10 PM, Dan Christensen wrote:
> > It's great to see this proved!
> >
> > As a tangential remark, I mentioned after Jamie's talk that I had a
> > very short proof of Eckmann-Hilton, so I thought I should share it.
> > Kristina's proof is slightly different and is probably designed to
> > make the proof of syllepsis go through more easily, but here is mine.
> >
> > Dan
> >
> >
> > Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p =
> 1) (k : 1 = q)
> >    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
> > Proof.
> >    by induction k; revert p h; rapply paths_ind_r.
> > Defined.
> >
> > Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h : p
> = 1) (k : 1 = q)
> >    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
> > Proof.
> >    by induction k; revert p h; rapply paths_ind_r.
> > Defined.
> >
> > Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x)) :
> h @ k = k @ h
> >    := (horizontal_vertical h k) @ (horizontal_vertical' k h)^.
> >
> >
> >
> > On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
> >
> >> Dear all,
> >>
> >> I formalized my proof of syllepsis in Coq:
> >>
> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
> >>
> >>
> >> I am looking forward to see how it compares to the argument Egbert has
> >> been working on.
> >>
> >> Best,
> >>
> >> Kristina
> >>
> >> On 3/8/2021 2:38 PM, Noah Snyder wrote:
> >>
> >>      The generator of \pi_4(S^3) is the image of the generator of \pi_3
> >>      (S^2) under stabilization.  This is just the surjective the part
> >>      of Freudenthal.  So to see that this generator has order dividing
> >>      2 one needs exactly two things: the syllepsis, and my follow-up
> >>      question about EH giving the generator of \pi_3(S^2).  This is why
> >>      I asked the follow-up question.
> >>
> >>      Note that putting formalization aside, that EH gives the generator
> >>      of \pi_4(S^3) and the syllepsis the proof that it has order 2, are
> >>      well-known among mathematicians via framed bordism theory (already
> >>      Pontryagin knew these two facts almost a hundred years ago).  So
> >>      informally it’s clear to mathematicians that the syllepsis shows
> >>      this number is 1 or 2.  Formalizing this well-known result remains
> >>      an interesting question of course.
> >>
> >>      Best,
> >>
> >>      Noah
> >>
> >>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com>
> >>      wrote:
> >>
> >>          Dear Noah,
> >>
> >>          I don't think that your claim that syllepsis gives a proof
> >>          that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
> >>          you that a certain element of pi_4(S^3) has order 1 or 2, but
> >>          it is an entirely different matter to show that this element
> >>          generates the group. There could be many elements of order 2.
> >>
> >>          Best wishes,
> >>          Egbert
> >>
> >>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
> >>          <e.m.rijke@gmail.com> wrote:
> >>
> >>              Hi Kristina,
> >>
> >>              I've been on it already, because I was in that talk, and
> >>              while my formalization isn't yet finished, I do have all
> >>              the pseudocode already.
> >>
> >>              Best wishes,
> >>              Egbert
> >>
> >>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
> >>              <nsnyder@gmail.com> wrote:
> >>
> >>                  On the subject of formalization and the syllepsis, has
> >>                  it ever been formalized that Eckman-Hilton gives the
> >>                  generator of \pi_3(S^2)?  That is, we can build a
> >>                  3-loop for S^2 by refl_refl_base --> surf \circ surf^
> >>                  {-1} --EH--> surf^{-1} \circ surf -->  refl_refl_base,
> >>                  and we want to show that under the equivalence \pi_3
> >>                  (S^2) --> Z constructed in the book that this 3-loop
> >>                  maps to \pm 1 (which sign you end up getting will
> >>                  depend on conventions).
> >>
> >>                  There's another explicit way to construct a generating
> >>                  a 3-loop on S^2, namely refl_refl_base --> surf \circ
> >>                  surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
> >>                  refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
> >>                  -> refl_refl_base, where I've suppressed a lot of
> >>                  associators and other details.  One could also ask
> >>                  whether this generator is the same as the one in my
> >>                  first paragraph.  This should be of comparable
> >>                  difficulty to the syllepsis (perhaps easier), but is
> >>                  another good example of something that's "easy" with
> >>                  string diagrams but a lot of work to translate into
> >>                  formalized HoTT.
> >>
> >>                  Best,
> >>
> >>                  Noah
> >>
> >>                  On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
> >>                  <sojakova.kristina@gmail.com> wrote:
> >>
> >>                      Dear all,
> >>
> >>                      Ali told me that apparently the following problem
> >>                      could be of interest
> >>                      to some people
> >>                      (
> >>
> >>
> >>                      Given two higher paths p, q : 1_x = 1_x,
> >>                      Eckmann-Hilton gives us a path
> >>                      EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p)
> >>                      = 1_{p@q=q_p}.
> >>
> >>                      I just established the above in HoTT and am
> >>                      thinking of formalizing it,
> >>                      unless someone already did it.
> >>
> >>                      Thanks,
> >>
> >>                      Kristina
> >>
> >>                      --
> >>                      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
> >>                      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
> >>                  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
> .
>

--
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/CAO0tDg6s-UAfQ5_i8f49hTHzfEk-_%2Bzp4C_bnFFvi9Ecnx%2BZEg%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 15:23                Noah Snyder
@ 2021-03-08 15:35                  Noah Snyder
2021-03-08 15:46                    Egbert Rijke
0 siblings, 1 reply; 19+ messages in thread
From: Noah Snyder @ 2021-03-08 15:35 UTC (permalink / raw)
To: Kristina Sojakova; +Cc: Homotopy Type Theory

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

My funny remark is slightly inaccurate.  \pi_3(S^2) just classifies proofs
of EH where both 2-loops are the same as each other.  It is true that
there's also a Z-worth of proofs of EH in the general case, but this is a
subtler fact about \pi_3(S^2 \wedge S^2).  Nonetheless  the point remains
that any two reasonable proofs of EH will be equal or inverse to each
other.  Best,

Noah

On Mon, Mar 8, 2021 at 10:23 AM Noah Snyder <nsnyder@gmail.com> wrote:

> One funny remark, that \pi_3(S^2) = Z exactly tells you that any proof of
> Eckman-Hilton is given by repeatedly applying either the standard proof or
> its inverse.
>
> In a sense there are exactly two “good” proofs of EH (the standard one and
> it’s inverse).  In principle it’s not so automatic to see that a given
> proof is one of the good two, but in practice it’d be hard to give a bad
> one accidentally.  By contrast, put two people in two separate rooms and
> there’s a good chance they’ll produce the two different good proofs (ie the
> clockwise proof and the counterclockwise proof).  Best,
>
> Noah
>
> On Mon, Mar 8, 2021 at 10:15 AM Kristina Sojakova <
> sojakova.kristina@gmail.com> wrote:
>
>> Thanks Dan! I think we should have no trouble showing that what I used
>> is equal to your proof but packaged a bit differently.
>>
>> On 3/8/21 4:10 PM, Dan Christensen wrote:
>> > It's great to see this proved!
>> >
>> > As a tangential remark, I mentioned after Jamie's talk that I had a
>> > very short proof of Eckmann-Hilton, so I thought I should share it.
>> > Kristina's proof is slightly different and is probably designed to
>> > make the proof of syllepsis go through more easily, but here is mine.
>> >
>> > Dan
>> >
>> >
>> > Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p
>> = 1) (k : 1 = q)
>> >    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
>> > Proof.
>> >    by induction k; revert p h; rapply paths_ind_r.
>> > Defined.
>> >
>> > Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h : p
>> = 1) (k : 1 = q)
>> >    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
>> > Proof.
>> >    by induction k; revert p h; rapply paths_ind_r.
>> > Defined.
>> >
>> > Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x))
>> : h @ k = k @ h
>> >    := (horizontal_vertical h k) @ (horizontal_vertical' k h)^.
>> >
>> >
>> >
>> > On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
>> >
>> >> Dear all,
>> >>
>> >> I formalized my proof of syllepsis in Coq:
>> >>
>> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
>> >>
>> >>
>> >> I am looking forward to see how it compares to the argument Egbert has
>> >> been working on.
>> >>
>> >> Best,
>> >>
>> >> Kristina
>> >>
>> >> On 3/8/2021 2:38 PM, Noah Snyder wrote:
>> >>
>> >>      The generator of \pi_4(S^3) is the image of the generator of \pi_3
>> >>      (S^2) under stabilization.  This is just the surjective the part
>> >>      of Freudenthal.  So to see that this generator has order dividing
>> >>      2 one needs exactly two things: the syllepsis, and my follow-up
>> >>      question about EH giving the generator of \pi_3(S^2).  This is why
>> >>      I asked the follow-up question.
>> >>
>> >>      Note that putting formalization aside, that EH gives the generator
>> >>      of \pi_4(S^3) and the syllepsis the proof that it has order 2, are
>> >>      well-known among mathematicians via framed bordism theory (already
>> >>      Pontryagin knew these two facts almost a hundred years ago).  So
>> >>      informally it’s clear to mathematicians that the syllepsis shows
>> >>      this number is 1 or 2.  Formalizing this well-known result remains
>> >>      an interesting question of course.
>> >>
>> >>      Best,
>> >>
>> >>      Noah
>> >>
>> >>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com>
>> >>      wrote:
>> >>
>> >>          Dear Noah,
>> >>
>> >>          I don't think that your claim that syllepsis gives a proof
>> >>          that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
>> >>          you that a certain element of pi_4(S^3) has order 1 or 2, but
>> >>          it is an entirely different matter to show that this element
>> >>          generates the group. There could be many elements of order 2.
>> >>
>> >>          Best wishes,
>> >>          Egbert
>> >>
>> >>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
>> >>          <e.m.rijke@gmail.com> wrote:
>> >>
>> >>              Hi Kristina,
>> >>
>> >>              I've been on it already, because I was in that talk, and
>> >>              while my formalization isn't yet finished, I do have all
>> >>              the pseudocode already.
>> >>
>> >>              Best wishes,
>> >>              Egbert
>> >>
>> >>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
>> >>              <nsnyder@gmail.com> wrote:
>> >>
>> >>                  On the subject of formalization and the syllepsis, has
>> >>                  it ever been formalized that Eckman-Hilton gives the
>> >>                  generator of \pi_3(S^2)?  That is, we can build a
>> >>                  3-loop for S^2 by refl_refl_base --> surf \circ surf^
>> >>                  {-1} --EH--> surf^{-1} \circ surf -->  refl_refl_base,
>> >>                  and we want to show that under the equivalence \pi_3
>> >>                  (S^2) --> Z constructed in the book that this 3-loop
>> >>                  maps to \pm 1 (which sign you end up getting will
>> >>                  depend on conventions).
>> >>
>> >>                  There's another explicit way to construct a generating
>> >>                  a 3-loop on S^2, namely refl_refl_base --> surf \circ
>> >>                  surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>> >>                  refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
>> >>                  -> refl_refl_base, where I've suppressed a lot of
>> >>                  associators and other details.  One could also ask
>> >>                  whether this generator is the same as the one in my
>> >>                  first paragraph.  This should be of comparable
>> >>                  difficulty to the syllepsis (perhaps easier), but is
>> >>                  another good example of something that's "easy" with
>> >>                  string diagrams but a lot of work to translate into
>> >>                  formalized HoTT.
>> >>
>> >>                  Best,
>> >>
>> >>                  Noah
>> >>
>> >>                  On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>> >>                  <sojakova.kristina@gmail.com> wrote:
>> >>
>> >>                      Dear all,
>> >>
>> >>                      Ali told me that apparently the following problem
>> >>                      could be of interest
>> >>                      to some people
>> >>                      (
>> >>
>> >>
>> >>                      Given two higher paths p, q : 1_x = 1_x,
>> >>                      Eckmann-Hilton gives us a path
>> >>                      EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p)
>> >>                      = 1_{p@q=q_p}.
>> >>
>> >>                      I just established the above in HoTT and am
>> >>                      thinking of formalizing it,
>> >>                      unless someone already did it.
>> >>
>> >>                      Thanks,
>> >>
>> >>                      Kristina
>> >>
>> >>                      --
>> >>                      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
>> >>                      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
>> >>                  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
>> .
>>
>

--
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/CAO0tDg6MCr7skausPPmomQrswRk1umaq3_V%3D52z60vxMj-hraQ%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 15:35                  Noah Snyder
@ 2021-03-08 15:46                    Egbert Rijke
2021-03-08 15:49                      Kristina Sojakova
2021-03-08 16:25                      Dan Christensen
0 siblings, 2 replies; 19+ messages in thread
From: Egbert Rijke @ 2021-03-08 15:46 UTC (permalink / raw)
To: Noah Snyder; +Cc: Kristina Sojakova, Homotopy Type Theory

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

Congratulations, Kristina, on doing it so fast.

I had a different route in mind, much less efficient. There are three kinds
of concatenations in the third identity type, all three pairs of them
satisfy interchange laws, and there is a coherence law between the three
interchange laws. This is what I had already formalized, and this coherence
law induces the syllepsis. But it takes me a lot more coding to do it in
the way I had in mind, which is why it takes me forever.

Best,
Egbert

On Mon, Mar 8, 2021 at 4:36 PM Noah Snyder <nsnyder@gmail.com> wrote:

> My funny remark is slightly inaccurate.  \pi_3(S^2) just classifies proofs
> of EH where both 2-loops are the same as each other.  It is true that
> there's also a Z-worth of proofs of EH in the general case, but this is a
> subtler fact about \pi_3(S^2 \wedge S^2).  Nonetheless  the point remains
> that any two reasonable proofs of EH will be equal or inverse to each
> other.  Best,
>
> Noah
>
> On Mon, Mar 8, 2021 at 10:23 AM Noah Snyder <nsnyder@gmail.com> wrote:
>
>> One funny remark, that \pi_3(S^2) = Z exactly tells you that any proof of
>> Eckman-Hilton is given by repeatedly applying either the standard proof or
>> its inverse.
>>
>> In a sense there are exactly two “good” proofs of EH (the standard one
>> and it’s inverse).  In principle it’s not so automatic to see that a given
>> proof is one of the good two, but in practice it’d be hard to give a bad
>> one accidentally.  By contrast, put two people in two separate rooms and
>> there’s a good chance they’ll produce the two different good proofs (ie the
>> clockwise proof and the counterclockwise proof).  Best,
>>
>> Noah
>>
>> On Mon, Mar 8, 2021 at 10:15 AM Kristina Sojakova <
>> sojakova.kristina@gmail.com> wrote:
>>
>>> Thanks Dan! I think we should have no trouble showing that what I used
>>> is equal to your proof but packaged a bit differently.
>>>
>>> On 3/8/21 4:10 PM, Dan Christensen wrote:
>>> > It's great to see this proved!
>>> >
>>> > As a tangential remark, I mentioned after Jamie's talk that I had a
>>> > very short proof of Eckmann-Hilton, so I thought I should share it.
>>> > Kristina's proof is slightly different and is probably designed to
>>> > make the proof of syllepsis go through more easily, but here is mine.
>>> >
>>> > Dan
>>> >
>>> >
>>> > Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p
>>> = 1) (k : 1 = q)
>>> >    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
>>> > Proof.
>>> >    by induction k; revert p h; rapply paths_ind_r.
>>> > Defined.
>>> >
>>> > Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h :
>>> p = 1) (k : 1 = q)
>>> >    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
>>> > Proof.
>>> >    by induction k; revert p h; rapply paths_ind_r.
>>> > Defined.
>>> >
>>> > Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x))
>>> : h @ k = k @ h
>>> >    := (horizontal_vertical h k) @ (horizontal_vertical' k h)^.
>>> >
>>> >
>>> >
>>> > On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com>
>>> wrote:
>>> >
>>> >> Dear all,
>>> >>
>>> >> I formalized my proof of syllepsis in Coq:
>>> >>
>>> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
>>> >>
>>> >>
>>> >> I am looking forward to see how it compares to the argument Egbert has
>>> >> been working on.
>>> >>
>>> >> Best,
>>> >>
>>> >> Kristina
>>> >>
>>> >> On 3/8/2021 2:38 PM, Noah Snyder wrote:
>>> >>
>>> >>      The generator of \pi_4(S^3) is the image of the generator of
>>> \pi_3
>>> >>      (S^2) under stabilization.  This is just the surjective the part
>>> >>      of Freudenthal.  So to see that this generator has order dividing
>>> >>      2 one needs exactly two things: the syllepsis, and my follow-up
>>> >>      question about EH giving the generator of \pi_3(S^2).  This is
>>> why
>>> >>      I asked the follow-up question.
>>> >>
>>> >>      Note that putting formalization aside, that EH gives the
>>> generator
>>> >>      of \pi_4(S^3) and the syllepsis the proof that it has order 2,
>>> are
>>> >>      well-known among mathematicians via framed bordism theory
>>> >>      Pontryagin knew these two facts almost a hundred years ago).  So
>>> >>      informally it’s clear to mathematicians that the syllepsis shows
>>> >>      this number is 1 or 2.  Formalizing this well-known result
>>> remains
>>> >>      an interesting question of course.
>>> >>
>>> >>      Best,
>>> >>
>>> >>      Noah
>>> >>
>>> >>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com
>>> >
>>> >>      wrote:
>>> >>
>>> >>          Dear Noah,
>>> >>
>>> >>          I don't think that your claim that syllepsis gives a proof
>>> >>          that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
>>> >>          you that a certain element of pi_4(S^3) has order 1 or 2, but
>>> >>          it is an entirely different matter to show that this element
>>> >>          generates the group. There could be many elements of order 2.
>>> >>
>>> >>          Best wishes,
>>> >>          Egbert
>>> >>
>>> >>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
>>> >>          <e.m.rijke@gmail.com> wrote:
>>> >>
>>> >>              Hi Kristina,
>>> >>
>>> >>              I've been on it already, because I was in that talk, and
>>> >>              while my formalization isn't yet finished, I do have all
>>> >>              the pseudocode already.
>>> >>
>>> >>              Best wishes,
>>> >>              Egbert
>>> >>
>>> >>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
>>> >>              <nsnyder@gmail.com> wrote:
>>> >>
>>> >>                  On the subject of formalization and the syllepsis,
>>> has
>>> >>                  it ever been formalized that Eckman-Hilton gives the
>>> >>                  generator of \pi_3(S^2)?  That is, we can build a
>>> >>                  3-loop for S^2 by refl_refl_base --> surf \circ surf^
>>> >>                  {-1} --EH--> surf^{-1} \circ surf -->
>>> refl_refl_base,
>>> >>                  and we want to show that under the equivalence \pi_3
>>> >>                  (S^2) --> Z constructed in the book that this 3-loop
>>> >>                  maps to \pm 1 (which sign you end up getting will
>>> >>                  depend on conventions).
>>> >>
>>> >>                  There's another explicit way to construct a
>>> generating
>>> >>                  a 3-loop on S^2, namely refl_refl_base --> surf \circ
>>> >>                  surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>>> >>                  refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
>>> >>                  -> refl_refl_base, where I've suppressed a lot of
>>> >>                  associators and other details.  One could also ask
>>> >>                  whether this generator is the same as the one in my
>>> >>                  first paragraph.  This should be of comparable
>>> >>                  difficulty to the syllepsis (perhaps easier), but is
>>> >>                  another good example of something that's "easy" with
>>> >>                  string diagrams but a lot of work to translate into
>>> >>                  formalized HoTT.
>>> >>
>>> >>                  Best,
>>> >>
>>> >>                  Noah
>>> >>
>>> >>                  On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>>> >>                  <sojakova.kristina@gmail.com> wrote:
>>> >>
>>> >>                      Dear all,
>>> >>
>>> >>                      Ali told me that apparently the following problem
>>> >>                      could be of interest
>>> >>                      to some people
>>> >>                      (
>>> >>
>>> >>
>>> >>                      Given two higher paths p, q : 1_x = 1_x,
>>> >>                      Eckmann-Hilton gives us a path
>>> >>                      EH(p,q) : p @ = q @ p. Show that EH(p,q) @
>>> EH(q,p)
>>> >>                      = 1_{p@q=q_p}.
>>> >>
>>> >>                      I just established the above in HoTT and am
>>> >>                      thinking of formalizing it,
>>> >>                      unless someone already did it.
>>> >>
>>> >>                      Thanks,
>>> >>
>>> >>                      Kristina
>>> >>
>>> >>                      --
>>> >>                      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
>>> >>                      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
>>> >>                  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
>>> .
>>>
>> --
> 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
> .
>

--
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/CAGqv1OAuHQwnZvvDfkM99o6Za%3DSrjPYO3J62MPMFxphDzVOiEw%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 15:46                    Egbert Rijke
@ 2021-03-08 15:49                      Kristina Sojakova
2021-03-08 16:25                      Dan Christensen
1 sibling, 0 replies; 19+ messages in thread
From: Kristina Sojakova @ 2021-03-08 15:49 UTC (permalink / raw)
To: Egbert Rijke, Noah Snyder; +Cc: Homotopy Type Theory

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

Thanks Egbert, I think it will be useful to have both proofs, as they
offer different insights.

On 3/8/21 4:46 PM, Egbert Rijke wrote:
> Congratulations, Kristina, on doing it so fast.
>
> I had a different route in mind, much less efficient. There are three
> kinds of concatenations in the third identity type, all three pairs of
> them satisfy interchange laws, and there is a coherence law between
> the three interchange laws. This is what I had already formalized, and
> this coherence law induces the syllepsis. But it takes me a lot more
> coding to do it in the way I had in mind, which is why it takes me
> forever.
>
> Best,
> Egbert
>
> On Mon, Mar 8, 2021 at 4:36 PM Noah Snyder <nsnyder@gmail.com
> <mailto:nsnyder@gmail.com>> wrote:
>
>     My funny remark is slightly inaccurate.  \pi_3(S^2) just
>     classifies proofs of EH where both 2-loops are the same as each
>     other.  It is true that there's also a Z-worth of proofs of EH in
>     the general case, but this is a subtler fact about \pi_3(S^2
>     \wedge S^2).  Nonetheless  the point remains that any two
>     reasonable proofs of EH will be equal or inverse to each other.
>     Best,
>
>     Noah
>
>     On Mon, Mar 8, 2021 at 10:23 AM Noah Snyder <nsnyder@gmail.com
>     <mailto:nsnyder@gmail.com>> wrote:
>
>         One funny remark, that \pi_3(S^2) = Z exactly tells you that
>         any proof of Eckman-Hilton is given by repeatedly applying
>         either the standard proof or its inverse.
>
>         In a sense there are exactly two “good” proofs of EH (the
>         standard one and it’s inverse).  In principle it’s not so
>         automatic to see that a given proof is one of the good two,
>         but in practice it’d be hard to give a bad one accidentally.
>         By contrast, put two people in two separate rooms and there’s
>         a good chance they’ll produce the two different good proofs
>         (ie the clockwise proof and the counterclockwise proof). Best,
>
>         Noah
>
>         On Mon, Mar 8, 2021 at 10:15 AM Kristina Sojakova
>         <sojakova.kristina@gmail.com
>         <mailto:sojakova.kristina@gmail.com>> wrote:
>
>             Thanks Dan! I think we should have no trouble showing that
>             what I used
>             is equal to your proof but packaged a bit differently.
>
>             On 3/8/21 4:10 PM, Dan Christensen wrote:
>             > It's great to see this proved!
>             >
>             > As a tangential remark, I mentioned after Jamie's talk
>             that I had a
>             > very short proof of Eckmann-Hilton, so I thought I
>             should share it.
>             > Kristina's proof is slightly different and is probably
>             designed to
>             > make the proof of syllepsis go through more easily, but
>             here is mine.
>             >
>             > Dan
>             >
>             >
>             > Definition horizontal_vertical {A : Type} {x : A} {p q :
>             x = x} (h : p = 1) (k : 1 = q)
>             >    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
>             > Proof.
>             >    by induction k; revert p h; rapply paths_ind_r.
>             > Defined.
>             >
>             > Definition horizontal_vertical' {A : Type} {x : A} {p q
>             : x = x} (h : p = 1) (k : 1 = q)
>             >    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
>             > Proof.
>             >    by induction k; revert p h; rapply paths_ind_r.
>             > Defined.
>             >
>             > Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 =
>             1 :> (x = x)) : h @ k = k @ h
>             >    := (horizontal_vertical h k) @ (horizontal_vertical'
>             k h)^.
>             >
>             >
>             >
>             > On Mar  8, 2021, Kristina Sojakova
>             <sojakova.kristina@gmail.com
>             <mailto:sojakova.kristina@gmail.com>> wrote:
>             >
>             >> Dear all,
>             >>
>             >> I formalized my proof of syllepsis in Coq:
>             >>
>             https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
>             >>
>             >>
>             >> I am looking forward to see how it compares to the
>             argument Egbert has
>             >> been working on.
>             >>
>             >> Best,
>             >>
>             >> Kristina
>             >>
>             >> On 3/8/2021 2:38 PM, Noah Snyder wrote:
>             >>
>             >>      The generator of \pi_4(S^3) is the image of the
>             generator of \pi_3
>             >>      (S^2) under stabilization.  This is just the
>             surjective the part
>             >>      of Freudenthal.  So to see that this generator has
>             order dividing
>             >>      2 one needs exactly two things: the syllepsis, and
>             my follow-up
>             >>      question about EH giving the generator of
>             \pi_3(S^2).  This is why
>             >>      I asked the follow-up question.
>             >>
>             >>      Note that putting formalization aside, that EH
>             gives the generator
>             >>      of \pi_4(S^3) and the syllepsis the proof that it
>             has order 2, are
>             >>      well-known among mathematicians via framed bordism
>             >>      Pontryagin knew these two facts almost a hundred
>             years ago).  So
>             >>      informally it’s clear to mathematicians that the
>             syllepsis shows
>             >>      this number is 1 or 2.  Formalizing this
>             well-known result remains
>             >>      an interesting question of course.
>             >>
>             >>      Best,
>             >>
>             >>      Noah
>             >>
>             >>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke
>             <e.m.rijke@gmail.com <mailto:e.m.rijke@gmail.com>>
>             >>      wrote:
>             >>
>             >>          Dear Noah,
>             >>
>             >>          I don't think that your claim that syllepsis
>             gives a proof
>             >>          that Brunerie's number is 1 or 2 is accurate.
>             Syllepsis gives
>             >>          you that a certain element of pi_4(S^3) has
>             order 1 or 2, but
>             >>          it is an entirely different matter to show
>             that this element
>             >>          generates the group. There could be many
>             elements of order 2.
>             >>
>             >>          Best wishes,
>             >>          Egbert
>             >>
>             >>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
>             >>          <e.m.rijke@gmail.com
>             <mailto:e.m.rijke@gmail.com>> wrote:
>             >>
>             >>              Hi Kristina,
>             >>
>             >>              I've been on it already, because I was in
>             that talk, and
>             >>              while my formalization isn't yet finished,
>             I do have all
>             >>              the pseudocode already.
>             >>
>             >>              Best wishes,
>             >>              Egbert
>             >>
>             >>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
>             >>              <nsnyder@gmail.com
>             <mailto:nsnyder@gmail.com>> wrote:
>             >>
>             >>                  On the subject of formalization and
>             the syllepsis, has
>             >>                  it ever been formalized that
>             Eckman-Hilton gives the
>             >>                  generator of \pi_3(S^2)? That is, we
>             can build a
>             >>                  3-loop for S^2 by refl_refl_base -->
>             surf \circ surf^
>             >>                  {-1} --EH--> surf^{-1} \circ surf -->
>             refl_refl_base,
>             >>                  and we want to show that under the
>             equivalence \pi_3
>             >>                  (S^2) --> Z constructed in the book
>             that this 3-loop
>             >>                  maps to \pm 1 (which sign you end up
>             getting will
>             >>                  depend on conventions).
>             >>
>             >>                  There's another explicit way to
>             construct a generating
>             >>                  a 3-loop on S^2, namely refl_refl_base
>             --> surf \circ
>             >>                  surf \circ \surf^-1 \circ surf^-1 --EH
>             whiskered refl
>             >>                  refl--> surf \circ surf \circ surf^-1
>             \circ surf^-1 -
>             >>                  -> refl_refl_base, where I've
>             suppressed a lot of
>             >>                  associators and other details.  One
>             could also ask
>             >>                  whether this generator is the same as
>             the one in my
>             >>                  first paragraph.  This should be of
>             comparable
>             >>                  difficulty to the syllepsis (perhaps
>             easier), but is
>             >>                  another good example of something
>             that's "easy" with
>             >>                  string diagrams but a lot of work to
>             translate into
>             >>                  formalized HoTT.
>             >>
>             >>                  Best,
>             >>
>             >>                  Noah
>             >>
>             >>                  On Fri, Mar 5, 2021 at 1:27 PM
>             Kristina Sojakova
>             >>                  <sojakova.kristina@gmail.com
>             <mailto:sojakova.kristina@gmail.com>> wrote:
>             >>
>             >>                      Dear all,
>             >>
>             >>                      Ali told me that apparently the
>             following problem
>             >>                      could be of interest
>             >>                      to some people
>             >>
>             >>
>             >>
>             >>                      Given two higher paths p, q : 1_x
>             = 1_x,
>             >>                      Eckmann-Hilton gives us a path
>             >>                      EH(p,q) : p @ = q @ p. Show that
>             EH(p,q) @ EH(q,p)
>             >>                      = 1_{p@q=q_p}.
>             >>
>             >>                      I just established the above in
>             HoTT and am
>             >>                      thinking of formalizing it,
>             >>                      unless someone already did it.
>             >>
>             >>                      Thanks,
>             >>
>             >>                      Kristina
>             >>
>             >>                      --
>             >>                      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
>             >>                      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
>             >>                  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
>             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
>

--
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/d0c29b9f-842a-f418-4c76-df1f040c422e%40gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 15:46                    Egbert Rijke
2021-03-08 15:49                      Kristina Sojakova
@ 2021-03-08 16:25                      Dan Christensen
2021-03-08 16:27                        Kristina Sojakova
1 sibling, 1 reply; 19+ messages in thread
From: Dan Christensen @ 2021-03-08 16:25 UTC (permalink / raw)
To: Homotopy Type Theory

On Mar  8, 2021, Egbert Rijke <e.m.rijke@gmail.com> wrote:

> I had a different route in mind, much less efficient. There are three
> kinds of concatenations in the third identity type, all three pairs of
> them satisfy interchange laws, and there is a coherence law between
> the three interchange laws.

In case anyone wants to play with this in Coq, in this branch

https://github.com/jdchristensen/HoTT/tree/Hurewicz

the file Smashing.v contains similar facts, e.g. pmagma_loops_shuffle.
(But no coherence law is proved.)

Dan

--
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/87pn09ipd5.fsf%40uwo.ca.

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 16:25                      Dan Christensen
@ 2021-03-08 16:27                        Kristina Sojakova
0 siblings, 0 replies; 19+ messages in thread
From: Kristina Sojakova @ 2021-03-08 16:27 UTC (permalink / raw)
To: HomotopyTypeTheory

Is there a geometric interpretation for the proof I gave?

On 3/8/21 5:25 PM, Dan Christensen wrote:
> On Mar  8, 2021, Egbert Rijke <e.m.rijke@gmail.com> wrote:
>
>> I had a different route in mind, much less efficient. There are three
>> kinds of concatenations in the third identity type, all three pairs of
>> them satisfy interchange laws, and there is a coherence law between
>> the three interchange laws.
> In case anyone wants to play with this in Coq, in this branch
>
>    https://github.com/jdchristensen/HoTT/tree/Hurewicz
>
> the file Smashing.v contains similar facts, e.g. pmagma_loops_shuffle.
> (But no coherence law is proved.)
>
> Dan
>

--
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/c4d0d50f-8a11-3d63-7c32-3fa3aae1fd96%40gmail.com.

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 15:10            Dan Christensen
2021-03-08 15:15              Kristina Sojakova
@ 2021-03-08 16:38              Kristina Sojakova
2021-03-08 16:54                Egbert Rijke
1 sibling, 1 reply; 19+ messages in thread
From: Kristina Sojakova @ 2021-03-08 16:38 UTC (permalink / raw)
To: HomotopyTypeTheory

If I'm not mistaken, Favonia also found a very short proof of EH some
years ago.

On 3/8/21 4:10 PM, Dan Christensen wrote:
> It's great to see this proved!
>
> As a tangential remark, I mentioned after Jamie's talk that I had a
> very short proof of Eckmann-Hilton, so I thought I should share it.
> Kristina's proof is slightly different and is probably designed to
> make the proof of syllepsis go through more easily, but here is mine.
>
> Dan
>
>
> Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p = 1) (k : 1 = q)
>    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
> Proof.
>    by induction k; revert p h; rapply paths_ind_r.
> Defined.
>
> Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h : p = 1) (k : 1 = q)
>    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
> Proof.
>    by induction k; revert p h; rapply paths_ind_r.
> Defined.
>
> Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x)) : h @ k = k @ h
>    := (horizontal_vertical h k) @ (horizontal_vertical' k h)^.
>
>
>
> On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
>
>> Dear all,
>>
>> I formalized my proof of syllepsis in Coq:
>> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
>>
>>
>> I am looking forward to see how it compares to the argument Egbert has
>> been working on.
>>
>> Best,
>>
>> Kristina
>>
>> On 3/8/2021 2:38 PM, Noah Snyder wrote:
>>
>>      The generator of \pi_4(S^3) is the image of the generator of \pi_3
>>      (S^2) under stabilization.  This is just the surjective the part
>>      of Freudenthal.  So to see that this generator has order dividing
>>      2 one needs exactly two things: the syllepsis, and my follow-up
>>      question about EH giving the generator of \pi_3(S^2).  This is why
>>      I asked the follow-up question.
>>
>>      Note that putting formalization aside, that EH gives the generator
>>      of \pi_4(S^3) and the syllepsis the proof that it has order 2, are
>>      well-known among mathematicians via framed bordism theory (already
>>      Pontryagin knew these two facts almost a hundred years ago).  So
>>      informally it’s clear to mathematicians that the syllepsis shows
>>      this number is 1 or 2.  Formalizing this well-known result remains
>>      an interesting question of course.
>>
>>      Best,
>>
>>      Noah
>>
>>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com>
>>      wrote:
>>
>>          Dear Noah,
>>
>>          I don't think that your claim that syllepsis gives a proof
>>          that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
>>          you that a certain element of pi_4(S^3) has order 1 or 2, but
>>          it is an entirely different matter to show that this element
>>          generates the group. There could be many elements of order 2.
>>
>>          Best wishes,
>>          Egbert
>>
>>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
>>          <e.m.rijke@gmail.com> wrote:
>>
>>              Hi Kristina,
>>
>>              I've been on it already, because I was in that talk, and
>>              while my formalization isn't yet finished, I do have all
>>              the pseudocode already.
>>
>>              Best wishes,
>>              Egbert
>>
>>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
>>              <nsnyder@gmail.com> wrote:
>>
>>                  On the subject of formalization and the syllepsis, has
>>                  it ever been formalized that Eckman-Hilton gives the
>>                  generator of \pi_3(S^2)?  That is, we can build a
>>                  3-loop for S^2 by refl_refl_base --> surf \circ surf^
>>                  {-1} --EH--> surf^{-1} \circ surf -->  refl_refl_base,
>>                  and we want to show that under the equivalence \pi_3
>>                  (S^2) --> Z constructed in the book that this 3-loop
>>                  maps to \pm 1 (which sign you end up getting will
>>                  depend on conventions).
>>
>>                  There's another explicit way to construct a generating
>>                  a 3-loop on S^2, namely refl_refl_base --> surf \circ
>>                  surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>>                  refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
>>                  -> refl_refl_base, where I've suppressed a lot of
>>                  associators and other details.  One could also ask
>>                  whether this generator is the same as the one in my
>>                  first paragraph.  This should be of comparable
>>                  difficulty to the syllepsis (perhaps easier), but is
>>                  another good example of something that's "easy" with
>>                  string diagrams but a lot of work to translate into
>>                  formalized HoTT.
>>
>>                  Best,
>>
>>                  Noah
>>
>>                  On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>>                  <sojakova.kristina@gmail.com> wrote:
>>
>>                      Dear all,
>>
>>                      Ali told me that apparently the following problem
>>                      could be of interest
>>                      to some people
>>
>>
>>                      Given two higher paths p, q : 1_x = 1_x,
>>                      Eckmann-Hilton gives us a path
>>                      EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p)
>>                      = 1_{p@q=q_p}.
>>
>>                      I just established the above in HoTT and am
>>                      thinking of formalizing it,
>>                      unless someone already did it.
>>
>>                      Thanks,
>>
>>                      Kristina
>>
>>                      --
>>                      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
>>                      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
>>                  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/8de81acf-3a00-ae98-7003-9eaf404d0b89%40gmail.com.

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 16:38              Kristina Sojakova
@ 2021-03-08 16:54                Egbert Rijke
2021-03-08 19:55                  'Favonia' via Homotopy Type Theory
0 siblings, 1 reply; 19+ messages in thread
From: Egbert Rijke @ 2021-03-08 16:54 UTC (permalink / raw)
To: Kristina Sojakova; +Cc: Homotopy Type Theory

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

My agda file with the the interchange laws and EH is here

https://github.com/HoTT-Intro/Agda/blob/master/extra/interchange.agda

And the coherence law is here

https://github.com/HoTT-Intro/Agda/blob/master/extra/syllepsis.agda

For anyone who is interested.

On Mon, Mar 8, 2021 at 5:38 PM Kristina Sojakova <
sojakova.kristina@gmail.com> wrote:

> If I'm not mistaken, Favonia also found a very short proof of EH some
> years ago.
>
> On 3/8/21 4:10 PM, Dan Christensen wrote:
> > It's great to see this proved!
> >
> > As a tangential remark, I mentioned after Jamie's talk that I had a
> > very short proof of Eckmann-Hilton, so I thought I should share it.
> > Kristina's proof is slightly different and is probably designed to
> > make the proof of syllepsis go through more easily, but here is mine.
> >
> > Dan
> >
> >
> > Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p =
> 1) (k : 1 = q)
> >    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
> > Proof.
> >    by induction k; revert p h; rapply paths_ind_r.
> > Defined.
> >
> > Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h : p
> = 1) (k : 1 = q)
> >    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
> > Proof.
> >    by induction k; revert p h; rapply paths_ind_r.
> > Defined.
> >
> > Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x)) :
> h @ k = k @ h
> >    := (horizontal_vertical h k) @ (horizontal_vertical' k h)^.
> >
> >
> >
> > On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
> >
> >> Dear all,
> >>
> >> I formalized my proof of syllepsis in Coq:
> >>
> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
> >>
> >>
> >> I am looking forward to see how it compares to the argument Egbert has
> >> been working on.
> >>
> >> Best,
> >>
> >> Kristina
> >>
> >> On 3/8/2021 2:38 PM, Noah Snyder wrote:
> >>
> >>      The generator of \pi_4(S^3) is the image of the generator of \pi_3
> >>      (S^2) under stabilization.  This is just the surjective the part
> >>      of Freudenthal.  So to see that this generator has order dividing
> >>      2 one needs exactly two things: the syllepsis, and my follow-up
> >>      question about EH giving the generator of \pi_3(S^2).  This is why
> >>      I asked the follow-up question.
> >>
> >>      Note that putting formalization aside, that EH gives the generator
> >>      of \pi_4(S^3) and the syllepsis the proof that it has order 2, are
> >>      well-known among mathematicians via framed bordism theory (already
> >>      Pontryagin knew these two facts almost a hundred years ago).  So
> >>      informally it’s clear to mathematicians that the syllepsis shows
> >>      this number is 1 or 2.  Formalizing this well-known result remains
> >>      an interesting question of course.
> >>
> >>      Best,
> >>
> >>      Noah
> >>
> >>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com>
> >>      wrote:
> >>
> >>          Dear Noah,
> >>
> >>          I don't think that your claim that syllepsis gives a proof
> >>          that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
> >>          you that a certain element of pi_4(S^3) has order 1 or 2, but
> >>          it is an entirely different matter to show that this element
> >>          generates the group. There could be many elements of order 2.
> >>
> >>          Best wishes,
> >>          Egbert
> >>
> >>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
> >>          <e.m.rijke@gmail.com> wrote:
> >>
> >>              Hi Kristina,
> >>
> >>              I've been on it already, because I was in that talk, and
> >>              while my formalization isn't yet finished, I do have all
> >>              the pseudocode already.
> >>
> >>              Best wishes,
> >>              Egbert
> >>
> >>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
> >>              <nsnyder@gmail.com> wrote:
> >>
> >>                  On the subject of formalization and the syllepsis, has
> >>                  it ever been formalized that Eckman-Hilton gives the
> >>                  generator of \pi_3(S^2)?  That is, we can build a
> >>                  3-loop for S^2 by refl_refl_base --> surf \circ surf^
> >>                  {-1} --EH--> surf^{-1} \circ surf -->  refl_refl_base,
> >>                  and we want to show that under the equivalence \pi_3
> >>                  (S^2) --> Z constructed in the book that this 3-loop
> >>                  maps to \pm 1 (which sign you end up getting will
> >>                  depend on conventions).
> >>
> >>                  There's another explicit way to construct a generating
> >>                  a 3-loop on S^2, namely refl_refl_base --> surf \circ
> >>                  surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
> >>                  refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
> >>                  -> refl_refl_base, where I've suppressed a lot of
> >>                  associators and other details.  One could also ask
> >>                  whether this generator is the same as the one in my
> >>                  first paragraph.  This should be of comparable
> >>                  difficulty to the syllepsis (perhaps easier), but is
> >>                  another good example of something that's "easy" with
> >>                  string diagrams but a lot of work to translate into
> >>                  formalized HoTT.
> >>
> >>                  Best,
> >>
> >>                  Noah
> >>
> >>                  On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
> >>                  <sojakova.kristina@gmail.com> wrote:
> >>
> >>                      Dear all,
> >>
> >>                      Ali told me that apparently the following problem
> >>                      could be of interest
> >>                      to some people
> >>                      (
> >>
> >>
> >>                      Given two higher paths p, q : 1_x = 1_x,
> >>                      Eckmann-Hilton gives us a path
> >>                      EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p)
> >>                      = 1_{p@q=q_p}.
> >>
> >>                      I just established the above in HoTT and am
> >>                      thinking of formalizing it,
> >>                      unless someone already did it.
> >>
> >>                      Thanks,
> >>
> >>                      Kristina
> >>
> >>                      --
> >>                      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
> >>                      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
> >>                  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
> .
>

--
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/CAGqv1ODEzmBLWmOvgVmtBO7D_xttUKDW6NSNF2Q2_3K7wfYcCA%40mail.gmail.com.

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

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

* Re: [HoTT] Syllepsis in HoTT
2021-03-08 16:54                Egbert Rijke
@ 2021-03-08 19:55                  'Favonia' via Homotopy Type Theory
0 siblings, 0 replies; 19+ messages in thread
From: 'Favonia' via Homotopy Type Theory @ 2021-03-08 19:55 UTC (permalink / raw)
To: Egbert Rijke; +Cc: Kristina Sojakova, Homotopy Type Theory, Dan Christensen

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

I remember multiple people (including me) discovered relatively short
proofs. Some history on GitHub: https://github.com/HoTT/book/issues/27

Best,
Favonia
they/them/theirs

On Mon, Mar 8, 2021 at 10:54 AM Egbert Rijke <e.m.rijke@gmail.com> wrote:

> My agda file with the the interchange laws and EH is here
>
> https://github.com/HoTT-Intro/Agda/blob/master/extra/interchange.agda
>
> And the coherence law is here
>
> https://github.com/HoTT-Intro/Agda/blob/master/extra/syllepsis.agda
>
> For anyone who is interested.
>
> On Mon, Mar 8, 2021 at 5:38 PM Kristina Sojakova <
> sojakova.kristina@gmail.com> wrote:
>
>> If I'm not mistaken, Favonia also found a very short proof of EH some
>> years ago.
>>
>> On 3/8/21 4:10 PM, Dan Christensen wrote:
>> > It's great to see this proved!
>> >
>> > As a tangential remark, I mentioned after Jamie's talk that I had a
>> > very short proof of Eckmann-Hilton, so I thought I should share it.
>> > Kristina's proof is slightly different and is probably designed to
>> > make the proof of syllepsis go through more easily, but here is mine.
>> >
>> > Dan
>> >
>> >
>> > Definition horizontal_vertical {A : Type} {x : A} {p q : x = x} (h : p
>> = 1) (k : 1 = q)
>> >    : h @ k = (concat_p1 p)^ @ (h @@ k) @ (concat_1p q).
>> > Proof.
>> >    by induction k; revert p h; rapply paths_ind_r.
>> > Defined.
>> >
>> > Definition horizontal_vertical' {A : Type} {x : A} {p q : x = x} (h : p
>> = 1) (k : 1 = q)
>> >    : h @ k = (concat_1p p)^ @ (k @@ h) @ (concat_p1 q).
>> > Proof.
>> >    by induction k; revert p h; rapply paths_ind_r.
>> > Defined.
>> >
>> > Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 = 1 :> (x = x))
>> : h @ k = k @ h
>> >    := (horizontal_vertical h k) @ (horizontal_vertical' k h)^.
>> >
>> >
>> >
>> > On Mar  8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
>> >
>> >> Dear all,
>> >>
>> >> I formalized my proof of syllepsis in Coq:
>> >>
>> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v
>> >>
>> >>
>> >> I am looking forward to see how it compares to the argument Egbert has
>> >> been working on.
>> >>
>> >> Best,
>> >>
>> >> Kristina
>> >>
>> >> On 3/8/2021 2:38 PM, Noah Snyder wrote:
>> >>
>> >>      The generator of \pi_4(S^3) is the image of the generator of \pi_3
>> >>      (S^2) under stabilization.  This is just the surjective the part
>> >>      of Freudenthal.  So to see that this generator has order dividing
>> >>      2 one needs exactly two things: the syllepsis, and my follow-up
>> >>      question about EH giving the generator of \pi_3(S^2).  This is why
>> >>      I asked the follow-up question.
>> >>
>> >>      Note that putting formalization aside, that EH gives the generator
>> >>      of \pi_4(S^3) and the syllepsis the proof that it has order 2, are
>> >>      well-known among mathematicians via framed bordism theory (already
>> >>      Pontryagin knew these two facts almost a hundred years ago).  So
>> >>      informally it’s clear to mathematicians that the syllepsis shows
>> >>      this number is 1 or 2.  Formalizing this well-known result remains
>> >>      an interesting question of course.
>> >>
>> >>      Best,
>> >>
>> >>      Noah
>> >>
>> >>      On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com>
>> >>      wrote:
>> >>
>> >>          Dear Noah,
>> >>
>> >>          I don't think that your claim that syllepsis gives a proof
>> >>          that Brunerie's number is 1 or 2 is accurate. Syllepsis gives
>> >>          you that a certain element of pi_4(S^3) has order 1 or 2, but
>> >>          it is an entirely different matter to show that this element
>> >>          generates the group. There could be many elements of order 2.
>> >>
>> >>          Best wishes,
>> >>          Egbert
>> >>
>> >>          On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke
>> >>          <e.m.rijke@gmail.com> wrote:
>> >>
>> >>              Hi Kristina,
>> >>
>> >>              I've been on it already, because I was in that talk, and
>> >>              while my formalization isn't yet finished, I do have all
>> >>              the pseudocode already.
>> >>
>> >>              Best wishes,
>> >>              Egbert
>> >>
>> >>              On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder
>> >>              <nsnyder@gmail.com> wrote:
>> >>
>> >>                  On the subject of formalization and the syllepsis, has
>> >>                  it ever been formalized that Eckman-Hilton gives the
>> >>                  generator of \pi_3(S^2)?  That is, we can build a
>> >>                  3-loop for S^2 by refl_refl_base --> surf \circ surf^
>> >>                  {-1} --EH--> surf^{-1} \circ surf -->  refl_refl_base,
>> >>                  and we want to show that under the equivalence \pi_3
>> >>                  (S^2) --> Z constructed in the book that this 3-loop
>> >>                  maps to \pm 1 (which sign you end up getting will
>> >>                  depend on conventions).
>> >>
>> >>                  There's another explicit way to construct a generating
>> >>                  a 3-loop on S^2, namely refl_refl_base --> surf \circ
>> >>                  surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>> >>                  refl--> surf \circ surf \circ surf^-1 \circ surf^-1 -
>> >>                  -> refl_refl_base, where I've suppressed a lot of
>> >>                  associators and other details.  One could also ask
>> >>                  whether this generator is the same as the one in my
>> >>                  first paragraph.  This should be of comparable
>> >>                  difficulty to the syllepsis (perhaps easier), but is
>> >>                  another good example of something that's "easy" with
>> >>                  string diagrams but a lot of work to translate into
>> >>                  formalized HoTT.
>> >>
>> >>                  Best,
>> >>
>> >>                  Noah
>> >>
>> >>                  On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>> >>                  <sojakova.kristina@gmail.com> wrote:
>> >>
>> >>                      Dear all,
>> >>
>> >>                      Ali told me that apparently the following problem
>> >>                      could be of interest
>> >>                      to some people
>> >>                      (
>> >>
>> >>
>> >>                      Given two higher paths p, q : 1_x = 1_x,
>> >>                      Eckmann-Hilton gives us a path
>> >>                      EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p)
>> >>                      = 1_{p@q=q_p}.
>> >>
>> >>                      I just established the above in HoTT and am
>> >>                      thinking of formalizing it,
>> >>                      unless someone already did it.
>> >>
>> >>                      Thanks,
>> >>
>> >>                      Kristina
>> >>
>> >>                      --
>> >>                      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
>> >>                      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
>> >>                  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
>> .
>>
> --
> 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
> .
>

--
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/CAH_%2Brvd184QS__yNafR5835opTA6DiZ1Wy%2BuGsDKp3%3DtG0TWPw%40mail.gmail.com.

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

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

end of thread, other threads:[~2021-03-08 19:55 UTC | newest]

Thread overview: 19+ messages (download: mbox.gz / follow: Atom feed)
2021-03-05 18:27 [HoTT] Syllepsis in HoTT Kristina Sojakova
2021-03-05 18:40  Jamie Vicary
2021-03-05 19:18    Noah Snyder
2021-03-07 18:00  Noah Snyder
2021-03-08  8:44    Egbert Rijke
2021-03-08  8:53      Egbert Rijke
2021-03-08 13:38        Noah Snyder
2021-03-08 14:31          Kristina Sojakova
2021-03-08 15:10            Dan Christensen
2021-03-08 15:15              Kristina Sojakova
2021-03-08 15:23                Noah Snyder
2021-03-08 15:35                  Noah Snyder
2021-03-08 15:46                    Egbert Rijke
2021-03-08 15:49                      Kristina Sojakova
2021-03-08 16:25                      Dan Christensen
2021-03-08 16:27                        Kristina Sojakova
2021-03-08 16:38              Kristina Sojakova
2021-03-08 16:54                Egbert Rijke
2021-03-08 19:55                  'Favonia' via Homotopy Type Theory


Discussion of Homotopy Type Theory and Univalent Foundations

This inbox may be cloned and mirrored by anyone:

git clone --mirror http://inbox.vuxu.org/hott

# If you have public-inbox 1.1+ installed, you may
# initialize and index your mirror using the following commands:
public-inbox-init -V1 hott hott/ http://inbox.vuxu.org/hott \
AGPL code for this site: git clone https://public-inbox.org/public-inbox.git