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 autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 17681 invoked from network); 8 Mar 2021 15:23:56 -0000 Received: from mail-oo1-xc3d.google.com (2607:f8b0:4864:20::c3d) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 15:23:56 -0000 Received: by mail-oo1-xc3d.google.com with SMTP id q23sf5341553oot.1 for ; Mon, 08 Mar 2021 07:23:56 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615217034; cv=pass; d=google.com; s=arc-20160816; b=cz3FVnuxx7U1bOBkkPsA/7ihmdIbrAKYLxny9mwLQ7lUZf7oJM3cHeyDrQspvzIvmM pFiuBMtZQOl4/JOwsNbrJ7rwOICH2ws+PHLc5bxYITWezLhtj0PtlnKeG1E2ngolzr/A iAWfqUlkahZV/nYO7GSLEVZbsUbBhRfkljFFh1JdrE5WS/pdFAnYxbHg+d/zCch/cD1z NCYVC29jJ56G6xC/7+LmquIYQK/x3Wjpgm/Nby+PQFwXH8DsA9trUpxztPH2p0t+FSJ9 +RLF3ARr+jCu69Z6hAZiVfQmF11GTYLMadcGstMb17FuqML5UXSXW8sy2NZwO3MeufWI KmRQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe: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=+SyN0PNIXbwe1Dcr5gzP3h0c71ADMmEFNZgsm8vSyRY=; b=Y1xnvGorOtuO77cKKsv6AMlmJRKKHLgB3WSeXNEQxgSh5ES1A7P011BvbmtPSdYd96 wc4xWKj8W6Z5LqOSRur+7PgHOgmOP5fYhS85qjez2APX1BuGD/be6XAlaSkS7uDDbewn Fk1GdcP4a+Z35EvVwnQAuvJ89as07vvWNw7YEbB3bVDclEFS3auWXZihMroWYvidAXRD dEUwQORH1+vvloFEeELo4HUJHgKAGwUg3584MQqgUj1itzt0ERMj4ipt4BgZTmMFcUPj KZXcVvXuC3344e1+/fHDB9vnD9TYhMdPK7VxkeeVAKxxm53bzwWdAqReA5h4FIM/NZsm gKRA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=o42pPl1f; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::935 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=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+SyN0PNIXbwe1Dcr5gzP3h0c71ADMmEFNZgsm8vSyRY=; b=k/gyh8DMtlXrXLdH75XJsNb4IfRyubCUu9xckV369z1IKypzPxYEQc15xJenkzdBzD uP5PBVcxta18jMRFtx2LQ8yCOW4fCT1nkLG0OD+eUckRHi3dt3aenNV2dZezwzs6COEA GpzDzyi+MdsaOK/o46Rjv4dlg3aIDqGBAHd7UPfvSRPph+VEDrUfiBggeNLzQpHQ+qiI h7qVf/QRHaF4fusb7qRGA8utpW4lddfAZrd11GsG7fkG77IQA9qXoIjStluk+C6mwrQh 4impiSQmKJn2fT3wY/gG63lxi35+nvhDkAbn3RViBVChvyMBIDuS07smsya4t+F22a9g +OBw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+SyN0PNIXbwe1Dcr5gzP3h0c71ADMmEFNZgsm8vSyRY=; b=nu94Fo6EQhcImdlhSPS5xJSTuRDIu/G7iiBlngl271SY4DsGbQgzr9y1mdKsVHkqXx ML0zzvg9OSthlFxPG2LKCvx+J87G+jafNdyXDkCXxjfkyrnmhJgkQL/hFnst8wlb/ZVq 831S4mD3zSImb3jej6eTLndHkSdYgCMTMivoH5jAisoycvH+haArT47oPCNLHrYX8GGL YGlCqBAqrM6/h78KUU9Du2KTJWRQ4DTDTG1j18ARLLKo3FJE3DpygGSMhPUVlsj6cv44 UrVB3wXxVIZUqLjU5mRlJZ2rNLI+Vjx6VkgLzKhf7hI4eIOwFMlTkgAudgpIOT1vnL3S RqHw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=+SyN0PNIXbwe1Dcr5gzP3h0c71ADMmEFNZgsm8vSyRY=; b=Df6eAzvS4Mt6xEwO38kNYOai+usscb+AYL1BWRbEgE8HX5CFtJ0OWDfSKab0mtPWpO pYgaeKY/3FR20ZLpvyeEo7Ko5sgf3il87SeeJ6BdlAUYD3ffM2CpuZDMT1TstCmJ7f73 LS/ECefN+eEhPPKGzdlnr4fGZY1GONPt6OoPF6sV0LTpFT5P/j9e5MZeLHD8yRTBpsfz yVqWGhOQDujx7hXqXL0Gw4WOe/rh8uN28kQxjaviTSdrUtar11XoVL9shMlEYk2/o/Uh emrnawQpQ5/6ug5cLHSrRBdieVngzBgPgPV4qEIiVIsUsDYAWW43sgQNZjKsWN2Jd9E7 zS4Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530/eT18CG0gX0kFMdoShwAP6CyuD3GjXpz2fHMxu22xb/YfSVp7 r4FEkYhqcpBzMOdBQb5v5PE= X-Google-Smtp-Source: ABdhPJxSfRgkhlNsifulC4VWoVDzvjmCj5wj/bc5l8QkcSOcz4sEeQdSd1c/h5f1oMIUpHUiTzJkGw== X-Received: by 2002:a05:6830:1502:: with SMTP id k2mr20654877otp.166.1615217034285; Mon, 08 Mar 2021 07:23:54 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:1156:: with SMTP id u22ls4421854oiu.6.gmail; Mon, 08 Mar 2021 07:23:53 -0800 (PST) X-Received: by 2002:a05:6808:b15:: with SMTP id s21mr13971103oij.130.1615217033914; Mon, 08 Mar 2021 07:23:53 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615217033; cv=none; d=google.com; s=arc-20160816; b=Dyza4GzWfMiHKbQ9RQd8HDIaSgtyr4NMpIvCw6joXG5SI924OIUz2bPRNEWd2XHTg8 k2H9Y1iF9Hky/sz1XOlC02YM6uCHZU8jhFaYjLO7DVdNF5q5Gyw81j3Lkj9XcDgId/f2 /KcWkGDRlpwBPDiYaRTtikFgo/bgnTkpxWuHvphE29lYs4xnmSf91jZxkLfARjelHt/3 OKCDv7cbY4n3Sd3A2Y2keKnpyzpj6gY21e4yW6D9cWs95qyNtdN08M7p5HJiiOuq+uM2 ixn1oiLy26TTk3tmIcySkP02mJ9w/jJIMzU0v+w5q7y9Z0Dr0SzFmWexLDKkR40uGFXW xFVQ== 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=uaCCNXRAWrT7elaYgX3bP412gml33peAN9cdJq2Buks=; b=XNz0nOlCElf/ewxGP73KXkpVqS7v8uPNN5cDuVGsnn8pdjFUEa8C2I6OVAxZKFbZNY 4/Hk34/7/iNYgzkC0QODcfSPB7UWE+HydKdFjkfbbkD2a2iOQ8tXUR0OS1aZ+VeYZZea uzfMIxgFXynUWH3NX6Bzk5h/6b4eMAzNQxmt6ZM/jQcy3svLYKPIqNf1HOzH16wsAOsv sPFMirZ61jzc7MTZGsRRFz2wq5w/+uedBA3eMFygUgug/x9xy8xZHpy0T7f8/wraQPi5 Yf9Po69c/ADCMmS5E2AF1XwIvf5Q3FMjGhXtA5q/VcAhRAlAVOJ3sfniQPFyk0KhErfu y4ow== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=o42pPl1f; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::935 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ua1-x935.google.com (mail-ua1-x935.google.com. [2607:f8b0:4864:20::935]) by gmr-mx.google.com with ESMTPS id s7si640959ois.0.2021.03.08.07.23.53 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 07:23:53 -0800 (PST) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::935 as permitted sender) client-ip=2607:f8b0:4864:20::935; Received: by mail-ua1-x935.google.com with SMTP id u13so3416496uap.8 for ; Mon, 08 Mar 2021 07:23:53 -0800 (PST) X-Received: by 2002:a9f:2341:: with SMTP id 59mr11441254uae.30.1615217033309; Mon, 08 Mar 2021 07:23:53 -0800 (PST) MIME-Version: 1.0 References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> <7d4b6fd7-3035-e0b9-c966-97dd89d8b457@gmail.com> <87blbtk7ey.fsf@uwo.ca> <1f7bbcb8-ee50-0c24-174e-d3852e52bbee@gmail.com> In-Reply-To: <1f7bbcb8-ee50-0c24-174e-d3852e52bbee@gmail.com> From: Noah Snyder Date: Mon, 8 Mar 2021 10:23:42 -0500 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Kristina Sojakova Cc: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000008172b805bd080565" X-Original-Sender: nsnyder@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=o42pPl1f; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::935 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: , --0000000000008172b805bd080565 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable One funny remark, that \pi_3(S^2) =3D 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 =E2=80=9Cgood=E2=80=9D proofs of EH (the s= tandard one and it=E2=80=99s inverse). In principle it=E2=80=99s not so automatic to see t= hat a given proof is one of the good two, but in practice it=E2=80=99d be hard to give = a bad one accidentally. By contrast, put two people in two separate rooms and there=E2=80=99s a good chance they=E2=80=99ll produce the two different goo= d 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 =3D x} (h : = p =3D > 1) (k : 1 =3D q) > > : h @ k =3D (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 =3D x} (h := p > =3D 1) (k : 1 =3D q) > > : h @ k =3D (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 =3D 1 :> (x =3D = x)) : > h @ k =3D k @ h > > :=3D (horizontal_vertical h k) @ (horizontal_vertical' k h)^. > > > > > > > > On Mar 8, 2021, Kristina Sojakova wrote: > > > >> Dear all, > >> > >> I formalized my proof of syllepsis in Coq: > >> > https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colim= its/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 wh= y > >> I asked the follow-up question. > >> > >> Note that putting formalization aside, that EH gives the generato= r > >> of \pi_4(S^3) and the syllepsis the proof that it has order 2, ar= e > >> well-known among mathematicians via framed bordism theory (alread= y > >> Pontryagin knew these two facts almost a hundred years ago). So > >> informally it=E2=80=99s clear to mathematicians that the syllepsi= s shows > >> this number is 1 or 2. Formalizing this well-known result remain= s > >> an interesting question of course. > >> > >> Best, > >> > >> Noah > >> > >> On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke > >> 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 > >> 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 > >> wrote: > >> > >> On the subject of formalization and the syllepsis, ha= s > >> 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 generatin= g > >> 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 > >> wrote: > >> > >> Dear all, > >> > >> Ali told me that apparently the following problem > >> could be of interest > >> to some people > >> ( > https://www.youtube.com/watch?v=3DTSCggv_YE7M&t=3D4350s): > >> > >> > >> Given two higher paths p, q : 1_x =3D 1_x, > >> Eckmann-Hilton gives us a path > >> EH(p,q) : p @ =3D q @ p. Show that EH(p,q) @ EH(q= ,p) > >> =3D 1_{p@q=3Dq_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-5= 91f-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/CAO0tDg7MCVQWLfSf13P= vEu%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-1= 74e-d3852e52bbee%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/CAO0tDg6s-UAfQ5_i8f49hTHzfEk-_%2Bzp4C_bnFFvi9Ecnx%2BZEg%= 40mail.gmail.com. --0000000000008172b805bd080565 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
One funny remark, that \pi_3(S^2) =3D 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 =E2=80=9Cgood=E2=80=9D proofs of= EH (the standard one and it=E2=80=99s inverse).=C2=A0 In principle it=E2= =80=99s not so automatic to see that a given proof is one of the good two, = but in practice it=E2=80=99d be hard to give a bad one accidentally.=C2=A0 = By contrast, put two people in two separate rooms and there=E2=80=99s a goo= d chance they=E2=80=99ll produce the two different good proofs (ie the cloc= kwise proof and the counterclockwise proof).=C2=A0 Best,

