Thank you for spotting this typo. It is supposed to be P_1. I have corrected the slides. > On Jul 19, 2016, at 8:16 PM, Michael Shulman wrote: > > Can you explain the idea on the last slide a little more? Did you > actually mean to say that R and "transportb0 R e" both have type P2, > or should one of them have had type P1? If the latter, then how can > we tell what type(s) "transportb0 R e" is allowed to have based on > knowing the types of R and e? > > On Tue, Jul 19, 2016 at 2:18 PM, Vladimir Voevodsky wrote: >> Hello, >> >> the slides of my FOMUS talk that have started the discussion about >> equalities are now available at my website >> https://www.math.ias.edu/vladimir/lectures . >> >> Vladimir. >> >> -- >> 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 HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.