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, NICE_REPLY_A,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 11177 invoked from network); 8 Mar 2021 14:31:17 -0000 Received: from mail-lf1-x139.google.com (2a00:1450:4864:20::139) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 14:31:17 -0000 Received: by mail-lf1-x139.google.com with SMTP id p12sf3405528lfu.7 for ; Mon, 08 Mar 2021 06:31:17 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615213877; cv=pass; d=google.com; s=arc-20160816; b=qLxioWOJ0huRyENYhmmSOiI3/KQZQ6zP9NyZ4fRUjvHRW62Bch9w1rKiGMSV7giZgD zid/a3ciUYy5rFotholmT7P/sM73UO8sVXA2OJ82ub45fjtbB0XcDJkAQvV6YjaeK+XI bqGIks0wmymiZa8Vzl01vuJY3Cip0NdhLxAEN5Ngdxf6fcC+C4HKt8J3R+UIsP4EUx7I trbjRz5fqhFb1g2c1/PrQoxe+X9pn5we3T4DEMw99bYIUe2hJdUXjo3nQHZkhmTvsD4r qcmPFCYH9Xxg3VUGWr2az9G4XyfVQewzlKZRBjmPlxGLDpcSVqreGf7DVbsJ3r/FtvLT wYJw== 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:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature:dkim-signature; bh=RsyEzwxiG5QFQ+LLmqKY9abUdYwFuElP1s2ug0Y3DDk=; b=SZwemtgJgfpKPOFMNhgNFg5GVIXyiMSYtRt4qKNSexr1+qo65zri/VouH9YXKUePhT 0CIOiq9hHRVToj5BlZllafsdL/8skNzeA/+HsedwQKTBpQQ46KGTLLn7TCruIdfuJcKd UIInBL4eHDCBhpxcyNvraCRqFCxuDpKc6SQu7kRqVfvMMv7uG2RE06W2ymIwwTMytOUw ziRi+uKCSdrNiVrbroz12jLjC1GJURswDESPIIzpvEisx6ZUJvsS/y4bSd5R8JwaceLY 0k+T2F7L63VXlztE1DbLutWfcBytQlbtr/nZ1UZdSVgDmVVSUaDky9DefBVbvNgmjijN ZchA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=huPDXBeU; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=sojakova.kristina@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:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=RsyEzwxiG5QFQ+LLmqKY9abUdYwFuElP1s2ug0Y3DDk=; b=WZG2PdUmypb3XzepaS/mxW8hGTTft3r+nZvPkNhPhYI/6L/qJUA4dSridhv3VwcfSP XovHFkvhSJ1ZKMtcdL+824wlArm8nbcj4eepGK0+v3yN8TM0pxZtMknNGDzXl9oWBsxg cRRoTFG/uVPmLoojEC6qebHmwSdMFmpH5f03/KCqLQ0e3jyshi4V5FlWODAg+/LKkwsJ O5RKMpPHnlbU8U5QtAop0ujYZpCIDcFhI3o6ZgWN1yWOk1csELHv6yc3sqpA5tIE7do1 ZdS7/+HxPga/ekk1QyNsUktZsQyCB33f/zltN2Zm+7ovjmaeHgNgRyfhZQ8QM8nHs0uq SpKw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=RsyEzwxiG5QFQ+LLmqKY9abUdYwFuElP1s2ug0Y3DDk=; b=VFEH+lIkPqOFYZB5nNDo1AXsW43gV3WO3K0kgx2ttXoEtabU71jAqdX9BWUSiFHuB6 4p55fnUycH5il+ujdzf3aMBbHk8XkCQQ/rRmiYVAFOKAUk7/USkCcrHh8HE5Nb/Uk5Jd 9Amlba2PAwfCbHRVLshYb66CUQLLX8fBZ+wP/zTXAFhvUMeiHcsH0fJh710R7asP19vz GA0gHGV5RrDQTueaWFbAoZthoZhnc2U/9x1JPYJcBjeV1GtIucyhXu0Oc/uC5b66plQ2 WwLxSKFhG7XxfalotHtS72VvHAPMUEJukHC5MepSyG99hvqTsb7D5n+IvOJN1XtgWo5O C0IQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :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=RsyEzwxiG5QFQ+LLmqKY9abUdYwFuElP1s2ug0Y3DDk=; b=ol9I0md3/CwURCN8kwRIoJmVzA3e7z403gtvdWUGVDegUOUgSM8/mhT7b09b7W7Lsh rBtqukRH2UkiOPMjLxbfZ0LON78JBLwPc/cHqCyol8JGrLIKZUqdIouf8TreCcEW1VMS NaCXY9hasKqVPTg8/Sc4drW97kkmjrlq/+5P7JU9O8aeZGcoWtA+WhNdtdzBKOybTfFP jP4SkxrgNtZsm+wY3z6R92y2VUXBXipGlZRLESXmpbzFLIPV6WGJPq7nSD+b96ecP9Bs vfTNtgUYv0Dt4BkV9KDIJz83GvEqCguCPUkyACW0VNVjJTQFBF7tAsuRhgYPg/nrxOD6 SGTQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532+2NBL9BuOjTMvJ7U2IeH7OPL6TazISQt/PyurBcMUhURnWiQ8 g2bcHS/k652/s43oMiUVfYQ= X-Google-Smtp-Source: ABdhPJy15z36AurnHikSLwxNybqPDKpmLytSNvgaEytg/MxpNSHBC1NbiFwvdGdH4LpcAs59gYk6sQ== X-Received: by 2002:ac2:5970:: with SMTP id h16mr14325301lfp.108.1615213876815; Mon, 08 Mar 2021 06:31:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:b603:: with SMTP id r3ls3490177ljn.5.gmail; Mon, 08 Mar 2021 06:31:15 -0800 (PST) X-Received: by 2002:a2e:9c8e:: with SMTP id x14mr14260529lji.312.1615213875588; Mon, 08 Mar 2021 06:31:15 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615213875; cv=none; d=google.com; s=arc-20160816; b=tsGEeFrxwRBSHGR6CH9R9bsJObTMpFCT+E6DEGC3ou6qNVLJ05m7Zb3a9KAYurcSPm ONLCzNC6eRjHQJu6XpRS6MnEp7/jAP2kvSSMYY13OxHVtiaoB/jlrZSR7TzXGvJKZG/3 0qb6ZLY7mqNlGu20ZxJLUZ81WH05rJwaV/RhFTEeZ5ZKZPDdZXnMpFsaLjWIfwfmK0st x+cAYtz+oBuLrenA2utEdUJ7enGiC3Bz+O0eojmipU18LkAgGOOaPNaOlfHBc5EqHCwW xgXW515ntOrXQDrBEZCWpZkZEkB0zNEN+i7ZCNSK71rze2Vfnhg0KnfHtn++z/mcPEPU Jb1Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:to:subject:dkim-signature; bh=Jb4QmM7h2S54PkbRULtZCH/8ibduT1u/8B0wKa3Ut+s=; b=APm1SVfedG79xd+Ct95MFpwBHTonhbYDKcjoS/AE+cG36U+hCFbQ0OC2oJZt0JYgjX a1d5z8+XbqIy188k/gaqw3DsA2X1kgHm1zcS0GVx2wvD1Vkoc7W7xjow5N0UIoLrtmqB Dm8L8aaxaFfxI69WIYTmwkaHEK52D9xERpRMWEwvdV774yZFdjcPsELNNWuuOELZ5izW C5xttGj+cdbgdiBko5MYeOmeex2jxwJwuTNHu6F4lrSLposQJRdWqHB7it1rOLMifIoR Cl3NgVMmiF4tElPfZQxRCgkEBlZf5PYhNZPi2VjuPZr7cNqw2rpan/y4Y+6Iz/nju6XU q0bg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=huPDXBeU; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32a.google.com (mail-wm1-x32a.google.com. [2a00:1450:4864:20::32a]) by gmr-mx.google.com with ESMTPS id b27si342028ljf.6.2021.03.08.06.31.15 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 06:31:15 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) client-ip=2a00:1450:4864:20::32a; Received: by mail-wm1-x32a.google.com with SMTP id y124-20020a1c32820000b029010c93864955so3933982wmy.5 for ; Mon, 08 Mar 2021 06:31:15 -0800 (PST) X-Received: by 2002:a7b:c759:: with SMTP id w25mr19463737wmk.139.1615213874672; Mon, 08 Mar 2021 06:31:14 -0800 (PST) Received: from ?IPv6:2001:861:3cc3:38e0:10a:8a77:7d4c:e344? ([2001:861:3cc3:38e0:10a:8a77:7d4c:e344]) by smtp.gmail.com with ESMTPSA id a8sm14800738wmm.46.2021.03.08.06.31.13 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 06:31:14 -0800 (PST) Subject: Re: [HoTT] Syllepsis in HoTT To: homotopytypetheory@googlegroups.com References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> From: Kristina Sojakova Message-ID: <7d4b6fd7-3035-e0b9-c966-97dd89d8b457@gmail.com> Date: Mon, 8 Mar 2021 15:31:13 +0100 User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.8.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/alternative; boundary="------------0A457A4B96851B0A10E6E854" Content-Language: en-US X-Original-Sender: sojakova.kristina@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=huPDXBeU; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=sojakova.kristina@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: , This is a multi-part message in MIME format. --------------0A457A4B96851B0A10E6E854 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Dear all, I formalized my proof of syllepsis in Coq:=20 https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimit= s/Syllepsis.v I am looking forward to see how it compares to the argument Egbert has=20 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=20 > \pi_3(S^2) under stabilization.=C2=A0 This is just the surjective the par= t=20 > of Freudenthal.=C2=A0 So to see that this generator has order dividing 2= =20 > one needs exactly two things: the syllepsis, and my follow-up question=20 > about EH giving the generator of \pi_3(S^2).=C2=A0 This is why I asked th= e=20 > follow-up question. > > Note that putting formalization aside, that EH gives the generator of=20 > \pi_4(S^3) and the syllepsis the proof that it has order 2, are=20 > well-known among mathematicians via framed bordism theory (already=20 > Pontryagin knew these two facts almost a hundred years ago).=C2=A0 So=20 > informally it=E2=80=99s clear to mathematicians that the syllepsis shows = this=20 > number is 1 or 2. Formalizing this well-known result remains an=20 > 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, has it > ever been formalized that Eckman-Hilton gives the > generator of \pi_3(S^2)? That is, we can build a 3-loop > for S^2 by refl_refl_base --> surf \circ surf^{-1} --EH--> > surf^{-1} \circ surf --> =C2=A0refl_refl_base, and we want to > show that under the equivalence \pi_3(S^2) --> Z > constructed in the book that this 3-loop maps to \pm 1 > (which sign you end up getting will depend on conventions). > > There's another explicit way to construct a generating a > 3-loop on S^2, namely refl_refl_base --> surf \circ surf > \circ \surf^-1 \circ surf^-1 --EH whiskered refl refl--> > surf \circ surf \circ surf^-1 \circ surf^-1 --> > refl_refl_base, where I've suppressed=C2=A0a lot of associato= rs > and other details.=C2=A0 One could also ask whether this > generator is the same as the one in my first paragraph.=C2=A0 > 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 > > --=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 email to > HomotopyTypeTheory+unsubscribe@googlegroups.com > . > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0= d354-7588-0516-591f-94ad920e1559%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 email to > HomotopyTypeTheory+unsubscribe@googlegroups.com > . > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7= MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%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/7d4b6fd7-3035-e0b9-c966-97dd89d8b457%40gmail.com. --------------0A457A4B96851B0A10E6E854 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Dear all,

