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 20702 invoked from network); 8 Mar 2021 15:46:43 -0000 Received: from mail-ot1-x33c.google.com (2607:f8b0:4864:20::33c) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 15:46:43 -0000 Received: by mail-ot1-x33c.google.com with SMTP id m22sf7414835otn.4 for ; Mon, 08 Mar 2021 07:46:43 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615218401; cv=pass; d=google.com; s=arc-20160816; b=PXnEsL1930XRUDgIuVnPmqyu0ffCnoWbguW0VaiPP5QY+lByQ6CZQ+RVjoQV6vi1cn lUmByWJACpyamjMW+S4lWyDumN7O5TI69H7j4TmP21J/F1sD0J13XFVZua6xA3R9aTRa Zb/2pT70kPr5v3EBFqQxGdx+kXJLnb1v2TIFdJA4KOomurCfjh68CQqxsk+AsbSvDFpA BdJpwv72qzU/Jj4VG8F1zqkPtd1VRd9raiJ3lhe5iuLgcBZ5GRCQFJn0EDC/QqH6xSQH NLnR6X576JyTIh5xbhgA2+7E+tW/EBt7j60Kf/BsjEVvHdxEqSQofaf52vAJ4JbDD26T GcUA== 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=PRw4Bnxwa6rnlBTIT7tSE0rhhsJ3X67X7zD9NXMK9T4=; b=e4lzE/zVJ917bh1r7pMbHz9r2MmF6TV0XqGV89ap8G3yf2T8/43GUoXj0QECXXa09c PzNJG55HQJslVZ/m65de9IVYPGix/352IKGh6PCFvxWCEthjeQ3J4JnWFkkDp8ic1G8p VUNVhrqa9Xk1aULp7UoVmDlvdqohiiiRXip5ZZycBwUj7zNXmpmkDtsX6gKBV5bhc5VH OOHtOoPqkQklOBNhfORmCajmv5JPYMzbRWYBNUbtVAxnrzAxijG3jrW4/nOXvQGMQVEf HpkQQa7RHLFVW82Vszw7cydwNi8mB9inPL7NbC4ilgev00xoFF+OAEZZdZgVc/SuSXp+ h1yg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bSVeTan6; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a33 as permitted sender) smtp.mailfrom=e.m.rijke@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=PRw4Bnxwa6rnlBTIT7tSE0rhhsJ3X67X7zD9NXMK9T4=; b=dY4eG59wp71mC9hFRzM7pHvgpaBlzA4D/vHg3nyhaztiLGZ5LaJSn8NwMzqe9TzZT6 /yStnYLBkV2M0GcJk2rH27kmRS/hxT+x3g+yEg3y02ivpYdpGSYdDkkzJjoos4sfYkNs a/uejnoegykLCCtZggKwV9Ln427ZmebVH+0essl60MzDBDSKdebkMQscIONvm0okloNf dWYMedW659eL6tISw4IMb9IaUJiXWTcooXl2JX3wORssWSxEaOwna+r4TTRsHKc3Uh4G ll0yxUL18vBCLUNDhtAOVdWfct47atGFI8NhHtyWdr9qSuvXi/h+0vlGlc7rM6ojJ4pU fyLQ== 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=PRw4Bnxwa6rnlBTIT7tSE0rhhsJ3X67X7zD9NXMK9T4=; b=b1TIWqMiqQM+Bqp57K4OJK3X5lOdPGJP+Rmzm3oiHzPaoWosF9oIY9ly1/GAvWdCEz PhnNdsWRTFCMn+LdXUDiGNm3nkUQCMGq4U935JaE9ma6nHRewNm+TRlaq4kE5zquDeJ+ r4kqXtflCJfA55nL3Zi4HdXIv3LK3Hhb3zqca8TSy9iUdhRMFgx5aEHy5tsKgBJlxTNC hdUvVoUdNS/jpsynIxzUwS+iyKgDpBjKTtzOnC0a37BBz0XpyNpS6UGJDiovXKfVOOhC VN2KxgLuRI8FdfkJu88waVOzRm6PI9720oeLxIIAEySKrZy9McZWedgSWhJnae2OZnQM yoTw== 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=PRw4Bnxwa6rnlBTIT7tSE0rhhsJ3X67X7zD9NXMK9T4=; b=kj6O5NsY/TowR7se/DAHZqARRmP6I2crTFCN2xC3I0dC4i17Ls0oEGX2MkcsE07/Av n9rhSigKBGBBSRyPpJjWYzYL/GNRvYJg5VsqVvOwworRi/VuH7+Kw9zkHsOHnC0y1uyP YxAbpbsycnymCqSi5+KMfqDcw9E2ndzRrqsUJJ1ZWJiawOliVp7bGW2Bbd/VvxjX/PBd KTxiwIsX6ZQbsEbhqsOseQqFCzdQzLrfuURNhwAIqXZBYAYdo0Y5/0Qy74XXs9O70idy PJF+vl5r+Zc+E9LPHQDNEB5+F2LFNjMpgeVjthclMYrtCOCVy6OIae1UwhVufLimeF9x A8fA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5330SchcbicgROPcSRaZdVs776qqLT610Mg9kuQI9hcsJp4Q25ym swvQVI9SAKiUakt0WL81HOg= X-Google-Smtp-Source: ABdhPJz+LqOdXpL6eJZx3heLrD3xyA1AcjyBO2KdwAbArEqsEtNVP8IC4MGwpomx/NGnozlP6hImDw== X-Received: by 2002:a05:6808:687:: with SMTP id k7mr18265461oig.140.1615218401793; Mon, 08 Mar 2021 07:46:41 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:b303:: with SMTP id c3ls3323714oif.11.gmail; Mon, 08 Mar 2021 07:46:41 -0800 (PST) X-Received: by 2002:aca:ab09:: with SMTP id u9mr17384161oie.153.1615218401381; Mon, 08 Mar 2021 07:46:41 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615218401; cv=none; d=google.com; s=arc-20160816; b=Gqq1Bj0WgOIivp9YIdLzgrPej4ch9V2YdSFBo8zv7MBD3cdt1C0NTbdJLvx8mU3SiX K89c3bwT/4C/0DeSaaxkBmxLKMmjuXWcCZ3aIGNqVqrkwDaKw1R44bqPZGvJ6+ZhbU+O G5i9u28r6xl4wrnvrSBpjr+OeoHbg+vjmLpJ3u7ynapbT3Bht6YjFnw9X2JxuMyxpxEg L+Bm8xhTCXBUFbtLaP6sBi2RulIdLfUs6mLH8W8KwFpR8b48KyBlUIe96xjGuCgQQVjf m9MFpY8S/aeObBb/GdddUZcvW00jokLpo4O/U9wGD2EsMq62AH/2/FVJbp+Nb9Dui0Hf +mzg== 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=YCPQRK/fKWGCjaTYtoglVBx9DugLcG3mQmE1k7MTiXc=; b=1DmenDyiNpyDn7io4uhj4gJGH4Qb4+i7kPr8E3C/JPVPdKyC+ioRdCuUD+N+5udyEQ 5R9ChElvyKs6a26Pt/8j1+HYintVmH1k/XWnpx1IukH9JOyXOIZB41CanVEAV7rpTata dR+pLibzJRmpsGQyDj9fhbthMws3azn9Ya9C43jH8mc70DLJL/8GaITbmKlw4tDyPD5r cpVH2zFdWQ+BITPqSvDR6HepD/uGgoZrHwZazjABX41AtnKnJyl8q/twBwF5svXp4Z4R AuPvQoNE/Pq4Z0wa0hEg2p9au39Q3d8W/OSLHv7+McXVSFJoJn3d7TiSERHjo9F6k9n6 38XA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bSVeTan6; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a33 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vk1-xa33.google.com (mail-vk1-xa33.google.com. [2607:f8b0:4864:20::a33]) by gmr-mx.google.com with ESMTPS id c10si794468oiw.3.2021.03.08.07.46.41 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 07:46:41 -0800 (PST) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a33 as permitted sender) client-ip=2607:f8b0:4864:20::a33; Received: by mail-vk1-xa33.google.com with SMTP id 7so2246078vke.5 for ; Mon, 08 Mar 2021 07:46:41 -0800 (PST) X-Received: by 2002:a1f:9d8c:: with SMTP id g134mr13405565vke.20.1615218400698; Mon, 08 Mar 2021 07:46:40 -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: From: Egbert Rijke Date: Mon, 8 Mar 2021 16:46:29 +0100 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Noah Snyder Cc: Kristina Sojakova , Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000002240505bd085752" X-Original-Sender: E.M.Rijke@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=bSVeTan6; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a33 as permitted sender) smtp.mailfrom=e.m.rijke@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: , --00000000000002240505bd085752 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 wrote: > My funny remark is slightly inaccurate. \pi_3(S^2) just classifies proof= s > 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 wrote: > >> 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 (th= e standard one >> and it=E2=80=99s inverse). In principle it=E2=80=99s not so automatic t= o see that a given >> proof is one of the good two, but in practice it=E2=80=99d be hard to gi= ve 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 = 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 =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/Col= imits/Syllepsis.v >>> >> >>> >> >>> >> I am looking forward to see how it compares to the argument Egbert h= as >>> >> 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 par= t >>> >> of Freudenthal. So to see that this generator has order dividi= ng >>> >> 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). S= o >>> >> informally it=E2=80=99s clear to mathematicians that the syllep= sis 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 >> > >>> >> 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 giv= es >>> >> you that a certain element of pi_4(S^3) has order 1 or 2, b= ut >>> >> it is an entirely different matter to show that this elemen= t >>> >> 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, an= d >>> >> while my formalization isn't yet finished, I do have al= l >>> >> 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, >>> has >>> >> it ever been formalized that Eckman-Hilton gives th= e >>> >> generator of \pi_3(S^2)? That is, we can build a >>> >> 3-loop for S^2 by refl_refl_base --> surf \circ sur= f^ >>> >> {-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-loo= p >>> >> 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 \ci= rc >>> >> surf \circ \surf^-1 \circ surf^-1 --EH whiskered re= fl >>> >> 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 i= s >>> >> another good example of something that's "easy" wit= h >>> >> 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 probl= em >>> >> 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 receivi= ng >>> >> 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 subscribe= d >>> >> 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/CAO0tDg7MCVQWLfSf1= 3PvEu%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/CAO0tDg6MCr7skausPPm= omQrswRk1umaq3_V%3D52z60vxMj-hraQ%40mail.gmail.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/CAGqv1OAuHQwnZvvDfkM99o6Za%3DSrjPYO3J62MPMFxphDzVOiEw%40= mail.gmail.com. --00000000000002240505bd085752 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Congratulations, Kristina, on doing it so fast.

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

