## 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:Note that ex-directory lists are not shown. |
## Other listsMidlands Logic Seminar Jane Langdale Bravo## Other talksFischer Groups Privileged side-channel attacks for enclave adversaries Subgroups of the Monster How hard is LWE anyway? Operator Preconditioning and Some Recent Developments for Boundary Integral Equations An attack on ECDSA using lattice techniques |