Dear Kristina,

Am I correct in assuming that the "syllepsis for syllepsis" is the equality
of (4) and (5) in your paper?

Is this related to the fact stable pi_2 is Z/2?

Best,

On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, <
sojakova.kristina@gmail.com> wrote:

> Dear Andrej,
>
> Indeed, my message could have been more user-friendly. The file contains
> alternative proofs of Eckmann-Hilton and syllepsis, together with the
> proofs of the coherences described in Section 8 of
>
> https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf
>
> The last coherence outlined in the paper is what I referred to as
> "syllepsis for syllepsis".
>
> Best,
>
> Kristina
>
> On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
> > Dear Kristina,
> >
> > any chance you could spare a few words in English on the content of your
> formalization? Not everyone reads Coq code for breakfast.
> >
> > Many thanks in advance!
> >
> > Andrej
> >
>
> --
> 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/8e549102-49ca-407f-e95f-22d971f4b9fe%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/CAFL%2BZM-%2Bkw%3D_VbtnLAkmdnEvmJSC8PCUf3NfK6hc%2ByYN_zuszQ%40mail.gmail.com.