Best,
Egbert

<= div dir=3D"ltr" class=3D"gmail_attr">On Mon, Mar 8, 2021 at 4:36 PM Noah Sn= yder <nsnyder@gmail.com> wro= te:
My funny remark is slightly = inaccurate. =C2=A0\pi_3(S^2) just classifies proofs of EH where both 2-loop= s are the same as each other.=C2=A0 It is true that there's also a Z-wo= rth of proofs of EH in the general case, but this is a subtler fact about \= pi_3(S^2 \wedge S^2).=C2=A0 Nonetheless =C2=A0the point remains that any tw= o reasonable proofs of EH will be equal or inverse to each other.=C2=A0 Bes= t,

Noah

On Mon, Mar 8, 2021 at 10:23 AM Noah Snyder= <nsnyder@gmail.c= om> wrote:
One funny rem= ark, that \pi_3(S^2) =3D Z exactly tells you that any proof of Eckman-Hilto= n is given by repeatedly applying either the standard proof or its inverse.=

In a sense there are ex= actly 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 t= hat a given proof is one of the good two, but in practice it=E2=80=99d be h= ard to give a bad one accidentally.=C2=A0 By contrast, put two people in tw= o separate rooms and there=E2=80=99s a good chance they=E2=80=99ll produce = the two different good proofs (ie the clockwise proof and the counterclockw= ise proof).=C2=A0 Best,

= Noah

On Mon, Mar 8, 2021 at 10:15 AM Kristina Sojakova <sojakova.kristina@gmai= l.com> wrote:
Thanks Dan! I think we shoul= d 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/CAO0tDg6M= Cr7skausPPmomQrswRk1umaq3_V%3D52z60vxMj-hraQ%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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1OAuHQwnZvvDfkM99o6Za%3DSr= jPYO3J62MPMFxphDzVOiEw%40mail.gmail.com.
--00000000000002240505bd085752--