Noah

On Mon, Mar 8, 2021 at 10:15 AM K= ristina Sojakova <sojakov= a.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.<= br> >
> Dan
>
>
> Definition horizontal_vertical {A : Type} {x : A} {p q : x =3D x} (h := p =3D 1) (k : 1 =3D q)
>=C2=A0 =C2=A0 : h @ k =3D (concat_p1 p)^ @ (h @@ k) @ (concat_1p q). > Proof.
>=C2=A0 =C2=A0 by induction k; revert p h; rapply paths_ind_r.
> Defined.
>
> Definition horizontal_vertical' {A : Type} {x : A} {p q : x =3D x}= (h : p =3D 1) (k : 1 =3D q)
>=C2=A0 =C2=A0 : h @ k =3D (concat_1p p)^ @ (k @@ h) @ (concat_p1 q). > Proof.
>=C2=A0 =C2=A0 by induction k; revert p h; rapply paths_ind_r.
> Defined.
>
> Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 =3D 1 :>= (x =3D x)) : h @ k =3D k @ h
>=C2=A0 =C2=A0 :=3D (horizontal_vertical h k) @ (horizontal_vertical'= ; k h)^.
>
>
>
> On Mar=C2=A0 8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> = wrote:
>
>> Dear all,
>>
>> I formalized my proof of syllepsis in Coq:
>> htt= ps://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/S= yllepsis.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:
>>
>>=C2=A0 =C2=A0 =C2=A0 The generator of \pi_4(S^3) is the image of th= e generator of \pi_3
>>=C2=A0 =C2=A0 =C2=A0 (S^2) under stabilization.=C2=A0 This is just = the surjective the part
>>=C2=A0 =C2=A0 =C2=A0 of Freudenthal.=C2=A0 So to see that this gene= rator has order dividing
>>=C2=A0 =C2=A0 =C2=A0 2 one needs exactly two things: the syllepsis,= and my follow-up
>>=C2=A0 =C2=A0 =C2=A0 question about EH giving the generator of \pi_= 3(S^2).=C2=A0 This is why
>>=C2=A0 =C2=A0 =C2=A0 I asked the follow-up question.
>>
>>=C2=A0 =C2=A0 =C2=A0 Note that putting formalization aside, that EH= gives the generator
>>=C2=A0 =C2=A0 =C2=A0 of \pi_4(S^3) and the syllepsis the proof that= it has order 2, are
>>=C2=A0 =C2=A0 =C2=A0 well-known among mathematicians via framed bor= dism theory (already
>>=C2=A0 =C2=A0 =C2=A0 Pontryagin knew these two facts almost a hundr= ed years ago).=C2=A0 So
>>=C2=A0 =C2=A0 =C2=A0 informally it=E2=80=99s clear to mathematician= s that the syllepsis shows
>>=C2=A0 =C2=A0 =C2=A0 this number is 1 or 2.=C2=A0 Formalizing this = well-known result remains
>>=C2=A0 =C2=A0 =C2=A0 an interesting question of course.
>>
>>=C2=A0 =C2=A0 =C2=A0 Best,
>>
>>=C2=A0 =C2=A0 =C2=A0 Noah
>>
>>=C2=A0 =C2=A0 =C2=A0 On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke &l= t;e.m.rijke@gmail.= com>
>>=C2=A0 =C2=A0 =C2=A0 wrote:
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Dear Noah,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 I don't think that your clai= m that syllepsis gives a proof
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 that Brunerie's number is 1 = or 2 is accurate. Syllepsis gives
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 you that a certain element of pi= _4(S^3) has order 1 or 2, but
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 it is an entirely different matt= er to show that this element
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 generates the group. There could= be many elements of order 2.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Best wishes,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Egbert
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 On Mon, Mar 8, 2021 at 9:44 AM E= gbert Rijke
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 <e.m.rijke@gmail.com> wrote:
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Hi Kristina,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 I've been on i= t already, because I was in that talk, and
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 while my formaliza= tion isn't yet finished, I do have all
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 the pseudocode alr= eady.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Best wishes,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Egbert
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 On Sun, Mar 7, 202= 1 at 7:00 PM Noah Snyder
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 <nsnyder@gmail.com> wrote: >>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 On t= he subject of formalization and the syllepsis, has
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 it e= ver been formalized that Eckman-Hilton gives the
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 gene= rator of \pi_3(S^2)?=C2=A0 That is, we can build a
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 3-lo= op for S^2 by refl_refl_base --> surf \circ surf^
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 {-1}= --EH--> surf^{-1} \circ surf -->=C2=A0 refl_refl_base,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 and = we want to show that under the equivalence \pi_3
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 (S^2= ) --> Z constructed in the book that this 3-loop
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 maps= to \pm 1 (which sign you end up getting will
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 depe= nd on conventions).
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Ther= e's another explicit way to construct a generating
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 a 3-= loop on S^2, namely refl_refl_base --> surf \circ
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 surf= \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 refl= --> surf \circ surf \circ surf^-1 \circ surf^-1 -
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 ->= ; refl_refl_base, where I've suppressed a lot of
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 asso= ciators and other details.=C2=A0 One could also ask
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 whet= her this generator is the same as the one in my
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 firs= t paragraph.=C2=A0 This should be of comparable
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 diff= iculty to the syllepsis (perhaps easier), but is
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 anot= her good example of something that's "easy" with
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 stri= ng diagrams but a lot of work to translate into
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 form= alized HoTT.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Best= ,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Noah=
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 On F= ri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 <= sojakova.k= ristina@gmail.com> wrote:
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Dear all,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Ali told me that apparently the following problem
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 could be of interest
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 to some people
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 (https://www.youtube.com/watc= h?v=3DTSCggv_YE7M&t=3D4350s):
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Given two higher paths p, q : 1_x =3D 1_x,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Eckmann-Hilton gives us a path
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 EH(p,q) : p @ =3D q @ p. Show that EH(p,q) @ EH(q,p)
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =3D 1_{p@q=3Dq_p}.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 I just established the above in HoTT and am
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 thinking of formalizing it,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 unless someone already did it.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Thanks,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Kristina
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 --
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 You received this message because you are
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 subscribed to the Google Groups "Homotopy Type
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Theory" group.
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 To unsubscribe from this group and stop receiving
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 emails from it, send an email to
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 HomotopyTypeTheory+unsubscribe@googlegroups.com.=
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 To view this discussion on the web visit
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7= 588-0516-591f-94ad920e1559%40gmail.com.
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 -- >>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 You = received this message because you are subscribed
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 to t= he Google Groups "Homotopy Type Theory" group.
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 To u= nsubscribe from this group and stop receiving
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 emai= ls from it, send an email to
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 To v= iew this discussion on the web visit
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 https://groups.google.com/d/msgid/HomotopyTypeTheory/C= AO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.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://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 &= 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:/= /groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg6s-UAfQ5_i8f49hTHzfEk-= _%2Bzp4C_bnFFvi9Ecnx%2BZEg%40mail.gmail.com.
--0000000000008172b805bd080565--