From: Noah Snyder <nsnyder@gmail.com>
To: Jamie Vicary <jamievicary@gmail.com>
Cc: Kristina Sojakova <sojakova.kristina@gmail.com>,
Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Syllepsis in HoTT
Date: Fri, 5 Mar 2021 14:18:37 -0500 [thread overview]
Message-ID: <CAO0tDg4oCaZ--OuOVDynT5sXK5jQh1+OTM2FNzpx-QLEUg73Ng@mail.gmail.com> (raw)
In-Reply-To: <CANr23v3E+kaPKgL-So_s_h95KUwSM5i1vPSqzQyEmKa=_D46iQ@mail.gmail.com>
[-- Attachment #1: Type: text/plain, Size: 2010 bytes --]
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 <jamievicary@gmail.com> 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.
[-- Attachment #2: Type: text/html, Size: 3105 bytes --]
next prev parent reply other threads:[~2021-03-05 19:18 UTC|newest]
Thread overview: 19+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-03-05 18:27 Kristina Sojakova
2021-03-05 18:40 ` Jamie Vicary
2021-03-05 19:18 ` Noah Snyder [this message]
2021-03-07 18:00 ` Noah Snyder
2021-03-08 8:44 ` Egbert Rijke
2021-03-08 8:53 ` Egbert Rijke
2021-03-08 13:38 ` Noah Snyder
2021-03-08 14:31 ` Kristina Sojakova
2021-03-08 15:10 ` Dan Christensen
2021-03-08 15:15 ` Kristina Sojakova
2021-03-08 15:23 ` Noah Snyder
2021-03-08 15:35 ` Noah Snyder
2021-03-08 15:46 ` Egbert Rijke
2021-03-08 15:49 ` Kristina Sojakova
2021-03-08 16:25 ` Dan Christensen
2021-03-08 16:27 ` Kristina Sojakova
2021-03-08 16:38 ` Kristina Sojakova
2021-03-08 16:54 ` Egbert Rijke
2021-03-08 19:55 ` 'Favonia' via Homotopy Type Theory
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=CAO0tDg4oCaZ--OuOVDynT5sXK5jQh1+OTM2FNzpx-QLEUg73Ng@mail.gmail.com \
--to=nsnyder@gmail.com \
--cc=homotopytypetheory@googlegroups.com \
--cc=jamievicary@gmail.com \
--cc=sojakova.kristina@gmail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).