BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Categorical models of dependent types - Ian Orton (University of C
 ambridge)
DTSTART:20160122T110000Z
DTEND:20160122T120000Z
UID:TALK63830@talks.cam.ac.uk
CONTACT:Ian Orton
DESCRIPTION:I will run through the basics of how dependent types are model
 led inside a category\, including how to construct dependent sums and prod
 ucts\, and how to represent substitution. I will then discuss the coherenc
 e issues relating to substitution and how these can be resolved using a ca
 tegory with families (CwF) or similar construction (e.g. comprehension cat
 egories\, categories with attributes etc).\n\nCovering:\n\n  * Dependent t
 ypes as fibrations\n  * Dependent sum/product as adjoints to the pullback 
 functor\n  * Substitution via pullback and its problems\n  * Fixing those 
 problems with categories with families (CwFs)\n\nPrerequisites:\n\n  * Bas
 ic category theory (functors and pullbacks)\n  * Basic knowledge of depend
 ent types
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
END:VEVENT
END:VCALENDAR