Homotopy Type Theory project

Research project key facts
Project title Applying Homotopy Type Theory in Logic, Metaphysics, and Philosophy of Physics
School Arts
Department Philosophy
Dates September 2013 to September 2016
Funder Leverhulme Trust Research Project Grant
Contact James Ladyman

More about this project

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.


  • Workshop title: Applying Homotopy Type Theory to physics,
  • Date: 7 to 8 April 2015
  • Venue: University of Bristol

Confirmed speakers include Urs Schreiber, Teru Thomas, James Ladyman and Stuart Presnell. More details to follow.


People involved in this project

Principal investigator:

Postdoctoral research assistant: