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 24665 invoked from network); 7 Mar 2021 18:00:37 -0000 Received: from mail-qt1-x837.google.com (2607:f8b0:4864:20::837) by inbox.vuxu.org with ESMTPUTF8; 7 Mar 2021 18:00:37 -0000 Received: by mail-qt1-x837.google.com with SMTP id k15sf6520608qtx.15 for ; Sun, 07 Mar 2021 10:00:37 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615140032; cv=pass; d=google.com; s=arc-20160816; b=yQ1DfdbSh7iUEoU19cer71f33RWQik3xe7/6PNXGOYLjWrT5Kc/oeVoLfqXa0MMty6 mkYX64bU126VE6a51rIeWXDkeM7ExpWi+scuvwvmZcKvhD9Hx/E/WpoWPitIcmUJIH/E R9Nac6OZfzRSjTZtkkAWHrwMguaXshBB/jHnGb8C3XlCyXcZ0F3YAseU+cMfrIPuUE/o VaWd3YlKjIoAhpYoIQr3g2/zxj44PH0/klKGxP8nESwmTgS8NGNyO4PHMfAq7Y7YIZaA 1g+Rbq8N/UUhZq6ypljSOpsuDv+nAGQqKk7SV47dhcA/Dtut8YkRlVy8M0EnULdSYyjK lomw== 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=WhVxS2wV4IyzlYRIg3vJLvgHV3WOE1nf2YJ0YCvhcDI=; b=GhhRe64TgOvYNL6jKPTT8gcR93hV7JBu8xDavtRkfvSR8rgDNljaJDWfnieJooBILO Ff13GyQLFOA+HcXNYNvuMhQWL2f4o2tOtyC6nIjTtl9H3bvoXXIrD1EGrslCL0ZSOQr5 cEJjWtzW8oQsVwfIHY7CYcq+eLn2Hexpx0w0HJs9ciqj08gpJrmviZtZAksERYUENhOx pWPclFe2hQhQHagDeTfQcF9KKG9KslG8L31UFlO/+N1p2OpFaVbybEu6jB7/PngrvRUZ OydYDknEFvXdshF3fflLIhPvjWp0BK1EVIXebErIZBELluv2LVDPMYb83dfD98U19ztR Cp2w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=fCYGa6ii; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e33 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=WhVxS2wV4IyzlYRIg3vJLvgHV3WOE1nf2YJ0YCvhcDI=; b=fjf/dtl4fXeuSMQNkbLdB3Fqd5jixp+JEMI7Ib4iI1H2ViOT+W7SYrP29Vn1lCSmPA GsCMRxDlJWJopdh86xIK/coI3OQOew4XRQ0u69vaDTbmYGpnSED4pY0ne2DgVHaacoyh sDwX0szcm84IWk8cLRSv5Y4sEUcxyfEYNFhI+bI95UVF8ZMGGwABbw8f9Ht3D5TZoZXU gdLcc0E0mbCr3u+s/28WF0EnT07odesGxXBzGMRQs1CR6eQuBp+Ht8Mb9a9Tmhx4JbI8 5BRwZ7G3kYn+1U5+PcnJ8wVe5RoKQ4pf8VQd5I5e47otzidop1YpDSvbMpcHoJhVqoHL wmkw== 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=WhVxS2wV4IyzlYRIg3vJLvgHV3WOE1nf2YJ0YCvhcDI=; b=GGc7bkNiBvBLFlc91W043EYswFv1aAu59juwWa5MIPOM3Eoh47fhzUTjWsUsVcskgA uqdIAn4k1F1tpLHZt8o9D7grBW8xDg9IOssF8TchCiAplr5NDOyY2bTd1iweq48w0lUM 49Xn26WNWqSWuZSDSkZEb5H6/Ojmnv7a4mV5cpruV2Jooz86g7lsEVBLLJImplkHx8lS x26iQ5Xu30PPPesPHlNUvpxTXi4P2QAywVI7lMeghcpAlTo3LWksdVp17I9XEx+r5Lwt Qo2pjqt/cS6kmloppJ+NPWDwC7DzoW+Ribv32Sk/UKlXUJgiHP8Iark0QRVZRvDLuLQS k3Sw== 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=WhVxS2wV4IyzlYRIg3vJLvgHV3WOE1nf2YJ0YCvhcDI=; b=kaSOK+mgLI1BGFKFqUsP2zk2lr9yLJgVPONyCpCILGM4owrnTegvvXYdoAWNROkiRS ohCyZQy4oHjsQEKKWgdAiGH/Ky1OfUms+0TqyJTlM+3vyRJ/MJtcjf7EQ832VT/QIm+j ZShj+vlJ/Ub7yNNQbDwwXp+C/W2UIuAieXcboXnod5qL2pAjmppwkcxAWihZvq2gLgnW 9UuFmt9p8w9yx9xGrkEvx0pJnkQmvCY//kjbtOiWM440/TNjsWfvL+h4q0g1Tjqtw+eZ PynJPglM3sPwYoZjw8yqq9enbK/VHLPFfa6bjm8OAM2PvKH/viD/AC4f/Qoe3T4DyRoC dF5g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532nPmpC/UHtZE2Y29HV7e8OVErJuX/GEYHhoB4cbC1I6Qzecs6L L32sZOmoT97l16hKhmSSOzU= X-Google-Smtp-Source: ABdhPJwZpjzkXJZssJIOFGci9u1B7eOj+IE/vdaKgEqRhB/MoZfaMorwgPpaGsfd/nwoJ8mQmVIYnw== X-Received: by 2002:ac8:5390:: with SMTP id x16mr17629515qtp.194.1615140030781; Sun, 07 Mar 2021 10:00:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:620a:7c5:: with SMTP id 5ls7656159qkb.8.gmail; Sun, 07 Mar 2021 10:00:30 -0800 (PST) X-Received: by 2002:a05:620a:791:: with SMTP id 17mr17804313qka.170.1615140030323; Sun, 07 Mar 2021 10:00:30 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615140030; cv=none; d=google.com; s=arc-20160816; b=1LGnfOxeS6iaRDh0qD3+zIuknPB7EWAgjCrIMb6XIZYpyUzkhBkp42egpk8JF3lRaA /pZj+fCQCxLQ1hn/l6Jghc1obsjzElfsuBUkGpR/N1lLy7GSLCtuw4uWoU5btxUOBi2x Ra45cr0iBy1qfqwwHpO2FLKq9J7BkWzhwf0EVwxj07BxmSWth+9wB0AJa5+PicPSz3jC HJ2Slsd+Djhu5yO9HcCA5kLls9XxpmwYwTGmgfhkDm6rB28mVl/gnoGPNhljYaU9jKMS p3Sk5kXYWI/0JglURPoquklLY3sj4hEwRGcdDLkzFu3ryxsvxUtBBSpyr/M52z49ZIaV Iqbw== 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=RS3vrIGrrhtK4OZ6cwbvebtDGEDBG93YXUge9bgxawI=; b=vWrwVeJbYJFuffCThZua1slEV6Ga3NJKBnTvIx+BbIaACsMykODJBXmZ6L4ut69Rty rnzZDZFVYMdqrnTO8Awvz9Dkhdl0oPiaPLfQI+cMbgRmOm/3xjLR+KuJvQs9G3K3bHuO S8ykB3iV854JSc8uPBSArP3xqjhxuxzX8BStsfWmYuFsxuv+eLc6VIaBn7H+hx3YF/Ws GqI4fw8VkfdFv6865gFswvOCWDkVeDKKAS6J50m7xcNFCZPOn0id4oQ9l3cRthdjhtt4 oVvphIqnIO6r9LMuC9daH0I8nvQHcjQlnlnN7RX3Jo5JU2o1mhVkuIVuG7dHuHtiBAAD aoQQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=fCYGa6ii; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e33 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vs1-xe33.google.com (mail-vs1-xe33.google.com. [2607:f8b0:4864:20::e33]) by gmr-mx.google.com with ESMTPS id d12si445791qkn.0.2021.03.07.10.00.30 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 07 Mar 2021 10:00:30 -0800 (PST) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e33 as permitted sender) client-ip=2607:f8b0:4864:20::e33; Received: by mail-vs1-xe33.google.com with SMTP id d25so3711066vsr.11 for ; Sun, 07 Mar 2021 10:00:30 -0800 (PST) X-Received: by 2002:a67:79c4:: with SMTP id u187mr2335401vsc.1.1615140029983; Sun, 07 Mar 2021 10:00:29 -0800 (PST) MIME-Version: 1.0 References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> In-Reply-To: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> From: Noah Snyder Date: Sun, 7 Mar 2021 13:00:19 -0500 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Kristina Sojakova Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000bff0ed05bcf6175f" 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=fCYGa6ii; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e33 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: , --000000000000bff0ed05bcf6175f Content-Type: text/plain; charset="UTF-8" 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. --000000000000bff0ed05bcf6175f Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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_bas= e, and we want to show that under the equivalence \pi_3(S^2) --> Z const= ructed in the book that this 3-loop maps to \pm 1 (which sign you end up ge= tting will depend on conventions).

There's another e= xplicit way to construct a generating a 3-loop on S^2, namely refl_refl_bas= e --> surf \circ surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl r= efl--> 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 sylle= psis (perhaps easier), but is another good example of something that's = "easy" with string diagrams but a lot of work to translate into f= ormalized HoTT.

Best,

Noa= h

On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova <sojakova.kristina@gmail.com> wrote:<= br>
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/CAO0tDg7MCVQWLfSf13PvEu%2BUv1= mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com.
--000000000000bff0ed05bcf6175f--