I formalized my proof of syllepsis in Coq: https://github.co= m/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/Syllepsis.v=

I am looking forward to see how it compares to the argument Egbert has been working on.

Best,

Kristina

On 3/8/2021 2:38 PM, Noah Snyder wrote:<= br>
The generator of \pi_4(S^3) is the image of the generator of \pi_3(S^2) under stabilization.=C2=A0 This is just the surjective the part of Freudenthal.=C2=A0 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).=C2=A0 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).=C2=A0 So informally it=E2=80=99s clear= to mathematicians that the syllepsis shows this number is 1 or 2.=C2= =A0 Formalizing this well-known result remains an interesting question of course.

Best,

Noah=C2=A0


On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke <e.m.rijke@gmail.com> wrote:
Dear Noah,

I don't think that your claim that syllepsis gives a proof that Brunerie's number is 1 or 2 is accurate. Syllepsis gives you that a certain element of pi_4(S^3) has order 1 or 2, but it is an entirely different matter to show that this element generates the group. There could be many elements of order 2.

Best wishes,
Egbert

On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke <e.m.rijke@gmail.com> wrote:
Hi Kristina,

I've been on it already, because I was in that talk, and while my formalization isn't yet finished, I do have all the pseudocode already.

Best wishes,
Egbert

On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder <nsnyder@gmail.com> wrote:
On the subject of formalization and the syllepsis, has it ever been formalized that Eckman-Hilton gives the generator of \pi_3(S^2)?=C2= =A0 That is, we can build a 3-loop for S^2 by refl_refl_base --> surf \circ surf^{-1} --EH--> surf^{-1} \circ surf --> =C2=A0refl_refl_base, and we want to show that under the equivalence \pi_3(S^2) --> Z constructed in the book that this 3-loop maps to \pm 1 (which sign you end up getting will depend on conventions).

There's another explicit way to construct a generating a 3-loop on S^2, namely refl_refl_base --> surf \circ surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl refl--> surf \circ surf \circ surf^-1 \circ surf^-1 --> refl_refl_base, where I've suppressed=C2=A0a lot of associators and other details.=C2=A0 One could also ask whether this generator is the same as the one in my first paragraph.=C2=A0 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 <sojako= va.kristina@gmail.com> wrote:
Dear all,

Ali told me that apparently the following problem could be of interest
to some people (https://www.youtube.com/= watch?v=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 Homoto= pyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.c= om.
--
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 HomotopyTy= peTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://gr= oups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7MCVQWLfSf13PvEu%2BUv1mP2= A%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/msg= id/HomotopyTypeTheory/7d4b6fd7-3035-e0b9-c966-97dd89d8b457%40gmail.com.=
--------------0A457A4B96851B0A10E6E854--