Hello David,

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?

We do not yet understand the implications of this result, that's another interesting question I guess. Do you have a conjecture here?

Kristina

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.