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:DPMMS PhD student colloquium
SUMMARY:From intuitionism to synthetic homotopy theory - S
ean Moss\, DPMMS
DTSTART;TZID=Europe/London:20161017T162000
DTEND;TZID=Europe/London:20161017T170000
UID:TALK68335AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/68335
DESCRIPTION:Intuitionistic logic\, based on the philosophy of
Intuitionism\, is often summarized as proof withou
t the Law of the Excluded Middle. An intuitionisti
c proof carries constructive information about its
conclusion\, and different proofs will yield diff
erent such information. This is a mathematics wher
e the proofs themselves matter more than the mere
truth of propositions. I will discuss how the idea
of proof-relevant mathematics has evolved into th
e new field of Homotopy Type Theory\, which is int
ended to be a new formal foundation for mathematic
s and\, miraculously\, supports a kind of syntheti
c (or axiomatic) version of the homotopy theory of
spaces.
LOCATION:MR3\, CMS
CONTACT:Jack Smith
END:VEVENT
END:VCALENDAR