BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The interpretation of intuitionistic type theory in locally cartes
 ian closed categories: an intuitionistic approach - Peter Dybjer
DTSTART:20080627T130000Z
DTEND:20080627T140000Z
UID:TALK12452@talks.cam.ac.uk
CONTACT:Tom Ridge
DESCRIPTION:I [Peter Dybjer] will give an intuitionistic view of Seely's i
 nterpretation of Martin-Löf type in locally cartesian closed categories. 
 The point is to use Martin-Löf type theory itself as metalanguage\, and a
  constructive notion of category\, a so called E-category. As a categorica
 l substitute for the formal system of Martin-Löf type theory I will use E
 -categories with families\, and discuss how to interpret such categories i
 n E-locally cartesian closed categories. This is joint work with Alexandre
  Buisse\, who has formalized the key part of this proof in Coq.\n 
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR