Internal "parametricity" of HoTT

Add to your list(s) Download to your calendar using vCal

• Auke Booij
• Wednesday 24 February 2016, 13:00-14:00
• CS 217.

If you have a question about this talk, please contact Uday Reddy.

Parametricity tells us that in dependent type theory, a term f_X : X → X (where X is a type parameter) must be equal to the identity. However, parametricity theory is external to type theory. Additionally, assuming the law of excluded middle, we are able to exhibit function family f_X with f_Bool = flip. I have proved a converse to this: if we are given a function family f_X that is not the identity on the booleans, then we get an instance of the law of excluded middle. In this sense, non-parametricity can be seen as a constructive taboo.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.