|Project title||Applying Homotopy Type Theory in Logic, Metaphysics, and Philosophy of Physics|
|Dates||September 2013 to September 2016|
|Funder||Leverhulme Trust Research Project Grant|
Homotopy Type Theory is an exciting new project in mathematics, founded by Steve Awodey and Vladimir Voevodsky. It assembles ideas from logic, computer science, and geometry to build a new approach to the basic ideas of mathematics.
It is radically different from the common set-theoretic foundational systems used by mathematicians, since it uses constructive rather than classical logic, type theory rather than set theory, and provides intensional rather than extensional definitions.
The aim of our three-year project is first to study and develop the philosophical underpinnings of Homotopy Type Theory to ensure that it provides a coherent philosophical foundation for mathematics. We then investigate the consequences of adopting this alternative foundation for questions in metaphysics, the structuralist account of philosophy of mathematics, and applications to physics.
Confirmed speakers include Urs Schreiber, Teru Thomas, James Ladyman and Stuart Presnell. More details to follow.