![]() |
![]() |
Internal "parametricity" of HoTTAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsBirmingham Algebra Seminar Reading Group in Combinatorics and Probability Contemporary History SeminarOther talksTBC |