A couple of years ago, I have experimented with a system based on a similar idea. See page 7 here: https://dl.dropboxusercontent.com/u/7730626/ett3.pdf The reduction rules for transporting over a type equality e : A ≈ B can indeed be defined purely by induction on e, as on page 9. (And, if you want to add univalence, then equivalence will be a constructor for this type, in which case the transport will reduce to the function given in this constructor.) Cheers, Andrew On Tuesday, July 19, 2016 at 9:28:14 PM UTC+2, v v wrote: > > 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. > >