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 29327 invoked from network); 8 Mar 2021 16:54:58 -0000 Received: from mail-pg1-x53d.google.com (2607:f8b0:4864:20::53d) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 16:54:58 -0000 Received: by mail-pg1-x53d.google.com with SMTP id i1sf5967062pgg.20 for ; Mon, 08 Mar 2021 08:54:58 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615222492; cv=pass; d=google.com; s=arc-20160816; b=WavuyIRb8Hkp9pArf10G8lqhw+M4B9zkVsp3lQIgxrT5eAil1FwFi7kZx5hsL95R0H XguDQws1WN1sIIPLFmXV1ucAuwOIAYb7giFy2GpfQ3gbFP7lqCEJuBgh6XtB6nDyl9oH /AGTz281+QR7AZSh/NuQSuWGXotWK3AfVdnVBiLW7CVuANJS+yq4xeXVlSiWdCAhPxb7 3OA8Ktwvr2e3PPwBYpt+JorCmRx6H28lRAMk5zGRXYKNsJahfsZ4k/eZ+O24OPFOfm1T Ie6I2QXPNK8xLOv7hsMvFOzitwvf8sNdkHFu6pNa6XMjJCSTQ6cdxIli35eVdIvfi76J G2NA== 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=w1ZvNRuKwGq/v23LO9ApgFfWGs8xzbj4FQ3bCEu+4uI=; b=h9MYIF/D+dpdyhrb0wA7ZztSQm4RUjntIYwHbz1IWYPTo2YjY0dE8xm87gu2QdAVc0 9CpfgZc64i+O7QpywT5Kc8XYl/tvvhGbyWlbEc+gcsa0ABholm6oqCiQVGvstkoJq4Bt 86m5sfaf2GAkahfd7soysNb/pO6EWhC3ikgTHNFUhKxfzlITcPC/YPfX6Ld/slLBEJ4H aJU4T6BGjq8eQV3Qrq0OLt/lAhZr9GfHQR6alm4mEOYee6rwbWD0DOknNZVV5gZ4exV0 lOkVJGBBIHqBOhV2qwttnUWR5DHBIxGyrSZHtl2XHSj3DXXy6LjHms8qakeWTO2tE/KX y88Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=CipD5xqm; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::e36 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=w1ZvNRuKwGq/v23LO9ApgFfWGs8xzbj4FQ3bCEu+4uI=; b=gBQvBDPN0bWK8z0U+BGX4wndFvNtFhC3GgA67H/hSQvH89gtZKjBuwQj5gorXETSbz vne0hvlQKznCdB9+TTuJ17Oea0y8rQgKx05zoBZ+0f3slM1gHV9ZxlcCnkQmZ1UnBQuO vPZje8M+kuEbCMOmXICnoTVvNoWVusuETkMBa8n1O6DRAvDcm7mjECV6lCCS6vmNmUlG L7MrxByuIhuQGHkUO8U5pmhLuCLk+yskQfwGuaft9NxefOI8dyF09swOxq/jDPWEizD3 27+kiI8FoJceE7V3KzYWmdzZd0t1hXFmh2i8WfMWipVS4EI6jFnFX3dCGCOguPNJbMRX a5Og== 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=w1ZvNRuKwGq/v23LO9ApgFfWGs8xzbj4FQ3bCEu+4uI=; b=Rv+9V6ntJhFbgyF8ZMPp8TTeVWRnCpqmsS9Dbot4Zs7jfdp9V83j80WEEhddUKo5UJ fqqdO2gYcvkR2TX2SrvqhR4Obw4olFSnmh0rLIWjzItFqn0/LGWldRpJP6NlnIXVngUs TwwijUbpSWZ+aqo0wguOvUG/nFBufLW24pg+w+cwCkx8RiiWFUkJU/X5hih3/x/N+vlI /F0A71X8UW0WIa+8K7yp0XMvegdB50RlYxKUhN7ZVsEGtsWknD2MCjMtqHXCdDK4/Nzz HdyUkMrkr2CZcecF1bme5dD58Xko2rfcfAubmnI+Q+1fs7hj7uztnMf/Nl6qDYbmtw4w vgOw== 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=w1ZvNRuKwGq/v23LO9ApgFfWGs8xzbj4FQ3bCEu+4uI=; b=Ooj20+Yx2EBc5YHAIQJCfOnhUGhJfhVVMkb7LoTZ+T9yOdHoE888suY0EZ5VOLPRTP XCP6r/LPZ8HRBnQvW1XvfqPZbw39QDwOyEW8yvLXm7OGjN9Rul5gbfZ8JW9dz5nA3ICR wdnI116iFhA6Kc6EJE7tzTiTyj7JDxF7LqJ12JsqTChMXTRysc2ImA48gBcUHHoWpm/R k8JFxjDipTNEfVV5b09rICQRg9SqnQ+hG9wzBs+i4Leiafm3HhrGCCskxjOyCnDE8e2G wGgJlaL07jB9ASXJca1MPCLgCwan22gDNyJTEqfTYk6Tb5oA1l588EaufU/CM+M7g3nE VE9A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533Kn7hr2CO8VQtsW85J299Amnwa6mspVzTSrZAWRLyfPsYQA+6X pur/41w7eAQhTYOEN3cwzIg= X-Google-Smtp-Source: ABdhPJxSp6YaXvA5zoagRzufxoDbCNPd5IP4VI4BvaNjBR1tv0+ebKpEm+rP067iHKcIir1NpCCa8w== X-Received: by 2002:a17:90a:7c48:: with SMTP id e8mr26690842pjl.89.1615222492201; Mon, 08 Mar 2021 08:54:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:1d50:: with SMTP id d77ls1214342pfd.4.gmail; Mon, 08 Mar 2021 08:54:51 -0800 (PST) X-Received: by 2002:a63:4761:: with SMTP id w33mr21447118pgk.118.1615222491291; Mon, 08 Mar 2021 08:54:51 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615222491; cv=none; d=google.com; s=arc-20160816; b=oq4i4sE3WMpx0MYmCt//DJRZJtOOLwzGxJpuy675YsTsl0F2Qf1Gz8VyKABMiy40uF 1o+qAxIpqZCKKK47fMIsbKo1o5U+ExPZnncUN0rAXoANZUs5V4/SVXyuI8rqnmvEBYbw IrkrHpmFEgRijslFumgQMasamB9HuXYnNu7gd4DX4GZyjLh37+DHX94UDEH6gkFodECi 7+YH5GGEDGoPRCl/f3oV4EL8s1Z9O07sp1qlvjpcwSBnwq2veqLiM2QL0zC7ctSnLMoD I2uvGIfPjdCvgw4a03VYxqF5qPnE1IMLuiH+g7bDOb9uE2XMK1wH0X337q9Ksg2PufSY QShQ== 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=yGdwMhEqIeagtzqflNBpJbf4tJQBK45WYsgbQI4s7yE=; b=sTQc0g/Tf30sc7sHZh0aCiSafgRgK8RxudeVLCmQs3LGvppKD2ySiBZVYUmZYfDIbp i3ZYf0d1rjipgw7nO5n0ywJR3YcZ4UwzFKNKNgpuo0eCf7IHSuF43be8AWTjfSvaDVud oPBIPkk0PhPXPVvvCz9kNemVngDIerc3LcfWWsa881fR37jF1ZB4YiUa4TtQJKKAHNad rnQcPL917S+lDk2FndM3DstGlIFGhWJFYaiFPCFsnpdjcP9BfdxClPqfOcre8Vr8J04c kdRAyo9vEaIuaP4Qii4gfy2VxrMKTWecbT/Udr1pzZbT1QNA+7hAa5CLlZ1J/PfczBwG svDQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=CipD5xqm; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::e36 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-vs1-xe36.google.com (mail-vs1-xe36.google.com. [2607:f8b0:4864:20::e36]) by gmr-mx.google.com with ESMTPS id n10si714558pgq.2.2021.03.08.08.54.51 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 08:54:51 -0800 (PST) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::e36 as permitted sender) client-ip=2607:f8b0:4864:20::e36; Received: by mail-vs1-xe36.google.com with SMTP id j12so2929748vsm.2 for ; Mon, 08 Mar 2021 08:54:51 -0800 (PST) X-Received: by 2002:a67:3104:: with SMTP id x4mr14117018vsx.0.1615222490335; Mon, 08 Mar 2021 08:54:50 -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> <8de81acf-3a00-ae98-7003-9eaf404d0b89@gmail.com> In-Reply-To: <8de81acf-3a00-ae98-7003-9eaf404d0b89@gmail.com> From: Egbert Rijke Date: Mon, 8 Mar 2021 17:54:39 +0100 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Kristina Sojakova Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000c5122b05bd094ab2" 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=CipD5xqm; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::e36 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: , --000000000000c5122b05bd094ab2 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable My agda file with the the interchange laws and EH is here https://github.com/HoTT-Intro/Agda/blob/master/extra/interchange.agda And the coherence law is here https://github.com/HoTT-Intro/Agda/blob/master/extra/syllepsis.agda For anyone who is interested. On Mon, Mar 8, 2021 at 5:38 PM Kristina Sojakova < sojakova.kristina@gmail.com> wrote: > If I'm not mistaken, Favonia also found a very short proof of EH some > years ago. > > 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/8de81acf-3a00-ae98-7= 003-9eaf404d0b89%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/CAGqv1ODEzmBLWmOvgVmtBO7D_xttUKDW6NSNF2Q2_3K7wfYcCA%40ma= il.gmail.com. --000000000000c5122b05bd094ab2 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
My agda file with the th= e interchange laws and EH is here

And the coherence law is here

=

For anyone who is interested.
On Mon, = Mar 8, 2021 at 5:38 PM Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
If I'm not mistaken, Favonia also found a very short proof o= f EH some
years ago.

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/8de81acf-3a00-ae98-7003-9eaf404d0b89%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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1ODEzmBLWmOvgVmtBO7D_xttUKDW= 6NSNF2Q2_3K7wfYcCA%40mail.gmail.com.
--000000000000c5122b05bd094ab2--