![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Sean Moss, DPMMS
Monday 17 October 2016, 16:20-17:00
From intuitionism to synthetic homotopy theory
- đ¤ Speaker: Sean Moss, DPMMS
- đ Date & Time: Monday 17 October 2016, 16:20 - 17:00
- đ Venue: MR3, CMS
Abstract
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.
Series This talk is part of the DPMMS PhD student colloquium series.
Included in Lists
- All CMS events
- bld31
- CMS Events
- DPMMS info aggregator
- DPMMS PhD student colloquium
- Hanchen DaDaDash
- Interested Talks
- MR3, CMS
Note: Ex-directory lists are not shown.