Hello David, On 7/8/2023 4:00 PM, David Roberts wrote: > Dear Kristina, > > Am I correct in assuming that the "syllepsis for syllepsis" is the > equality of (4) and (5) in your paper? Indeed, we show the equality between (4) and (5). > > 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, > 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/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com.