The Hole Argument in Homotopy Type Theory

James Ladyman, Stuart Presnell

Research output: Contribution to journalArticle (Academic Journal)peer-review

2 Citations (Scopus)
227 Downloads (Pure)


The Hole Argument is primarily about the meaning of general covariance in general relativity. As such it raises many deep issues about identity in mathematics and physics, the ontology of space–time, and how scientific representation works. This paper is about the application of a new foundational programme in mathematics, namely homotopy type theory (HoTT), to the Hole Argument. It is argued that the framework of HoTT provides a natural resolution of the Hole Argument. The role of the Univalence Axiom in the treatment of the Hole Argument in HoTT is clarified.
Original languageEnglish
Pages (from-to)319-329
Number of pages11
JournalFoundations of Physics
Early online date4 Oct 2019
Publication statusPublished - 1 Apr 2020

Structured keywords

  • Centre for Science and Philosophy
  • Centre_for_science_and_philosophy


  • Hole argument
  • Homotopy type theory
  • General covariance
  • Univalence


Dive into the research topics of 'The Hole Argument in Homotopy Type Theory'. Together they form a unique fingerprint.

Cite this