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 3285 invoked from network); 5 Mar 2021 19:18:53 -0000 Received: from mail-yb1-xb40.google.com (2607:f8b0:4864:20::b40) by inbox.vuxu.org with ESMTPUTF8; 5 Mar 2021 19:18:53 -0000 Received: by mail-yb1-xb40.google.com with SMTP id l3sf3507106ybf.17 for ; Fri, 05 Mar 2021 11:18:53 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614971929; cv=pass; d=google.com; s=arc-20160816; b=THusF1k6IQ/DtRLSFiiJMkY0yJhBeiIKYooKZt4kZHobZjtDRe7l+gF17MJaF8R6xi GRYGFHKP6mQnRa+fhu4a5jxh2YactQGAevipbAx12MF4W4R6zmCNiK0GyF+pVLEdUB1z 0uiMyA8A83jxXBn0mDZ6i87swGQOPzKxrnzvm1myAVuAlP97Ta5Ej6SrlvVb0AEkKnJ2 K+S3gzBwI+zuz1JXJgTvOMZJpPBIcElorr5OJa/T0lH/JvDrzv1/3WKwO0Zh0QlfgIoS FQN1hqVKJ6wW4GdmIvOiOvZ+GjbjBKxqr6HP1hIXDAkmswlmiJ+W/BcgmIxmDzyu+TeM E2QQ== 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=o8LM5FoXrn/GHWimfiGoMXidc6Z9ZU3bJVwIwR21908=; b=eJpn9VVybAb6gd1esNEie4kfDTCYJOZqfIKKNGK+3HYiBtl9PWFL6ZIbBUG77hOTpX fsdmzvN6PdtNd4nWMdsuvG3WiWtk0DSvJrXaB9HAk6lpgHBUtNddWQC8cZ2cmGFVd0rj +aP3EmQc4U0vUcB8ixV7aNBL5k+itup9qHZoVV6MkzCFzb0+JmIpIS18f1rWBndNvPZ2 o1/aUajm1pLFAnN3OluBgecKDxWURIRFe3DrDuJRqmLC++B/nvM5p45i+iSEcvn5e9nO zfuDK6sM4nyKGLPTgSDMw1i7NtFniWvXvRhn3WFw+pEfkHPrRSCZxzesdiL3QFUgELmJ gy3w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XY2I6P1R; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e32 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=o8LM5FoXrn/GHWimfiGoMXidc6Z9ZU3bJVwIwR21908=; b=Ck2BQ1mjK7BaXIlDCjjeX3gwC40O1YWBqjY0k5WkJNDqCZUbs5MlqLUJAIKRt+F/w7 bFAMnGKoR3k+710k/6DbG6AI6EzZzrQ2eSE6AnG0rwhU4dLZIHJ8vRKjOMTGPFLKqzNV l0JSx4U8Bsk752yqe8BN5UTNPuH0B1drZWH3X0s+BK9XQnhyd+yqGb5QH/vgGd/CQbzO vdgzHNwP+VU4+8XznF4crVkcRZW8G8Ym4WSw2MUTTUK+9T2MsMcU/1ahjAgA0IzO2yMB qWY5kwSAV+OAsUXjl6pJw5DIg3kNwh1pRzyVu4xE+vwHwmm+xE2gHmKTtli3yHsTVrR5 b2TA== 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=o8LM5FoXrn/GHWimfiGoMXidc6Z9ZU3bJVwIwR21908=; b=brQ7m/SGDjGryMDR+DZrSxIw5CK/66PX9vyHhNDFBDTY6oakaFz228DxSFjPzZwuud NJYVKBvlhqCA0o7NraFs0s8aWukqfyN2fDDNjLUS4Fsn1VcMFERL+OQ4OddO97qKrytE sQzAkdriwvJ5WCcsLa977mDsjSXwqGPSJ/l/EvBsbvl39G9VDAe0nWHhXeaEaNl+5txF GzKcjUfJGItg9DiAVs3VDf6ceAMSaL2q31q3r20acqvKCgWyYCZq0bR/v6rPnqyHH3Ut Xo1R1kBgTBug9gTZWASnXdLxIe14Vj2XnPrD9Y+HK7bFBuIZu4Sm/eEhKD69Y5lSRiT8 YQtA== 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=o8LM5FoXrn/GHWimfiGoMXidc6Z9ZU3bJVwIwR21908=; b=gBK8Jz6Pllk9LgiDJ2h+ds1khKPiv9QskhM/4hMKMHvA6BVMKRwrW31nwRjzMVCoLg TSPcPbvL+PZis6ZgXIaQPaMjRJ7JIzziggQJ5VB3mgjKM6YP+jwQco/HxSPsi2RkDeng L72JLnbfzvuiJKZn0youpQG3nJ99LA4k959XTiYVJVG5pw+2cJrbUnwZu3c3rfoZkeQW YQJwt1A5aSMX4f1klcqj4LlDpIgrRDxvIKsrf2rKV+/u3RTs3B6L9L+o64+XMea71l+a H5UwPbJB2rha4zpr/xG8dyP02IuZZmxUuTfD2k+Bf/cdCWAQL6ZB0bRK/XZBiF0/jE1m ucCw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531xgcnFzCuQZ1fnVxjX0j2NO7uji7f4dzelosPM5130IkOgkGlA zu03yKX3GMEj20ESkL/oglw= X-Google-Smtp-Source: ABdhPJxUATgFzVGSNbk3EJe2Yj/0/ksYx3GkjaWObNU7cyEvWCdl9rI27G0UsgSCQitOTElcdnxhow== X-Received: by 2002:a25:a0c9:: with SMTP id i9mr14036288ybm.479.1614971928904; Fri, 05 Mar 2021 11:18:48 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:7807:: with SMTP id t7ls5105161ybc.10.gmail; Fri, 05 Mar 2021 11:18:48 -0800 (PST) X-Received: by 2002:a25:3802:: with SMTP id f2mr15623179yba.48.1614971928386; Fri, 05 Mar 2021 11:18:48 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614971928; cv=none; d=google.com; s=arc-20160816; b=NJB/T8AIOnNXp1F0TzlhQdjQ6Uf5kjfrj8dKOUvyPDYS/QKuhy1wHMlU3EwfaVFSPO LP8gbUwoRi5bFJ3wpAvJuskD0v8gV5/eq3mw8x2NU0Mq/uU2SGe+LVNpVJjDlbxoPyDZ LSHU9VqnQcOZjwdkrQv4bfxYrZEOah6E51XpW6gfrxTDeYU+TgUhTHu2ci6CTbWs1v82 EKb/TGYgK5NOY0ET8fT+IRYJ9GNb9ZlG1VsPGojgP3kNKy1OTcWLP49JxK43RkCcPxvb d59oDjLFpFNoot8fKWukwznLT/9rA3k8KBxiq6TURNmgX7AmW6rSOItGnRIVW5gpj1/1 QsaA== 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=3emdb3LoE/zajWYFBL9BVy6daKGEwEi6DU+sNIwbasQ=; b=R4/6nExljjCoFyklVjCals00cV5JhP0rrwyfmBWiOImfobmb5XSa90eOMyEvHW6rX2 sIzDU5LCmlrD7Xafra+2GL6DRDwR0sKYHNww80/dC1Q48nPdfM15+Yg+IlQXRGckEd8A nMt/ULRhO0x3g/xsaL4r+ez7k7RrCCYPfY42fVcEhiZ3+aTnAlTC6wOSokg/4ndt1bgw uiJvPgrGi+FnrefC0RdhELjZ/qzvZ0BabL7vP/Nj9Cm2OvByaHxurAidhN8gPPfT1kEl TTisu0Up6R1T3bRDLoVZA06Dahn1pN4tOoyqK5jYmXOlMP+KQuYUQ5t1HMu6MxAv1fsS +HRA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XY2I6P1R; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e32 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vs1-xe32.google.com (mail-vs1-xe32.google.com. [2607:f8b0:4864:20::e32]) by gmr-mx.google.com with ESMTPS id x7si268593ybm.0.2021.03.05.11.18.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 05 Mar 2021 11:18:48 -0800 (PST) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e32 as permitted sender) client-ip=2607:f8b0:4864:20::e32; Received: by mail-vs1-xe32.google.com with SMTP id b189so1553546vsd.0 for ; Fri, 05 Mar 2021 11:18:48 -0800 (PST) X-Received: by 2002:a67:d709:: with SMTP id p9mr6911798vsj.53.1614971928110; Fri, 05 Mar 2021 11:18:48 -0800 (PST) MIME-Version: 1.0 References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> In-Reply-To: From: Noah Snyder Date: Fri, 5 Mar 2021 14:18:37 -0500 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Jamie Vicary Cc: Kristina Sojakova , Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000018ed9b05bccef4ef" 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=XY2I6P1R; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::e32 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: , --00000000000018ed9b05bccef4ef Content-Type: text/plain; charset="UTF-8" It'd be great to see this done! I've been wanting to see this for a while, but haven't gotten anyone to do it. One remark on that part of the video: the syllepsis gives the proof that the "Brunerie number" is 1 or 2, but it doesn't immediately let you exclude the possibility that it's 1. I think my student Nachiket Karnick and I do understand how to show that the number is 2 (with a much more direct calculation than what's in the second half of Brunerie's thesis, but still using the James construction). I have an outline of an even more direct proof, but the syllepsis is one of the calculations required to make this more direct approach work. Which is all to say that I'm very interested in seeing this result, especially if it meant that related calculations of similar difficulty could be done thereby giving much more direct calculations of the small homotopy groups of spheres. Best, Noah On Fri, Mar 5, 2021 at 1:40 PM Jamie Vicary wrote: > Hi Kristina, that's great. I don't know that anyone's done this before. > > > Given two higher paths p, q : 1_x = 1_x > > I guess you mean p,q:1_(1_x) = 1_(1_x) ? > > Best wishes, > Jamie > > -- > 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/CANr23v3E%2BkaPKgL-So_s_h95KUwSM5i1vPSqzQyEmKa%3D_D46iQ%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/CAO0tDg4oCaZ--OuOVDynT5sXK5jQh1%2BOTM2FNzpx-QLEUg73Ng%40mail.gmail.com. --00000000000018ed9b05bccef4ef Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
It'd be great to see= this done!=C2=A0 I've been wanting to see this for a while, but haven&= #39;t gotten anyone to do it.

