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 <shu...@sandiego.edu> 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 <vla...@ias.edu> 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 HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.