## 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
Note that ex-directory lists are not shown. |
## Other listsSoCS PhD Research Training Sessions Cond. Mat. seminar Algebra Seminar## Other talksThe imprint of their explosions: Using supernova remnants to understand stellar death Discrete models of cellular mechanics The highwater algebra |