BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:Internal "\;parametricity"\; of HoTT - Au
ke Booij
DTSTART:20160224T130000Z
DTEND:20160224T140000Z
UID:TALK2011AT
URL:/talk/index/2011
DESCRIPTION:Parametricity tells us that in dependent type theo
ry\, a term f_X : X -> X (where X is a type parame
ter) must be equal to the identity. However\, para
metricity theory is external to type theory. Addit
ionally\, assuming the law of excluded middle\, we
are able to exhibit function family f_X with f_Bo
ol = flip.\nI have proved a converse to this: if w
e 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\, no
n-parametricity can be seen as a constructive tabo
o.
LOCATION:CS 217
CONTACT:Uday Reddy
END:VEVENT
END:VCALENDAR