One remark on that part of= the video: the syllepsis gives the proof that the "Brunerie number&qu= ot; is 1 or 2, but it doesn't immediately let you exclude the possibili= ty that it's 1.=C2=A0 I think my student Nachiket Karnick and I do unde= rstand how to show that the number is 2 (with a much more direct calculatio= n than what's in the second half of Brunerie's thesis, but still us= ing the James construction).=C2=A0 I have an outline of an even more direct= proof, but the syllepsis is one of the calculations required to make this = more direct approach work.=C2=A0 Which is all to say that I'm very inte= rested in seeing this result,=C2=A0especially if it meant that related calc= ulations of similar=C2=A0difficulty could be done thereby giving much more = direct calculations of the small homotopy groups of spheres.

=
Best,

Noah

<= div class=3D"gmail_quote">
On Fri, Mar= 5, 2021 at 1:40 PM Jamie Vicary <jamievicary@gmail.com> wrote:
Hi Kristi= na, that's great. I don't know that anyone's done this before.<= br>
> Given two higher paths p, q : 1_x =3D 1_x

I guess you mean p,q:1_(1_x) =3D 1_(1_x) ?

Best wishes,
Jamie

--
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/CANr23v3E%2BkaPKgL-So_s_h95KUwS= M5i1vPSqzQyEmKa%3D_D46iQ%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/CAO0tDg4oCaZ--OuOVDynT5sXK5jQh1= %2BOTM2FNzpx-QLEUg73Ng%40mail.gmail.com.
--00000000000018ed9b05bccef4ef--