BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From intuitionism to synthetic homotopy theory - Sean Moss\, DPMMS
DTSTART:20161017T152000Z
DTEND:20161017T160000Z
UID:TALK68335@talks.cam.ac.uk
CONTACT:Jack Smith
DESCRIPTION:Intuitionistic logic\, based on the philosophy of Intuitionism
 \, is often summarized as proof without the Law of the Excluded Middle. An
  intuitionistic proof carries constructive information about its conclusio
 n\, and different proofs will yield different such information. This is a 
 mathematics where the proofs themselves matter more than the mere truth of
  propositions. I will discuss how the idea of proof-relevant mathematics h
 as evolved into the new field of Homotopy Type Theory\, which is intended 
 to be a new formal foundation for mathematics and\, miraculously\, support
 s a kind of synthetic (or axiomatic) version of the homotopy theory of spa
 ces.
LOCATION:MR3\, CMS
END:VEVENT
END:VCALENDAR