## Internal "parametricity" of HoTTAdd 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
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Lab Lunch
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsBirmingham Algebra Seminar Reading Group in Combinatorics and Probability Contemporary History Seminar## Other talksTBC |