[-- Attachment #1: Type: text/plain, Size: 1443 bytes --] Dear all, I’m happy to announce that we’re recruiting for PhD students in HoTT (besides other topics) at Stockholm University, starting September 2021. Note that the deadline for applications is next Friday, 23 April — sorry I missed advertising it here sooner. Full details and application are through https://www.su.se/english/about-the-university/work-at-su/available-jobs/phd-student-positions-1.507588?rmpage=job&rmjob=14472&rmlang=UK Please let me know if you have any questions about the position! And (for advisors) please pass this on to any interested masters-level students. Answers to a few common questions: - PhD positions in Sweden are fully funded, with a livable salary. - The position includes up to 20% teaching. - Swedish speaking isn’t required, either formally or practically (though learning it during the PhD is encouraged) — all higher-level teaching is done in English, and most administrative business (including all necessities) can be. Best wishes, –Peter. -- 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/CAAkwb-%3DQCO9fw1BVjTtyihBphuoOaNbuviygm%2BaCMg8K5bTfjA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1985 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2102 bytes --] Dear all, A quick reminder of the researcher position in HoTT that I advertised a couple of weeks ago, with deadline this Friday (9 April). One point a couple of people asked about: Yes, this is effectively a postdoc — it’s formally called a “researcher” position here for administrative reasons. We are interested in applicants at any post-PhD stage (or expecting to complete their PhD before the position starts). Application link: https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=14506&rmlang=UK Once again, let me know if you have any questions! Best wishes, –Peter. On Mon, Mar 22, 2021 at 12:31 PM Peter LeFanu Lumsdaine < p.l.lumsdaine@gmail.com> wrote: > > Dear all, > > I’m pleased to announce that we’re hiring for a researcher position in Homotopy Type Theory at Stockholm University. It’s a 2 year position, provisionally starting this August, in the logic group of the Mathematics Department, supported by the Wallenberg Foundation project grant “Type Theory for Mathematics and Computer Science” (PI Thierry Coquand). The application deadline is 9 April. > > We welcome all applicants interested in working on homotopy type theory and related topics — either with previous background in HoTT, or with background in related fields but interested in moving into HoTT. > > Full details and application at > https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=14506&rmlang=UK > Departmental webpage: https://www.math.su.se > > Please get in touch with me if you have any questions about the position! > > Best, > –Peter. -- 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/CAAkwb-mW5%2BPShAxP1duTdB%2BFNZ-2Hfys%2BSEFDwWvv3gShMEPWg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2870 bytes --]

We are hiring lecturers / senior lecturers (corresponding to assistant / associate professors https://en.wikipedia.org/wiki/Senior_lecturer) at the School of Computer Science, University of Birmingham, UK. The official advert is here: https://bham.taleo.net/careersection/external/jobdetail.ftl?job=210000DX&tz=GMT%2B00%3A00&tzname=Europe%2FLondon In particular, applicants with interests close to our Theory Group are very welcome: https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-computation/index.aspx The interests of this group include, among other things, higher category theory, homotopy type theory, constructive mathematics, string diagrams and graphical calculi, proof assistants, topology and domain theory, game semantics, quantum computation, programming languages, verification and model checking, algorithms and complexity. Feel free to approach me or other members of the theory group for further information Martin -- 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/7b586bcf-3906-e5ba-d68e-e533d779bfc3%40googlemail.com.

[-- Attachment #1: Type: text/plain, Size: 1332 bytes --] Dear all, I’m pleased to announce that we’re hiring for a researcher position in Homotopy Type Theory at Stockholm University. It’s a 2 year position, provisionally starting this August, in the logic group of the Mathematics Department, supported by the Wallenberg Foundation project grant “Type Theory for Mathematics and Computer Science” (PI Thierry Coquand). The application deadline is 9 April. We welcome all applicants interested in working on homotopy type theory and related topics — either with previous background in HoTT, or with background in related fields but interested in moving into HoTT. Full details and application at https://www.su.se/english/about-the-university/work-at-su/available-jobs?rmpage=job&rmjob=14506&rmlang=UK Departmental webpage: https://www.math.su.se Please get in touch with me if you have any questions about the position! Best, –Peter. -- 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/CAAkwb-%3DHUbq3ucV4EMtshU37F8eefs6bAugDzcCo7N9ktLu2-Q%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1958 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3254 bytes --] We are hiring a research programmer at University of Minnesota to work with us on building next-generation proof assistant technology (broadly defined) based on homotopy type theory and cubical type theory. The ideal candidate would have some knowledge and interest in homotopy and cubical type theory, combined with concrete experience implementing type theoretic proof assistants using modern algorithms, such as bidirectional type checking and normalization-by-evaluation. You will be exposed to the latest research in the field and can get involved in theoretical development of the research ideas. We welcome applicants who do not have a Ph.D. degree---a BA/BS degree is sufficient. The research project is funded by the AFOSR through their MURI program, and your official affiliation would be the University of Minnesota with Favonia being your supervisor. However, you will frequently meet and collaborate with other researchers from Carnegie Mellon University, Wesleyan University, University of San Diego, and other institutions. Especially during the COVID-19 pandemic, most activities will be online, though you will have to be physically in the US. (We may be able to sponsor visas. Contact Favonia <kbh@umn.edu> for details.) We are interviewing candidates on a rolling basis until a match is found. Candidates applying by the end of March (2021/3/31) would be given priority. Here is the official link for application: https://hr.myu.umn.edu/jobs/ext/339220 Please also drop an email to Favonia <kbh@umn.edu> so that we can confirm that your application correctly enters the system. If you are a current employee of the University of Minnesota, please use https://hr.myu.umn.edu/jobs/int/339220 instead. # Some further information - What is the annual salary? About $60,000 USD. - When is the expected start date? As soon as you are ready. - How long does this position last? The position will last as long as the project can support it and benefit from it. However, the expectation is that you will be in this position around 1-3 years (negotiable) and may choose to leave early (for example, to start a Ph.D.). Your official contract will be one-year but renewable. - I see that there’s a “work experience” requirement. What counts as “work experience”? This requirement exists to satisfy an administrative requirement of the job code at the University of Minnesota. We will recognize a wide range of activities as “work experience”, such as contributions on GitHub during weekends. **Please document related activities in your CV.** If you are not sure if something counts as work experience, please ask Favonia <kbh@umn.edu >. - I have more questions! Please send an email to Favonia <kbh@umn.edu>. Best, Favonia they/them/theirs -- 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_%2Brvc0nayUNeSQvprodnpdQTfuXSLHeEicWTddRUhFRSDSxA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 11177 bytes --]

[-- 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 >> >> ( >> 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 >> . >> >> >> >> >> >> -- >> >> 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 >> . >> >> -- >> 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 >> . >> > -- > 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 > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODEzmBLWmOvgVmtBO7D_xttUKDW6NSNF2Q2_3K7wfYcCA%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAH_%2Brvd184QS__yNafR5835opTA6DiZ1Wy%2BuGsDKp3%3DtG0TWPw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 14604 bytes --]

[-- 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 > >> ( > 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 > . > >> > >> > >> -- > >> 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 > . > > -- > 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 > . > -- 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 --]

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 >> (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. >> >> >> -- >> 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. -- 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.

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.

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.

[-- 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 > 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 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 > >> > (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 > <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > >> To view this discussion on the web > visit > >> > https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com. > >> > >> > >> -- > >> You received this message because you > are subscribed > >> to the Google Groups "Homotopy Type > Theory" group. > >> To unsubscribe from this group and > stop receiving > >> emails from it, send an email to > >> HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > >> To view this discussion on the web visit > >> > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com. > > -- > You received this message because you are subscribed to > the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails > from it, send an email to > HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/1f7bbcb8-ee50-0c24-174e-d3852e52bbee%40gmail.com. > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto: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 > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg6MCr7skausPPmomQrswRk1umaq3_V%3D52z60vxMj-hraQ%40mail.gmail.com?utm_medium=email&utm_source=footer>. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d0c29b9f-842a-f418-4c76-df1f040c422e%40gmail.com. [-- Attachment #2: Type: text/html, Size: 23388 bytes --]

[-- 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 >>> (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 >>> >> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com >>> . >>> >> >>> >> >>> >> -- >>> >> You received this message because you are subscribed >>> >> to the Google Groups "Homotopy Type Theory" group. >>> >> To unsubscribe from this group and stop receiving >>> >> emails from it, send an email to >>> >> HomotopyTypeTheory+unsubscribe@googlegroups.com. >>> >> To view this discussion on the web visit >>> >> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com >>> . >>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/1f7bbcb8-ee50-0c24-174e-d3852e52bbee%40gmail.com >>> . >>> >> -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg6MCr7skausPPmomQrswRk1umaq3_V%3D52z60vxMj-hraQ%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg6MCr7skausPPmomQrswRk1umaq3_V%3D52z60vxMj-hraQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1OAuHQwnZvvDfkM99o6Za%3DSrjPYO3J62MPMFxphDzVOiEw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 15727 bytes --]

[-- 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 >> >> ( >> 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 >> . >> >> >> >> >> >> -- >> >> 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 >> . >> >> -- >> 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 >> . >> > -- 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 --]

[-- 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 > >> ( > 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 > . > >> > >> > >> -- > >> 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 > . > > -- > 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 > . > -- 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 --]

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 >> (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. >> >> >> -- >> 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. -- 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.

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 > (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. > > > -- > 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. -- 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.

[-- 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 > 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 > (https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s > <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 > <mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com>. > > -- > You received this message because you are subscribed to > the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails > from it, send an email to > HomotopyTypeTheory+unsubscribe@googlegroups.com > <mailto: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 > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com?utm_medium=email&utm_source=footer>. > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/7d4b6fd7-3035-e0b9-c966-97dd89d8b457%40gmail.com. [-- Attachment #2: Type: text/html, Size: 11410 bytes --]

[-- 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 >>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com >>>> . >>>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com >>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg5AjiFOxBf%2BG6g8iW5ui30gXmQsgbEH31CCxSY%3DQVLybw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 7138 bytes --]

[-- 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 >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com >>> . >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com >> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODR04M-4HB0-HvUsn%3Dmpe4PTR5osJUvFR6021xnCsd1sQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 5730 bytes --]

[-- 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 >> https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com >> . >> > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1OBJ7iSeng_MY3f%3DY1k3EWgm9Q6VpyU5-EH-j68H0BYC9w%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4913 bytes --]

[-- 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 > https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3540 bytes --]

[-- 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 > https://groups.google.com/d/msgid/HomotopyTypeTheory/CANr23v3E%2BkaPKgL-So_s_h95KUwSM5i1vPSqzQyEmKa%3D_D46iQ%40mail.gmail.com > . > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg4oCaZ--OuOVDynT5sXK5jQh1%2BOTM2FNzpx-QLEUg73Ng%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 3105 bytes --]

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.

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.

I don't have a particular application in mind at the moment. It just struck me how 2-adic integers have such simple coinductive definitions of the arithmetic operations, without any case distinctions at all, and I wondered whether there was a definition of plain integers with a similar property. It seems annoying to have to constantly case-split on a sign bit. I guess a lower-inductive representation could take advantage of the fact that the 2-adic representation of an integer other than 0 or -1 has a unique largest digit that differs from all larger digits, i.e. it's either ...0000 (i.e. 0) ...1111 (i.e. -1) ...0001 + arbitrary bit string ...1110 + arbitrary bit string This involves more case splits when defining arithmetic, but it would probably be an easy set to show that the HIT one is equivalent to. On Thu, Mar 4, 2021 at 7:02 PM Jason Gross <jasongross9@gmail.com> wrote: > > Note that the Coq standard library Z is a binary representation of integers and Z.testbit gives access to the infinite twos-compliment representation. Of course, it makes use of case-distinctions on sign to define it, but you go bit-by-bit; if the number is negative, you just invert the bit before returning it. Is there something you're after by having the representation not encode sign bits separately? > > On Thu, Mar 4, 2021, 21:27 Michael Shulman <shulman@sandiego.edu> wrote: >> >> On Thu, Mar 4, 2021 at 3:16 PM Nicolai Kraus <nicolai.kraus@gmail.com> wrote: >> > I'm not sure what the precise thing is that you're looking for because, without further specification, any standard definition of Z would qualify :-) >> >> Yes, that seems to be what Martin suggested too with ℕ + ℕ. It seemed >> to me as though the distance between ℕ + ℕ and my ℤ is greater than >> the distance between his 𝔹 and 𝔹', but maybe not in any important >> way. >> >> > The HIT is neat, but wouldn't it in practice behave pretty similar to a standard representation via binary lists? E.g. something like Unit + Bool * List(Bool), where inl(*) is zero, the first Bool is the sign, and you add a 1 in front of the list in order to get a positive integer. What's the advantage of the HIT - maybe one can avoid case distinctions? >> >> Is there a non-HIT binary representation that can be interpreted as >> two's-complement (thereby avoiding case distinctions on sign)? I >> haven't been able to figure out a way to do that with mere lists of >> booleans. >> >> -- >> 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/CAOvivQwtAMVnOG7D_A_s1EMAum4fv_x945MLB%2B01Y_pMdEKC2w%40mail.gmail.com. > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaqiyUcB%2BFrbvPmR-eS5ZMsb2CTVCtVbAYZeMUcOzCpmbA%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQxy2EJNScHu9Y2U%3DGLiHDrDxDq-Kg8Dz9TrFk3ZepiW8Q%40mail.gmail.com.