BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A functional interpretation of type theory - Tamara von Glehn\, DP
 MMS
DTSTART:20131119T141500Z
DTEND:20131119T151500Z
UID:TALK47754@talks.cam.ac.uk
CONTACT:Julia Goedecke
DESCRIPTION:Dependent types are interpreted in a category as certain maps\
 , called fibrations\, where substitution corresponds to pullback\, quantif
 iers correspond to adjoints to pullback\, and identity types arise from a 
 weak\nfactorisation system.\nIn this talk I will look at how\, given such 
 a category C with fibrations modelling dependent type theory\, we can get 
 another model in the category of polynomials in C. These can be thought of
  as types with quantifiers\nfreely added\, with maps analogous to implicat
 ion in Gödel's Dialectica interpretation of arithmetic.
LOCATION:MR5\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR