Re: [HoTT] Syllepsis in HoTT

[Noah Snyder <nsnyder@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2389 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 3540 bytes --]