From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 26791 invoked from network); 10 Jul 2023 17:44:07 -0000 Received: from mail-wr1-x437.google.com (2a00:1450:4864:20::437) by inbox.vuxu.org with ESMTPUTF8; 10 Jul 2023 17:44:07 -0000 Received: by mail-wr1-x437.google.com with SMTP id ffacd0b85a97d-31421c900b7sf2762088f8f.3 for ; Mon, 10 Jul 2023 10:44:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1689011046; cv=pass; d=google.com; s=arc-20160816; b=f7oMmzJKJjaPNfBMvK7iDuEkqCrHvzZSIRbp9OGWR+p91jwUlaMYW0qhWQ5fbnvgog vp0lqe8iaUHV5Osb+y2ncAs0puX8vkYVDpSmZiC3T40crudhbLj8dKlqWnWT2q83UMf+ E4gaKUWNN7roMXfueXEctiX6t7Md6tzsm100GSsPDKNgof06+nI5H3lJvbQCczvj4OH1 pqAylZfdvDI0+gV8dAwvlkbfIIOOqNUz/0E0zauRQP+Sb95Y7zZHp3aQKU1ypq0u9gqF M8CaFz5Qgb9m7ApwQ+OMQsU1XyhYipwTQ7mad7t5735M9CrOAZscwd71u++i8AY1x+Qa G66w== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=7AIHNu9E0UtKzjAPPPhmUTiOTWCwdCcuYEoZdnTizYY=; fh=AY64mgA9CNmRu11+JKT54RFtWGi1puaesHjNPSTKJj0=; b=J0/m46OV0FRWsFK9lKJOIqJwep79cSe+YM4BLoYVlH0L0pM8NRWT9SCwdeV8lsXY0N v1Plk0UzJxlQx2j8jhkFn9p1Fr+PlyMeEYzuj2xp64Cc/cF3qWE0JPKF8gfdaeO8y1xk k3zYF0V8SysSzPFrOfpudUuX5PJ883IYG5np9cZfOdU92JJXEsqQpNrizuAsFcur6mrt Cg1AjuyBFvq0wkR0DapfnMRLnwPzBwv7EQI/5K95mBoMn/Ni6nEnZ29Vwsi9LPRw7+Uw S81ilOHuV44kX1nal3tHiEgHBQA9KdOIDHsVh0GWBOWcvFYxhMTqewd1E5j0yTv1wKYG YYkw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=C+SI5sZA; spf=pass (google.com: domain of nsnyder@gmail.com designates 2a00:1450:4864:20::131 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1689011046; x=1691603046; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=7AIHNu9E0UtKzjAPPPhmUTiOTWCwdCcuYEoZdnTizYY=; b=PDLWKEXbl+hZ80/Im72u92u+Rwwg70RkR1nCiSVrd1hMmlLaXDzSPWXY5gNOvMinHW 6NP7BNYV+dcoJQ4gz/e3x5Mh8tHpcKh4xis8NSnwS5BWYxU9qZvDnlwbAojDorQnDjGs rNyparSY33mUoggQaoIXjogKx1P2OcbMwM0yB9WOCkkB8xQbyRM78jx8nLklCkpQ/kBf bBjFnxBDlRV/1GkrWfW37m1Jfey+1p0aE7k8S/sUbyD3hADvckMDWftCe3JQaggvrNki 9Sc8fLT8Bo0Lfebz4vH6vZtg9DYUijAJ9dgujDeHpqVxyr1Un5leHb8EbCpjPu13bgnp aKwA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1689011046; x=1691603046; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:from:to:cc:subject:date:message-id:reply-to; bh=7AIHNu9E0UtKzjAPPPhmUTiOTWCwdCcuYEoZdnTizYY=; b=L9Myd7358TNdRifHgZ2pL8mFS/23FW7OiutuLPp9FbKJkH20NOoeKn6b6m/sONC4Wi PPCm/uFZvqBy9t4jiM2YLprtGiT4b4mdCF0tb1f2YXetwOZAQ1tt7765LP+wnVE19KWo HS366XD7cqbOQ70zoM4wFBdBK7Cex4SUa7jeTU9lFRwJcie4JkzPTuTYVr3HRplFqXpG Ko6Epd/Sbi0S5qRFz68fdjCYNn19MSAc54zAMdlPYGXj6bOCEtgwXm0PF2bprAQUjolg eREjnvOwcjfjwGwAEwQzKEA134BRRZGz4Fc/rJu2j1xD4HSl21L27e6WRDZiPEopTVZb CMAw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1689011046; x=1691603046; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=7AIHNu9E0UtKzjAPPPhmUTiOTWCwdCcuYEoZdnTizYY=; b=mA+Hi3cF0CuD35iWWz9A0E8EHqaeDNAIw0lsmygcidtctrHPlk+KTj8EFolUPWt25i WSYx46kUoYV+YJ2P61gdBszW52/4mQObugpsrx5/+h3ak98ukFW/Ew/f0j8/Va/dn5qX UatE2NQH/2Y3GhyERRP4xF66kp7MpgrDFUa3zcidQgw/gw4FeJLlusDH7dO/cvAEaSGr Ys/E5gMzPNWHJ98Ssb+sPeHsWhoOBIRzHpHwAGx/e78B5PwPshPvk7cYUZojiscOlP0r k+9ObPYiVbq8w1WNKiiDDueR9QxWxt6V3TGoWxYsKzbuR6sVcacSm0j3yBLvLGTqS138 ec+w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLbMEeC2Rsmx435MPR4EkDS6NvscoHDZz1+96mn1yinKfvOCrlFI wYnf+0L93XwlGKJ79BrL10E= X-Google-Smtp-Source: APBJJlEFUqsF7eqC7ImVnn+8+Cwi4qeES3pxzBsBGHjDboM72yDL1MHPKae9R/D/5vMuOy+lLkEE9g== X-Received: by 2002:a5d:40c1:0:b0:314:399f:cfa8 with SMTP id b1-20020a5d40c1000000b00314399fcfa8mr13760081wrq.43.1689011045831; Mon, 10 Jul 2023 10:44:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:3b06:b0:3fb:b071:d165 with SMTP id m6-20020a05600c3b0600b003fbb071d165ls2154061wms.0.-pod-prod-02-eu; Mon, 10 Jul 2023 10:44:03 -0700 (PDT) X-Received: by 2002:a1c:720e:0:b0:3fc:2e8:ea8b with SMTP id n14-20020a1c720e000000b003fc02e8ea8bmr8981324wmc.28.1689011043315; Mon, 10 Jul 2023 10:44:03 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1689011043; cv=none; d=google.com; s=arc-20160816; b=zAlgNSa6UKX4l/G3PnhQP1vZUgNFfo3+/Qa2ntEakaXV4T6eoYiTSOMgJuo7ExejkH sszlGkKNQnVAqhP+pLCpsdpgkgDjXp4Y39FN8XgRdw3m5VJQvgNSLHxDgUXemmbtGvkL IPIHzeRlw3S8oKuHG0CaFpnw0cQs3D+1m8+j4QUhllwrKB74n9No+JXIAWxbYC0iS+zg KiE3gKDmV1bKW83I4Ls+qqqM11eYVBCO7gFexZIDdZPDEcGhsHO8JWHcXuf8a2wLmb8D 3c8SXSVWCsmKvASfJ8V3fVWqZsnsxz1vtPcHYR4SQZSipixMaEg0xlJouMVzzOk9bcT/ Bozg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=5ixol07WYfLnog5F0MPgpGb3ae2Ie3C4zrtgpLCdwkw=; fh=AY64mgA9CNmRu11+JKT54RFtWGi1puaesHjNPSTKJj0=; b=W584bphG8KPEAkWmeUxGn0WWD9O5dSPl1H1DYKJbDSn2tFDv/lICZPASlO3ckIWi3D koJy5joFu6WZqU4qiKTatsEJqyourI1mvAHn0IKpLF1Cv2mqq47Bd3E2fzydy8PKExK8 3q4d8CjFFbxUmNH271WHvIw5E5ZJ0tSh92sbTlsgcDcZnuEAq95jmINTB2eO/VqtDmGl SLjHNIzS3NaHIQiNhIJNMxq2KpkmAkYuDWIa59UJctNTUtfQJivnEKF8sNs7OKUTfEwc 79IzCq07aHlEzYN5IBwatjDyy7qTBS/1kUFL2ojjrPqHQMt/MnJo2IURGhLH6BymlJjH feOQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=C+SI5sZA; spf=pass (google.com: domain of nsnyder@gmail.com designates 2a00:1450:4864:20::131 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x131.google.com (mail-lf1-x131.google.com. [2a00:1450:4864:20::131]) by gmr-mx.google.com with ESMTPS id p22-20020a05600c1d9600b003facc8c7725si583892wms.0.2023.07.10.10.44.03 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 10 Jul 2023 10:44:03 -0700 (PDT) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2a00:1450:4864:20::131 as permitted sender) client-ip=2a00:1450:4864:20::131; Received: by mail-lf1-x131.google.com with SMTP id 2adb3069b0e04-4f95bf5c493so7023638e87.3 for ; Mon, 10 Jul 2023 10:44:03 -0700 (PDT) X-Received: by 2002:a05:6512:128a:b0:4f8:5ab0:68c4 with SMTP id u10-20020a056512128a00b004f85ab068c4mr12945841lfs.59.1689011041913; Mon, 10 Jul 2023 10:44:01 -0700 (PDT) MIME-Version: 1.0 References: <5255bd6d-8b20-a4e5-bc6b-4f8418bc6700@gmail.com> <1F1A83E2-2EE9-42D6-BF30-D11DE1B12F56@andrej.com> <8e549102-49ca-407f-e95f-22d971f4b9fe@gmail.com> <7a08f997-1433-177d-ab99-b45ea4a14a8f@gmail.com> In-Reply-To: <7a08f997-1433-177d-ab99-b45ea4a14a8f@gmail.com> From: Noah Snyder Date: Mon, 10 Jul 2023 13:43:50 -0400 Message-ID: Subject: Re: [HoTT] Syllepsis for syllepsis To: Kristina Sojakova Cc: David Roberts , homotopytypetheory Content-Type: multipart/alternative; boundary="0000000000002ccf3306002587da" X-Original-Sender: nsnyder@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=C+SI5sZA; spf=pass (google.com: domain of nsnyder@gmail.com designates 2a00:1450:4864:20::131 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , --0000000000002ccf3306002587da Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Very nice! I really like this line of research! Let me try my hand at sketching what consequences I think this has for homotopy groups of spheres. This isn't exactly my area of expertise so I may have messed up something here. There's a TL;DR below. As a warmup let's talk about Eckmann-Hilton itself. EH says that if x and y are 2-loops, then xy =3D yx. Since this involves two variables this is a statement about a homotopy group of a wedge of spheres S^2 wedge S^2, namely it says that the commutator xyx^-1y^-1 which is non-trivial in \pi_1(S^1 wedge S^1) becomes trivial when you suspend it to get an element of \pi_2(S^2 wedge S^2). In other words, it gives a new relation (commutativity) in \pi_2(S^2 wedge S^2). From this viewpoint we can also easily get a statements about homotopy groups of wedges of spheres for more elaborate constructions. In particular, the syllepsis says that a certain element of \pi_3(S^2 wedge S^2) vanishes when you suspend it to \pi_4(S^3 wedge S^3). Finally, the "syllepsis of the syllepsis" (henceforth SoS, though see the postscript) says that a certain element of pi_5(S^3 wedge S^3) vanishes when you suspend it to pi_6(S^4 wedge S^4). Ok, but people are usually more interested in homotopy groups of spheres, rather than of wedges of two spheres. So let's go back to Eckmann-Hilton and think some more. We can consider EH where both variables are the same loop x (or, if you prefer, one is x and the other is x^-1) so that now we're talking about homotopy groups of a single sphere. Here something interesting happens, note that EH now gives an equality xx =3D xx, but we already knew xx =3D xx! Indeed if you look at the suspension map \pi_1(S^1) --> \pi_2 (S^2) it's an isomorphism, so we're not adding a new relation. Instead we're saying that xx =3D xx in two different ways! First xx =3D xx = via refl but second xx =3D xx via EH. If we compose one of these trivialization= s with the inverse of the other, what we end up with is a new element of pi_3(S^2). This is how EH is related to pi_3(S^2). Now let's think about what the syllepsis says about homotopy groups of spheres. So now we again want to look at the syllepsis of x with itself. This tells us that the element of pi_3(S^2) that we constructed from EH composed with itself will become trivial when suspended into pi_4(S^3). In this case this is killing 2 in Z, and so it really does add a new relation. Ok, now let's turn to SoS, and again restrict our attention to SoS of x with itself. This says that a certain element of pi_5(S^3) vanishes when suspended to pi_6(S^4). But if you look at the homotopy groups the map pi_5(S^3) --> pi_6(S^4) is already an isomorphism (this is analogous to what happened for EH!), in particular the paths (4) and (5) from Kristina's paper are already equal when p =3D q without assuming they're 4-loops! (I haven't thought at all how one would go about proving this though!) So instead we do what we did for EH, for a 4-loop x we have two different ways of showing (4) =3D (5) and this gives us an interesting element of pi_7(S^4= ). And looking in the table there is an interesting new element of pi_7(S^4) that doesn't come from pi_6(S^3), and I'd guess this construction gives this new generator of pi_7(S^4). Remark: Note that in general there's not a 1-to-1 relationship between interesting generators and relations in the homotopy groups of spheres (which are operations of one variable!) and interesting operations of two variables. You might need to write down a pretty elaborate composition of operators in two variables to write down a generator or relation in homotopy groups of spheres. In particular, the generator of pi_4(S^2) is a more elaborate composition (it's essentially EH applied to EH), the relation 2=3D0 in pi_4(S^2) is also more elaborate, and the generator of pi_6(S^3) is much much more elaborate! (In particular, the generator of pi_6(S^3) was essentially constructed by Andre Henriques, but in globular instead of HoTT so it's missing all the unitors and associators. Even without all the associators and unitors it's already extremely complicated! See http://globular.science/1702.001v2) TL;DR: First show that if you assume p =3D q then (4) =3D (5) is already tr= ue for 3-loops. Then taking p to be a 4-loop compose the proof of (4) =3D (5) using that p=3Dq with the inverse of the syllepsis of the syllepsis and you'll get an element of pi_7(S^4) which hopefully is the generator of the copy of Z in Z x Z/12 =3D pi_7(S^4). Best, Noah p.s. I wanted to push back a little on this "syllepsis of the syllepsis" name. The "syllepsis" gets its name because it's what you need to turn a "braided monoidal 2-category" into a "sylleptic monoidal 2-category." (Sylleptic in turn is just "symmetric" but changing "m" to "l" to make it a little bit less symmetric.) The "syllepsis of the syllepsis" by contrast is what's needed to turn a "sylleptic monoidal 2-category" into a "symmetric monoidal 2-category." That is, the parallel name would be the "symmetsis" or something similar. Perhaps a better nomenclature would be to use the E1 =3D monoidal, E2 =3D braided monoidal, E3, etc. phrasing which isn't specif= ic to 2-categories. So you might call Eckman-Hilton the E2-axiom, the syllepsis the E3-axiom, and the SoS the E4-axiom. There will also be an E5-axiom, though because of stability you won't see that when studying 2-categories, it'll come up when you look at 3-categories. Another way you might talk about it is the syllepsis is the "coherence of EH" while the syllepsis of the syllepsis is "the coherence of the coherence of EH" which I think maybe matches how you're thinking about the word sylleptsis? On Sat, Jul 8, 2023 at 4:14=E2=80=AFPM Kristina Sojakova < sojakova.kristina@gmail.com> wrote: > Hello David, > On 7/8/2023 4:00 PM, David Roberts wrote: > > Dear Kristina, > > Am I correct in assuming that the "syllepsis for syllepsis" is the > equality of (4) and (5) in your paper? > > Indeed, we show the equality between (4) and (5). > > > Is this related to the fact stable pi_2 is Z/2? > > We do not yet understand the implications of this result, that's another > interesting question I guess. Do you have a conjecture here? > > Kristina > > > Best, > > On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, < > sojakova.kristina@gmail.com> wrote: > >> Dear Andrej, >> >> Indeed, my message could have been more user-friendly. The file contains >> alternative proofs of Eckmann-Hilton and syllepsis, together with the >> proofs of the coherences described in Section 8 of >> >> https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf >> >> The last coherence outlined in the paper is what I referred to as >> "syllepsis for syllepsis". >> >> Best, >> >> Kristina >> >> On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote: >> > Dear Kristina, >> > >> > any chance you could spare a few words in English on the content of >> your formalization? Not everyone reads Coq code for breakfast. >> > >> > Many thanks in advance! >> > >> > Andrej >> > >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/8e549102-49ca-407f-= e95f-22d971f4b9fe%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/7a08f997-1433-177d-a= b99-b45ea4a14a8f%40gmail.com > > . > --=20 You received this message because you are subscribed to the Google Groups "= Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAO0tDg60ZcCDTgXM7WSWv7uQjCR5nmLe04X2y24uPge5HK%2B39w%40= mail.gmail.com. --0000000000002ccf3306002587da Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Very nice! I really like this line of research!

Let= me try my hand at sketching what consequences I think this has for homotop= y groups of spheres. This isn't exactly my area of expertise so I may h= ave messed up something here. There's a TL;DR below.

As a warmup= let's talk about Eckmann-Hilton itself. EH says that if x and y are 2-= loops, then xy =3D yx. Since this involves two variables this is a statemen= t about a homotopy group of a wedge of spheres S^2 wedge S^2, namely it say= s that the commutator xyx^-1y^-1 which is non-trivial in \pi_1(S^1 wedge S^= 1) becomes trivial when you suspend it to get an element of \pi_2(S^2 wedge= S^2). In other words, it gives a new relation (commutativity) in \pi_2(S^2= wedge S^2). From this viewpoint we can also easily get a statements about = homotopy groups of wedges of spheres for more elaborate constructions. In p= articular, the syllepsis says that a certain element of \pi_3(S^2 wedge S^2= ) vanishes when you suspend it to \pi_4(S^3 wedge S^3). Finally, the "= syllepsis of the syllepsis" (henceforth SoS, though see the postscript= ) says that a certain element of pi_5(S^3 wedge S^3) vanishes when you susp= end it to pi_6(S^4 wedge S^4).

Ok, but people are usually more inter= ested in homotopy groups of spheres, rather than of wedges of two spheres. = So let's go back to Eckmann-Hilton and think some more. We can consider= EH where both variables are the same loop x (or, if you prefer, one is x a= nd the other is x^-1) so that now we're talking about homotopy groups o= f a single sphere. Here something interesting happens, note that EH now giv= es an equality xx =3D xx, but we already knew xx =3D xx! Indeed if you look= at the suspension map \pi_1(S^1) --> \pi_2 (S^2) it's an isomorphis= m, so we're not adding a new relation. Instead we're saying that xx= =3D xx in two different ways! First xx =3D xx via refl but second xx =3D x= x via EH. If we compose one of these trivializations with the inverse of th= e other, what we end up with is a new element of pi_3(S^2). This is how EH = is related to pi_3(S^2).

Now let's think about what the syllepsi= s says about homotopy groups of spheres. So now we again want to look at th= e syllepsis of x with itself. This tells us that the element of pi_3(S^2) t= hat we constructed from EH composed with itself will become trivial when su= spended into pi_4(S^3). In this case this is killing 2 in Z, and so it real= ly does add a new relation.

Ok, now let's turn to SoS, and again= restrict our attention to SoS of x with itself. This says that a certain e= lement of pi_5(S^3) vanishes when suspended to pi_6(S^4). But if you look a= t the homotopy groups the map pi_5(S^3) --> pi_6(S^4) is already an isom= orphism (this is analogous to what happened for EH!), in particular the pat= hs (4) and (5) from Kristina's paper are already equal when p =3D q wit= hout assuming they're 4-loops! (I haven't thought at all how one wo= uld go about proving this though!) So instead we do what we did for EH, for= a 4-loop x we have two different ways of showing (4) =3D (5) and this give= s us an interesting element of pi_7(S^4). And looking in the table there is= an interesting new element of pi_7(S^4) that doesn't come from pi_6(S^= 3), and I'd guess this construction gives this new generator of pi_7(S^= 4).

Remark: Note that in general there's not a 1-to-1 relationsh= ip between interesting generators and relations in the homotopy groups of s= pheres (which are operations of one variable!) and interesting operations o= f two variables. You might need to write down a pretty elaborate compositio= n of operators in two variables to write down a generator or relation in ho= motopy groups of spheres. In particular, the generator of pi_4(S^2) is a mo= re elaborate composition (it's essentially EH applied to EH), the relat= ion 2=3D0 in pi_4(S^2) is also more elaborate, and the generator of pi_6(S^= 3) is much much more elaborate! (In particular, the generator of pi_6(S^3) = was essentially constructed by Andre Henriques, but in globular instead of = HoTT so it's missing all the unitors and associators. Even without all = the associators and unitors it's already extremely complicated! See http://globular.science/1702.00= 1v2)

TL;DR: First show that if you assume p =3D q then (4) =3D = (5) is already true for 3-loops. Then taking p to be a 4-loop compose the p= roof of (4) =3D (5) using that p=3Dq with the inverse of the syllepsis of t= he syllepsis and you'll get an element of pi_7(S^4) which hopefully is = the generator of the copy of Z in Z x Z/12 =3D pi_7(S^4).

Best,
<= br>Noah

p.s. I wanted to push back a little on this "syllepsis = of the syllepsis" name. The "syllepsis" gets its name becaus= e it's what you need to turn a "braided monoidal 2-category" = into a "sylleptic monoidal 2-category." (Sylleptic in turn is jus= t "symmetric" but changing "m" to "l" to make= it a little bit less symmetric.) The "syllepsis of the syllepsis"= ; by contrast is what's needed to turn a "sylleptic monoidal 2-cat= egory" into a "symmetric monoidal 2-category." That is, the = parallel name would be the "symmetsis" or something similar. Perh= aps a better nomenclature would be to use the E1 =3D monoidal, E2 =3D braid= ed monoidal, E3, etc. phrasing which isn't specific to 2-categories. So= you might call Eckman-Hilton the E2-axiom, the syllepsis the E3-axiom, and= the SoS the E4-axiom. There will also be an E5-axiom, though because of st= ability you won't see that when studying 2-categories, it'll come u= p when you look at 3-categories. Another way you might talk about it is the= syllepsis is the "coherence of EH" while the syllepsis of the sy= llepsis is "the coherence of the coherence of EH" which I think m= aybe matches how you're thinking about the word sylleptsis?
On Sat, = Jul 8, 2023 at 4:14=E2=80=AFPM Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
=20 =20 =20

Hello David,

On 7/8/2023 4:00 PM, David Roberts wrote:
=20
Dear Kristina,

Am I correct in assuming that the "syllepsis= for syllepsis" is the equality of (4) and (5) in your paper?
Indeed, we show the equality between (4) and (5).

Is this related to the fact stable pi_2 is Z/2?

We do not yet understand the implications of this result, that's another interesting question I guess. Do you have a conjecture here?

Kristina


Best,

On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, <sojakova.kristina@gmail.com> wrote:
Dear Andrej,

Indeed, my message could have been more user-friendly. The file contains
alternative proofs of Eckmann-Hilton and syllepsis, together with the
proofs of the coherences described in Section 8 of

https://inria.hal.sc= ience/hal-03917004v1/file/syllepsis.pdf

The last coherence outlined in the paper is what I referred to as
"syllepsis for syllepsis".

Best,

Kristina

On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
> Dear Kristina,
>
> any chance you could spare a few words in English on the content of your formalization? Not everyone reads Coq code for breakfast.
>
> Many thanks in advance!
>
> Andrej
>

--
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 HomotopyTypeT= heory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://grou= ps.google.com/d/msgid/HomotopyTypeTheory/8e549102-49ca-407f-e95f-22d971f4b9= fe%40gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a= 14a8f%40gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg60ZcCDTgXM7WSWv7uQjCR5nm= Le04X2y24uPge5HK%2B39w%40mail.gmail.com.
--0000000000002ccf3306002587da--