University of Birmingham > Talks@bham > Lab Lunch > Internal "parametricity" of HoTT

Internal "parametricity" of HoTT

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.