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 19288 invoked from network); 8 Mar 2021 15:36:11 -0000 Received: from mail-vk1-xa3a.google.com (2607:f8b0:4864:20::a3a) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 15:36:11 -0000 Received: by mail-vk1-xa3a.google.com with SMTP id k198sf736217vke.12 for ; Mon, 08 Mar 2021 07:36:10 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615217768; cv=pass; d=google.com; s=arc-20160816; b=oIF/8xqieJ2u164dppKw8FbacQ05LqTiXuyvB4TQGVP+RkV3r9I3Vk/ud1cP9/iToa ae0AsPUxFX+qgg80EwRCIIY7n4BoRmIxTotHRQQhDFOdRISNt3GojZfDg48tBKoS5nMR DqJje5DUne748Ad8yqprCP0tnvAn1fSu1u1KlrWOwP4JoHNx2p3DNGACsXGMycNDtLwL NLqd/7npIoi56YLOs6VoLbY7PIVEPmkPMI+1yQuTyWaOjhWtAgTV0rJXgxZrXrYzLif8 kVmJGmFXQBMK4QInIPDIR3y9Ih9l7bTwfEXHhPbGbXTwY68PF7E3tewIRPZPx+QLqdB0 RmMQ== 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=KjKOwtWXHIbw8Ri5k6NPX3dlHzZhLdAvsXx7aXP6ySc=; b=paVCa3eE7jwH6peAszFrbRENA4x5+NP89TcEMv3l2yZO/tjEMGSr6wuq21Pi0iQ3Dt a2CEhx90B4ZDwXYePsFXcOu0yoRuOWwZxR2sNRn6GopxqB89PEcYjJ6tHfpVvWu2fTS1 HnEyoMjWteXS6saBbEKNH/cHMOyRM3rcFLfqvgYH+q6M+TSa0tsPvqpieb20cvBk702N 6QEzp+6dZDXPWAIVrbXEgqMQgjrko2WiceMRGlK0gbjYGLniK/FQkwtVTrhkZE7jLLMt wyEgjodSONA2tZbeO7XY1/NLyVjia5FSPuXiqGE033e8yKYrpWVN4j6eH7gsCNcZv206 +XVw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=djFpKip5; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::a29 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=KjKOwtWXHIbw8Ri5k6NPX3dlHzZhLdAvsXx7aXP6ySc=; b=hDmD+qnyY2mCG+4xo6ajHbraKGiIwcMYQLXNxTriWMx8YdQNoFDWlgsFmmXjzjIiRU cZT/n+nYoM84o8av7I6kY85Y5SAk7miRfT9PhPiCZybGEIc6p7qFAMJNcPSMm6AF9Pq4 yWPiAO8BzEljwCivHNgEnQJsUhvVzFLSMHRcXizonQtd7/4joBAIXP/8Xi2GMBMUFJE1 HsbZvIg08EcQV62hTSQcIf5H04qCsvbLEyG1OmbKR5zVOQ3gThX0seGHEGL1X2GYVXzM uvKIYyucuxuKblPsYfJj1xHg4HqFY8HAZbT3EIFMUo4z5UevbEu8xTfzlQXV3ny5eK08 biVw== 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=KjKOwtWXHIbw8Ri5k6NPX3dlHzZhLdAvsXx7aXP6ySc=; b=rLaOrOJBm5Q9gENE9gs222K+22koTf9HN71joeXUY/9AIkIq02V534y17/Vlf3g35B jYn9AInIJnDoP/FT4U+tLlWpWPBmNHniy6+aWQWdJnoPdyETSRAfgrLY+Me5LOPmwFgL JRm4RMx3HVr9+UhED/YDdNsOy0AUR8+H8xyencOGKpkGLO5PgXtWvGTNI5LOfFFmxlJK P9GDvrfyavvEvS5mkxdqRE58h4zK4/PhMqShZhOi+DN4OODai5sca0iV9zaLu8NwVn5C tfFCi5MH9a/UvuCxoI2oSzpvzsHgtlMsVXvICmNqmj51POdG1ItwqyolrgpBQKmOgRzE Cetg== 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=KjKOwtWXHIbw8Ri5k6NPX3dlHzZhLdAvsXx7aXP6ySc=; b=M9LiSVJoyC5FQxtf8yzBjtdpq2+NXHg5rdglFguth9DOmvdH8IOTlrQxO56TBtDhXq B+IcAkR5DI7sVo9ZgXp9kV2Buq7FMLINTbS79ANfvzOjkReXgy8HFh9Qg0MMAVxl6T74 51c/ywJbSwXpUKiS94izHudma8ieARQT2/ENqshN1fQqQzJrqbWDB79M28Uk/yn8Ym64 ugEstzquOXdVt/Dbl872vKRDl0Xvt6TBIP78L1Gn5w0m3eloRa8KNEIpGE8l0TJkB/Tw NqW1UuiC3RL++7ClSFNUvfzB45j/XJrFioU+D9h03X6kt8GwxOTzOxcPb0uiVH7r21j4 g7kw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5322naCbRAl6fft8xJk3VIsK9KLWGOh7lUKDCcVc/Bgh4lpUs2aV 6/E2XQYKz5GBTBbCLwNTNRg= X-Google-Smtp-Source: ABdhPJxzNX6arCqElc1fB6i62pvpFXkM5k3adMcZq3fFkBMEfSwoF6TAp3CoMsrO1A/f9TT7fpgbPQ== X-Received: by 2002:a67:2f93:: with SMTP id v141mr13056366vsv.6.1615217768294; Mon, 08 Mar 2021 07:36:08 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:e88d:: with SMTP id x13ls2125855vsn.11.gmail; Mon, 08 Mar 2021 07:36:07 -0800 (PST) X-Received: by 2002:a05:6102:ed4:: with SMTP id m20mr12792743vst.13.1615217767683; Mon, 08 Mar 2021 07:36:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615217767; cv=none; d=google.com; s=arc-20160816; b=iomSYzaD7Mm006s+fhhU3qScgasXYH7DoV5zwh+3ioi/ZsBv61CgisiWeSEzDJVEle kpfMSSKTFV7EUDwJAQRKxArLCxErnBQF0HL6Sg0akagCB4xD4jSqeoHZrSEEVzOE70qF RDngWuhz7FMSY4u4UD4eiGD+1V0nPwjMSnrpxyTXBwwi0tmugkS1sDAg9zc75MVTM2ao F0wPcWwwB2K/KFgLLDdfB50Yol759oszLCwmHTGwY3QK3DJtIffEUiPgl9gxeAC18Ri6 QBdnOxS/Z5aC1PHe6pTyy+KkYKwIutLhsa00lgfaQ+O0qagzEHVPZ2BXHUMl6dfdkS6Z TTNg== 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=QMPuSOHAbB3opbSkdjjgxwB6iNJ8lWLwkge7lKoQA3s=; b=o0Cq7n0AHh2MvDP2vPO1G1Hdh8HYLj4b1xKTZwq/KfRUy9pxN6yRVS8PYN6Vrug9Aa U0N/Tpk7XqzZ6zzp9t3GiN23cHfNDWOZUSoenBPQr6qzL3TwEUPon5yheHqqaYoFfEAV z5Jet+Hd00QCr3TPpVESIWNgtmK1k35aDw8ChzgHGYB7iqARrEehC6bv/fYSsYMiXHsB uTgiWHbZdHReDH4v/r7KrqfIzhp82DhKTH9PTxTFynESTSZDO0f48D9PDgF9DwaHaGVi uQi4/HfMHDOyG19z7EpeoekCE8EQRuti4Hdv3Onm456W2uZ43ysSW17XWAkPWQCBrNmJ hodg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=djFpKip5; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::a29 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vk1-xa29.google.com (mail-vk1-xa29.google.com. [2607:f8b0:4864:20::a29]) by gmr-mx.google.com with ESMTPS id l11si400920vkr.5.2021.03.08.07.36.07 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 07:36:07 -0800 (PST) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::a29 as permitted sender) client-ip=2607:f8b0:4864:20::a29; Received: by mail-vk1-xa29.google.com with SMTP id q17so2235123vkd.3 for ; Mon, 08 Mar 2021 07:36:07 -0800 (PST) X-Received: by 2002:a1f:9d43:: with SMTP id g64mr13775743vke.16.1615217767257; Mon, 08 Mar 2021 07:36:07 -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: Noah Snyder Date: Mon, 8 Mar 2021 10:35:55 -0500 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Kristina Sojakova Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000004098ee05bd083175" 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=djFpKip5; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::a29 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: , --0000000000004098ee05bd083175 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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 o= r > 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). 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 giv= e 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 g= ood 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/Coli= mits/Syllepsis.v >> >> >> >> >> >> I am looking forward to see how it compares to the argument Egbert ha= s >> >> 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 dividin= g >> >> 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 w= hy >> >> I asked the follow-up question. >> >> >> >> Note that putting formalization aside, that EH gives the generat= or >> >> of \pi_4(S^3) and the syllepsis the proof that it has order 2, a= re >> >> well-known among mathematicians via framed bordism theory (alrea= dy >> >> Pontryagin knew these two facts almost a hundred years ago). So >> >> informally it=E2=80=99s clear to mathematicians that the sylleps= is shows >> >> this number is 1 or 2. Formalizing this well-known result remai= ns >> >> 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 give= s >> >> you that a certain element of pi_4(S^3) has order 1 or 2, bu= t >> >> 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, h= as >> >> 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_bas= e, >> >> 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 generati= ng >> >> a 3-loop on S^2, namely refl_refl_base --> surf \cir= c >> >> surf \circ \surf^-1 \circ surf^-1 --EH whiskered ref= l >> >> 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 proble= m >> >> 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 receivin= g >> >> 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/CAO0tDg7MCVQWLfSf13= PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com >> . >> >> -- >> 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/1f7bbcb8-ee50-0c24-= 174e-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/CAO0tDg6MCr7skausPPmomQrswRk1umaq3_V%3D52z60vxMj-hraQ%40= mail.gmail.com. --0000000000004098ee05bd083175 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
My funny remark is slightly inaccurate. =C2=A0\pi_3(S^2) j= ust classifies proofs of EH where both 2-loops are the same as each other.= =C2=A0 It is true that there's also a Z-worth of proofs of EH in the ge= neral case, but this is a subtler fact about \pi_3(S^2 \wedge S^2).=C2=A0 N= onetheless =C2=A0the point remains that any two reasonable proofs of EH wil= l be equal or inverse to each other.=C2=A0 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) =3D Z exactly tells you th= at any proof of Eckman-Hilton is given by repeatedly applying either the st= andard 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 cont= rast, put two people in two separate rooms and there=E2=80=99s a good chanc= e they=E2=80=99ll produce the two different good proofs (ie the clockwise p= roof and the counterclockwise proof).=C2=A0 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.<= 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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg6MCr7skausPPmomQrswRk1um= aq3_V%3D52z60vxMj-hraQ%40mail.gmail.com.
--0000000000004098ee05bd083175--