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 31876 invoked from network); 8 Mar 2021 08:45:15 -0000 Received: from mail-pf1-x440.google.com (2607:f8b0:4864:20::440) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 08:45:15 -0000 Received: by mail-pf1-x440.google.com with SMTP id f17sf6047107pfj.3 for ; Mon, 08 Mar 2021 00:45:15 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615193111; cv=pass; d=google.com; s=arc-20160816; b=S28/D8Q33r3H/HMXTiKvvHzafzXH1TDsUSgrymvCRHe/9nMKkt4vhJ9TeZ+HjFCJJz 03WWk87xU7nLmv4fTf8nMaUoisyv+dZGa3GB8oquFNRpH3PE5Lk7hWlMo2pVw+yw6pv7 4GXULGKsaR5yhsjAhaY8b3WHkTtP81pvg6v3I6++B/POn5RtsBuS4XSX/YJ3h66YgjKH EkL94nDcGDCibyXTQNgT0t1ijYfAH0Gp8g8VHUZIdbcvr3TLSjbSdwgN8hChUwCpHOK+ bkDHqtd+jZdQs2QZbzZe95qEMbkg3m5bFfe7+SQPsr1OLk+8yqyz4tqc7doKwqJv8yEP dwng== 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=BWrDLEpqDwnf8j4aK9xOsXGAbPJ6atDMw4EPr0K/b0Y=; b=k4Y8LkHI0zi8qEHp59jImTOebLI+zBiJGMzfHw5XAhIkflPXLptJnR6ZxxGJr/Ma/t 19tNrEIzPkVexzndC6GTys7f0/2vsLhZdMSGWbKgqJeQlxOF51CaU1kQ0CWq7DQQYie5 BCx9zaiwofNeoJWRwgWLKMyLbIHZeHTSYf9se0Dz5dK5MuzIpW/VMUcaKvg1FdYmiqEP gjRoDXvqcN8CZZYkNe98yUqLEj3ZqP2HlAJ6AmrIsRn3D96qy21gw5IXUXu7cVJyXC2A tgZZzWbTp9Z1DBTaGW4oH2R3iBptoNG33OJLBUj2f4RGt99TtXt+Q1iY7XOwxjO4caQb JeEQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RnL6Hvsm; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a2a 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=BWrDLEpqDwnf8j4aK9xOsXGAbPJ6atDMw4EPr0K/b0Y=; b=Nqu9tCgb4YhmRiFSVtPatPAOIWvHllrC17jT6TbLvOz8yr3y63zCprtAQkVeBCiQlP aK082mS7ncPFB17O3pVvJiZVQqqRxckcYj/56fPK987U8y++gXka1UWSzGXQmdkuHEGA SmL3VkWo4u/Aid29lkDJmMrDzTzjXSatYKhfnEPEdMy50sNaIuhGS4u7pLmpzvyNiCCf BTP0ir7NssB1YPqPXKp7HXXm3gBnRQM2voWqYWXHqGvR0dfQArkR+1Cj07mZPRdtPATp Ra7zB9slPq8rYXExSSKMbnecRKvPe4N/2/53vSrDIQb8Dy2i2WscOPf2E26OWvJqKn5V kKAw== 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=BWrDLEpqDwnf8j4aK9xOsXGAbPJ6atDMw4EPr0K/b0Y=; b=H2nEvdSZ7nui7BVDs2S/kAYI9zyGT+juVBfq3R1JJfnGuQ+Myez3m3YzVqEn3cO5Wh fPKDD69yLez0ZA3acU7EQSekEb2ecChgGcmwxWSO+PI4lp15cXwsl4yENDwmkOHSsNKx rDwv7qC8VzsGeR3G8YM+2CKh+HQjCDrYXwx1yQ8OJl6v0OKyelZlRRs9Jw4dfmRyTgbt pf1wO2GlPZgjUrYKc1v4cejks9KNzJAqqo5EJY0aqDPZANeUW5/Q/8PAg9bFT/PjVbz1 AuuYvkMYHNMrUii0Uq+8GWhaeP49SsiFuYBNWfG+9W7dng4KzRKRObADtx4hbz4xo4nd Clhg== 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=BWrDLEpqDwnf8j4aK9xOsXGAbPJ6atDMw4EPr0K/b0Y=; b=Dk2caoaXb9CxOaqodGW4O1vVRj+awa299aF0DEP4Vrz8DshulFMMZZBSzgFRj47wMC gpyE2aY17pXzWxl0/DEU0WgYANfQ4ySL4mU0QnT1WNmGpXKLnB5shFCgpa4iZCjLWd8x y+8ZCNra2ONT4s8+TqEkzpFUMhF0JMqo4sg+1JSJva9t89E2voUCug5I8YSlcX8cyIcv yuF9+tiNvgHqdqMRsZDcKoPJmkU28RmdcMD3BKdzV+bwgaoO+nW3eeu+TUpw8HBkUkv9 AKIJ69xkE4JRl7a4M6CWWj6TLg2XCUQgoN/W2YvoyUaxn/jHlbz0jFq7ED1y7xQmv6y/ Yc4g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532pnRgcaPHCYw1WhpydVqR+D52OaiqsQ30c6ptkNMveXa655faP Bii2NFOAbCl1JNURNq9R//0= X-Google-Smtp-Source: ABdhPJzE3/dJ0Zh+nlZZ4xzs/LU/POgEWRogXhVvNpisKyrB0yPo7/aJCcc7EG3FNz5wLjUMNaWNsQ== X-Received: by 2002:a17:902:ee82:b029:e5:fd49:ca09 with SMTP id a2-20020a170902ee82b02900e5fd49ca09mr12691271pld.55.1615193111142; Mon, 08 Mar 2021 00:45:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:5302:: with SMTP id m2ls4827681pgq.5.gmail; Mon, 08 Mar 2021 00:45:10 -0800 (PST) X-Received: by 2002:aa7:9293:0:b029:1df:4e2:c981 with SMTP id j19-20020aa792930000b02901df04e2c981mr20114668pfa.41.1615193110492; Mon, 08 Mar 2021 00:45:10 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615193110; cv=none; d=google.com; s=arc-20160816; b=Tlw9ExyAzglkpECByOQN3iB78jUp+yDGrcfVJKldggoS3lepxP1Lu6RBOoXMNFjRc1 PM+kQlW/+RNiD1hGgTrKglC6kggGFTU0rpgUCxZrT3WYGiMT0xL3xUsxCDXs2MWV5qkh Tzx3h83ZwiKR0O4rHV/v3SNFl83l6sz5DZxksryGoQQFMa2LmW3/htlQj/tBSflHvd9N PhJR+va57Yh9a0Vyy4fC1XE1dbSGAcO0ogFwVpHcirgqAHTvANEfhVLT2bYymyCUU9iP Qn7SdM1mQDwaRQOR8PAMiseSo75zMEbY2j8BkYeoJO/HIYY2LR7/Hnc4YDNTufMfCtzx A/aQ== 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=C0DbEAJ9mhTPsUXqucxdN5AE49LyfuhGfVKNh1mXtxQ=; b=XNzX4sbTXUfJEP/CDt/WFrTAVkB/oT55piVmussXvc+bwfkN+2f8tdIaanhUTRdnhH FgV8opcOh8xATJ+oNwciQVxgCUJtRwwNmako70JxbThah8dUrpO0x7RTGXKK25z6FvQk E0L7Fog4Nsy0+oaNB6DZUbxi57NrvM/BKECtH6K23j8Rl5PNPbu818RNik2tOpbqfw9E B3VgGxjWF/Ao2x3Dkn3AD2A0/6uvY4EKDVTKuh1NLjGXTVSRhBt2sS1b4hYCsRRDpwrG RIdCuXfCjSZJK/z8MvsSOP7oojSvVNfLT5hZCnZ71g3kfIgl/EFZd4BzWIYASg7H1t1X KRIw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RnL6Hvsm; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a2a 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-xa2a.google.com (mail-vk1-xa2a.google.com. [2607:f8b0:4864:20::a2a]) by gmr-mx.google.com with ESMTPS id m2si435643pfk.0.2021.03.08.00.45.10 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 00:45:10 -0800 (PST) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a2a as permitted sender) client-ip=2607:f8b0:4864:20::a2a; Received: by mail-vk1-xa2a.google.com with SMTP id q17so1970444vkd.3 for ; Mon, 08 Mar 2021 00:45:10 -0800 (PST) X-Received: by 2002:a1f:9d8c:: with SMTP id g134mr12210555vke.20.1615193109613; Mon, 08 Mar 2021 00:45:09 -0800 (PST) MIME-Version: 1.0 References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> In-Reply-To: From: Egbert Rijke Date: Mon, 8 Mar 2021 09:44:58 +0100 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Noah Snyder Cc: Kristina Sojakova , Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000008ace3c05bd02736c" 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=RnL6Hvsm; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a2a 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: , --0000000000008ace3c05bd02736c Content-Type: text/plain; charset="UTF-8" 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 --> 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 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 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 < > sojakova.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=TSCggv_YE7M&t=4350s): >> >> Given two higher paths p, q : 1_x = 1_x, Eckmann-Hilton gives us a path >> EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) = 1_{p@q=q_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-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/CAO0tDg7MCVQWLfSf13PvEu%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/CAGqv1OBJ7iSeng_MY3f%3DY1k3EWgm9Q6VpyU5-EH-j68H0BYC9w%40mail.gmail.com. --0000000000008ace3c05bd02736c Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Kristina,

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

Best = wishes,
Egbert

On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder &l= t;nsnyder@gmail.com> wrote:
=
On the subject of formalization and= the syllepsis, has it ever been formalized that Eckman-Hilton gives the ge= nerator 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 --&g= t; =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 (wh= ich 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 d= ifficulty to the syllepsis (perhaps easier), but is another good example of= something that's "easy" with string diagrams but a lot of wo= rk to translate into formalized HoTT.

Best,
<= div>
Noah

On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojak= ova <so= jakova.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/w= atch?v=3DTSCggv_YE7M&t=3D4350s):

Given two higher paths p, q : 1_x =3D 1_x, Eckmann-Hilton gives us a path <= br> 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 &= 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/0aa0d354-7588-0516-591f-94ad920e1559%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/CAO0tDg= 7MCVQWLfSf13PvEu%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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAGqv1OBJ7iSeng_MY3f%3DY1k3EWgm= 9Q6VpyU5-EH-j68H0BYC9w%40mail.gmail.com.
--0000000000008ace3c05bd02736c--