BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Presheaf models of type theory - Ian Orton (University of Cambridg
 e)
DTSTART:20161118T104500Z
DTEND:20161118T114500Z
UID:TALK69249@talks.cam.ac.uk
CONTACT:Ian Orton
DESCRIPTION:In this talk I will present the standard way of constructing a
  presheaf model of type theory over a small category C.\n\nI will begin wi
 th a quick recap of the basics of type theory: contexts\, types\, terms et
 c. I will then explain what it means to have a model of type theory and wi
 ll describe the basics of the presheaf model of type theory. We will then 
 look at how to model various type formers such as: dependent sums\, depend
 ent products\, identity types and universes.
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
END:VEVENT
END:VCALENDAR