BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Category Theory Seminar
SUMMARY:Homotopy Type Theory and Univalent Foundations of
Mathematics II - Chris Kapulkin\, University of Pi
ttsburgh
DTSTART;TZID=Europe/London:20110629T141500
DTEND;TZID=Europe/London:20110629T151500
UID:TALK31966AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/31966
DESCRIPTION:This series of talks is an introduction to Homotop
y Type Theory and the Univalent Foundations of Mat
hematics. This new area of research develops a bea
utiful connection between algebraic topology (homo
topy theory) and theoretical computer science (typ
e theory).\n\nThe second talk will serve an introd
uction to the Univalent Foundations. This program
started by Vladimir Voevodsky (IAS\, Princeton) pr
ovides new interesting foundations of mathematics
(based on type theory)\, naturally formalizing cat
egorical and higher-categorical thinking. The main
purpose of this project is to have a language bas
ed on homotopy types (as opposed to sets) that wou
ld enable one to easily prove results from homotop
y theory using a proof assistant such as Coq. This
can be accomplished by adding the Univalence Axio
m to the standard set of rules of type theory. In
the talk we will discuss the Univalence Axiom toge
ther with some of its basic consequences\, higher
inductive types\, and a type theoretic proof of $\
\pi_1 (S^1) = \\mathbb{Z}$.
LOCATION:MR13\, Centre for Mathematical Sciences
CONTACT:Nathan Bowler
END:VEVENT
END:VCALENDAR