University of Cambridge > Talks.cam > DPMMS PhD student colloquium > From intuitionism to synthetic homotopy theory

From intuitionism to synthetic homotopy theory

Add to your list(s) Download to your calendar using vCal

  • UserSean Moss, DPMMS
  • ClockMonday 17 October 2016, 16:20-17:00
  • HouseMR3, CMS.

If you have a question about this talk, please contact Jack Smith.

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 conclusion, 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 has evolved into the new field of Homotopy Type Theory, which is intended to be a new formal foundation for mathematics and, miraculously, supports a kind of synthetic (or axiomatic) version of the homotopy theory of spaces.

This talk is part of the DPMMS PhD student colloquium series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity