BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Homotopy Type Theory and Univalent Foundations of Mathematics I - 
 Chris Kapulkin\, University of Pittsburgh
DTSTART:20110628T131500Z
DTEND:20110628T141500Z
UID:TALK31965@talks.cam.ac.uk
CONTACT:Nathan Bowler
DESCRIPTION:This series of talks is an introduction to Homotopy Type Theor
 y and the Univalent Foundations of Mathematics. This new area of research 
 develops a beautiful connection between algebraic topology (homotopy theor
 y) and theoretical computer science (type theory).\n\nThe first talk will 
 be a survey on Homotopy Type Theory. We will discuss the semantics of type
  theory in different presentations of homotopy theory (e.g. Quillen model 
 categories\, higher categories) as well as some constructions on syntax in
 dicating partial completeness of these semantics.\n
LOCATION:MR13\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR