The Hole Argument in Homotopy Type Theory

James Ladyman; Stuart Presnell

doi:10.1007/s10701-019-00293-9

The Hole Argument in Homotopy Type Theory

James Ladyman, Stuart Presnell

Department of Philosophy

Research output: Contribution to journal › Article (Academic Journal) › peer-review

2 Citations (Scopus)

227 Downloads (Pure)

Abstract

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 language	English
Pages (from-to)	319-329
Number of pages	11
Journal	Foundations of Physics
Volume	50
Early online date	4 Oct 2019
DOIs	https://doi.org/10.1007/s10701-019-00293-9
Publication status	Published - 1 Apr 2020

Structured keywords

Centre for Science and Philosophy
Centre_for_science_and_philosophy

Keywords

Hole argument
Homotopy type theory
General covariance
Univalence

Access to Document

10.1007/s10701-019-00293-9

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via Springer at https://link.springer.com/article/10.1007/s10701-019-00293-9 . Please refer to any applicable terms of use of the publisher.
Final published version, 301 KBLicence: CC BY

Handle.net

Persistent link

Embargoed Document

Full-text PDF (accepted author manuscript)
Accepted author manuscript, 239 KB
Request copy

Professor James A C Ladyman
- James.Ladymanbristol.acuk
- Department of Philosophy - Professor
Person: Academic

Cite this

@article{b01697090a984a1c9b5f018d81c125c2,

title = "The Hole Argument in Homotopy Type Theory",

abstract = "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.",

keywords = "Hole argument, Homotopy type theory, General covariance, Univalence",

author = "James Ladyman and Stuart Presnell",

year = "2020",

month = apr,

day = "1",

doi = "10.1007/s10701-019-00293-9",

language = "English",

volume = "50",

pages = "319--329",

journal = "Foundations of Physics",

issn = "0015-9018",

publisher = "Springer Netherlands",

}

TY - JOUR

T1 - The Hole Argument in Homotopy Type Theory

AU - Ladyman, James

AU - Presnell, Stuart

PY - 2020/4/1

Y1 - 2020/4/1

N2 - 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.

AB - 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.

KW - Hole argument

KW - Homotopy type theory

KW - General covariance

KW - Univalence

U2 - 10.1007/s10701-019-00293-9

DO - 10.1007/s10701-019-00293-9

M3 - Article (Academic Journal)

SN - 0015-9018

VL - 50

SP - 319

EP - 329

JO - Foundations of Physics

JF - Foundations of Physics

ER -

The Hole Argument in Homotopy Type Theory

Abstract

Structured keywords

Keywords

Access to Document

Handle.net

Embargoed Document

Fingerprint

Profiles

Professor James A C Ladyman

Cite this