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 474 invoked from network); 8 Mar 2021 08:53:58 -0000 Received: from mail-qv1-xf37.google.com (2607:f8b0:4864:20::f37) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 08:53:58 -0000 Received: by mail-qv1-xf37.google.com with SMTP id e9sf7156560qvf.21 for ; Mon, 08 Mar 2021 00:53:58 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615193638; cv=pass; d=google.com; s=arc-20160816; b=swXqmVL3pcXPpMjC2q3LFc9l0DHmYExoCEtjz5LvPuEhSgZMQHclENYtPmBZBkiypk WwPHQgBJ13jnVd7uuhn9iSiVVFYBL+IM2sRtX2/K0wIWRoYFMNg94poXk5nbSruq7sjH nM/G2yHUHOeIT3qE3Dzf0X6I990I7m24gQCHgED7I6blNMXb1c4d/fNjAOrZbVq+uUZb 60ZrC5pEUqvnXIbfSieKOKfNI5rRngySoqsa8VVc2MT8G83mIjJwdVVqXuVv7G2E2jeY bL9QH/Qy74wb37YmRydmht0BOecO6F2ukFwGIFDYC5UwPZjpfqwmpkaB9NvBRe6n0LCd ueig== 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=f5NNGYJS79MAQu1CFL82rpAygaK49cxtr/cxCUp1LeE=; b=Rm41M4y2SsYa+jexkA+TSL+jEtWbKpUTLYV9Mcnx0vU2ZVqfqD0/05uSSTf849sjw+ NS7lM99oomjJ/auEL0RaB6mlfBJVGxPKHSlMrJbG9uXwckfiV/U8xcdUKtTpbyE3FYBi uugNYP9Taih4KUaxmfUZVXL0MKT5FKduuJanZl5o+5ME8KYdWVXjvt5QCG53MQvO2EL2 GA6getGE1C3YKzETWRWTPLDKM8NOiDTnGAHfI8hc48MZLLPkuudmG+0kZAwD4gZwh2x4 TeaOJnd+4lFZIIl5JYjudi+KncmUjcPFwSbAnFcyPUe18SvQRvHh3jSKnBPR2++qz/be OKLA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=shEctDrA; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::e34 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=f5NNGYJS79MAQu1CFL82rpAygaK49cxtr/cxCUp1LeE=; b=Jua8FN/f7aF0QN21Y/i8rAHLZT44ziilSg0p4byotrgpFOMWmF3mAY3JUDNU2lUUz7 /OUP4dVgVnwTPpgKR/6nEC3YHv+TuV6l5utzhgNxxMCuySg3bHy54ktZl4S9vUijuax+ 5beLf3MBAwEy8e+V0pzbVy++t0JAtJgW3Yl6EyJxM8m7rTEILt3I+qgxsOuHQM/iZ2Xb rFkYiTSFsdSWVxxbNLiBor6dCQh7ZfZpVITfACZT1ap1lORhMqQc84Nc10Gh2JkSpCxC dITBtRecpC/cpEyzfi1vl09UZrA991lbaut83kTiL3XsSxW1jq5mK2Wb5TPU9oHO3RIu vfxw== 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=f5NNGYJS79MAQu1CFL82rpAygaK49cxtr/cxCUp1LeE=; b=Pcr3pFh9ROmf8B1b2jZgJggtkr6MTDnRnlWgyhQVEC/MImfvR9SRQFvUKgdZB+Ajfq n5UF1Y7Uvh7b1s4TlTorKKFiVOb8U5+7t4d6g5yqD/S7Z30xYqwgS0CfvY7U/ZqZ6hu9 mN0nrNiF+hMDcn5rB6g91WUFESlIuboj+QKSycl7iSTKnU8vTQpE0STNTEgzOw3qihha Hhnd1RFD82rLG6oRUHWrmGEeWrwRagx4tkq6lZ/jKZSbmFFvpfODraVmqABWVIPSMgFp rBBR0Xz1QYqR9/2UJjCvFWkpJp/0Ba8ReJO4LFF9BH4WhVukjM2hbo28hk8lRj7Lx68B sDkQ== 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=f5NNGYJS79MAQu1CFL82rpAygaK49cxtr/cxCUp1LeE=; b=dXe0G85vqtzsOMabBv1yj7YCkl7Bub+wh6iTr7K5zlV6OEcsuKAtA+MJN/GHxTM2if qUtJaixVnHiOCs3aH6AHmwD14u1vmjeUM6wTa/zLEmvL2o4xzX15SFvWxoMePOlP2MQ6 KvWkBbVpEv3NB0CV8kt5bQfSMakRm/65nV+hp3h3AQVIPE9c6iZ+MYvYUtttPYryhbDj 5FhNCvy81jh9gJiC5MLCp6k8rCjgOLlYXAPsNByPO/xtk3ezHpa8whiPhUjsuin5Fb5b ak18l6u4hSLxfigiIM6+qWaMJSrSfCrtky4Bi75L3vVvvp0qF0VqQXo8FoTH0FUlxuue ek+w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531QzObMwDWZGf+UJ0huXQp4kijDK40Flus7/hM5n/LBo57GL351 Wj3jaj6qDlkO5jo70kaugpQ= X-Google-Smtp-Source: ABdhPJwYhrhU13oM55TGC/aKSmRjXtcqmnhX552tmNoMHarDv/Ee8P7HltCXE8XZqiMKWwOJ3jvFdw== X-Received: by 2002:ac8:b49:: with SMTP id m9mr4612681qti.182.1615193637773; Mon, 08 Mar 2021 00:53:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:7497:: with SMTP id v23ls5583175qtq.5.gmail; Mon, 08 Mar 2021 00:53:57 -0800 (PST) X-Received: by 2002:ac8:660b:: with SMTP id c11mr19495288qtp.133.1615193637189; Mon, 08 Mar 2021 00:53:57 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615193637; cv=none; d=google.com; s=arc-20160816; b=XQ8OMfrxY0uvkHKZUl2/8kAUdMekrSiNJmT+zbZ1DL37tyl2DxZZoVcq2/9UN5ENrB dWGBmA7yclcq8IMScA4vywbytbfFayg6Bhxu6ynoqs349n6JsD146iwVx/mjImfqVBho Mvsr6p4pNjr57HzFWAeIyDRJZP+3dKNjQFh79fqHtEVCtg9G+o/9FOizApFQfUWevmxK jXzdKhclGWBO8r3Kx2xNwIYQvdglLnjzUKplUMybn+wyd6XF4TrJBc1B4Rw39SUySnww DaPVOLr02Yrqn+yIEHzcRYyPS8qQDZlaQ9fpI9+r3vS4B6LsUdyL51DftVgg3zZzHYAO EwPg== 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=hF+GfPqVtMN4Z3yXGzG00Sa7PETxedYgXHey12c5tWQ=; b=s8WLN5RWOGY+SHK1BrvICAZfN/lKVeIosbiOYrzFIT8Vjp5K0li3GnW59K5GNVQ+yq P+X6DASW4r555Rb2u20cy+G1ZHTC6txWHGmuBYGgSXlo1B+wrzkVn68yWpVsvWS6/TwT ZgwQ8XixnxRMRLknqWaW4wugTvEiRMdc5lZodzuh60j12QfvMplFTD3dyFdf/+FZI3hh rmUoGs9fWm12YMSDWGYRM1KEQhZQ4D6uaMU68F+hyJo50rM52fcsXZnqzFYjXjy0szAe Y5HlIEeEnKuS6EavbXVUdokk0t6eBt31wf4uXBlbyvQQFXJCCRNFcQTa+ly6+gD3U1a3 9GVA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=shEctDrA; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::e34 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-xe34.google.com (mail-vs1-xe34.google.com. [2607:f8b0:4864:20::e34]) by gmr-mx.google.com with ESMTPS id r24si391828qtp.1.2021.03.08.00.53.57 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 00:53:57 -0800 (PST) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::e34 as permitted sender) client-ip=2607:f8b0:4864:20::e34; Received: by mail-vs1-xe34.google.com with SMTP id b189so4459412vsd.0 for ; Mon, 08 Mar 2021 00:53:57 -0800 (PST) X-Received: by 2002:a67:3104:: with SMTP id x4mr12586609vsx.0.1615193636804; Mon, 08 Mar 2021 00:53:56 -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:53:45 +0100 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Noah Snyder Cc: Kristina Sojakova , Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000f71d5205bd0292c8" 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=shEctDrA; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::e34 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: , --000000000000f71d5205bd0292c8 Content-Type: text/plain; charset="UTF-8" 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 --> 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/CAGqv1ODR04M-4HB0-HvUsn%3Dmpe4PTR5osJUvFR6021xnCsd1sQ%40mail.gmail.com. --000000000000f71d5205bd0292c8 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 g= enerates the group. There could be many elements of order 2.

=
Best wishes,
Egbert

On Mon, Mar 8, 2021 at 9:44 A= M Egbert Rijke <e.m.rijke@gmail.c= om> 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 pseudo= code already.

Best wishes,
Egbert
<= /div>
O= n Sun, Mar 7, 2021 at 7:00 PM Noah Snyder <nsnyder@gmail.com> wrote:
On the subject of formalization and the syllepsi= s, has it ever been formalized that Eckman-Hilton gives the generator of \p= i_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 whisker= ed 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 de= tails.=C2=A0 One could also ask whether this generator is the same as the o= ne in my first paragraph.=C2=A0 This should be of comparable difficulty to = the syllepsis (perhaps easier), but is another good example of something th= at's "easy" with string diagrams but a lot of work to transla= te into formalized HoTT.

Best,

Noah

On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova <sojakova.kristin= a@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/CAGqv1ODR04M-4HB0-HvUsn%3Dmpe4P= TR5osJUvFR6021xnCsd1sQ%40mail.gmail.com.
--000000000000f71d5205bd0292c8--