scholarly journals The Hole Argument in Homotopy Type Theory

2019 ◽  
Vol 50 (4) ◽  
pp. 319-329 ◽  
Author(s):  
James Ladyman ◽  
Stuart Presnell
Keyword(s):  
General Relativity ◽  
Homotopy Type ◽  
Type Theory ◽  
Space Time ◽  
Scientific Representation ◽  
General Covariance ◽  
Hole Argument ◽  
Homotopy Type Theory ◽  
Mathematics And Physics

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.

scholarly journals Homotopy type-theoretic interpretations of constructive set theories

2019 ◽  
pp. 1-32
Author(s):  
Cesare Gallozzi
Keyword(s):  
Comparative Analysis ◽  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Axiom Of Choice ◽  
Homotopy Type Theory ◽  
Constructive Set Theory

Abstract We introduce a family of (k, h)-interpretations for 2 ≤ k ≤ ∞ and 1 ≤ h ≤ ∞ of constructive set theory into type theory, in which sets and formulas are interpreted as types of homotopy level k and h, respectively. Depending on the values of the parameters k and h, we are able to interpret different theories, like Aczel’s CZF and Myhill’s CST. We also define a proposition-as-hproposition interpretation in the context of logic-enriched type theories. The rest of the paper is devoted to characterising and analysing the interpretations considered. The formulas valid in the prop-as-hprop interpretation are characterised in terms of the axiom of unique choice. We also analyse the interpretations of CST into homotopy type theory, providing a comparative analysis with Aczel’s interpretation. This is done by formulating in a logic-enriched type theory the key principles used in the proofs of the two interpretations. Finally, we characterise a class of sentences valid in the (k, ∞)-interpretations in terms of the ΠΣ axiom of choice.

scholarly journals Reviving the Philosophy of Geometry

2018 ◽  
Author(s):  
David Corfield
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Great Part ◽  
Mathematical Physics ◽  
Relevant Today ◽  
Homotopy Type Theory ◽  
Philosophical Account ◽  
Hard Times ◽  
Anglophone World

In the Anglophone world, the philosophical treatment of geometry has fallen on hard times. This chapter argues that philosophy can come to a better understanding of mathematics by providing an account of modern geometry, including its development of new forms of space, both for mathematical physics and for arithmetic. It returns to the discussions of Weyl and Cassirer on geometry whose concerns are very much relevant today. A way of encompassing a great part of modern geometry via homotopy toposes is discussed, along with the `cohesive’ variant of their internal language, known as `homotopy type theory’. With these tools in place, we can now start to see what an adequate philosophical account of current geometry might look like.

SPACE–TIME ENERGY–MOMENTUM, THE OBSERVER AND UNCERTAINTY IN GENERAL RELATIVITY

2010 ◽  
Vol 19 (14) ◽  
pp. 2353-2359 ◽  
Author(s):  
F. I. COOPERSTOCK ◽  
M. J. DUPRE
Keyword(s):  
General Relativity ◽  
Gravitational Field ◽  
Uncertainty Principle ◽  
Ricci Tensor ◽  
Space Time ◽  
Energy Integral ◽  
New Approach ◽  
Extended Space ◽  
Energy And Momentum

In this essay, we introduce a new approach to energy–momentum in general relativity. Space–time, as opposed to space, is recognized as the necessary arena for its examination, leading us to define new extended space–time energy and momentum constructs. From local and global considerations, we conclude that the Ricci tensor is the required element for a localized expression of energy–momentum to include the gravitational field. We present and rationalize a fully invariant extended expression for space–time energy, guided by Tolman's well-known energy integral for an arbitrary bounded stationary system. This raises fundamental issues which we discuss. The role of the observer emerges naturally and we are led to an extension of the uncertainty principle to general relativity, of particular relevance to ultra-strong gravity.

Homotopy Types

2020 ◽  
pp. 77-106
Author(s):  
David Corfield
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Definite Descriptions ◽  
Homotopy Types ◽  
Homotopy Type Theory

A further innovation is the introduction of an intensional type theory. Here one need not reduce equivalence to mere identity. How two entities are the same tells us more than whether they are the same. This is explained by the homotopical aspect of HoTT, where types are taken to resemble spaces of points, paths, paths between paths, and so on. This allows us to rethink Russell’s definite descriptions. Mathematicians use a ‘generalized the’ in situations where it appears that they might be talking about a multiplicity of instances, but there is essentially a unique instance. Taken together with the ‘univalence axiom’ there results a language in which anything that can be said of a type can be said of an equivalent type. This allows homotopy type theory to become the language of choice for a structuralist, avoiding the need for any kind of abstraction away from multiple instantiations.

scholarly journals Identity in Homotopy Type Theory, Part I: The Justification of Path Induction

2015 ◽  
Vol 23 (3) ◽  
pp. 386-406 ◽  
Author(s):  
James Ladyman ◽  
Stuart Presnell
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Homotopy Type Theory

scholarly journals Homotopy limits in type theory

2015 ◽  
Vol 25 (5) ◽  
pp. 1040-1070 ◽  
Author(s):  
JEREMY AVIGAD ◽  
KRZYSZTOF KAPULKIN ◽  
PETER LEFANU LUMSDAINE
Keyword(s):  
Homotopy Type ◽  
Systematic Study ◽  
Type Theory ◽  
Proof Assistant ◽  
Classical Approach ◽  
Homotopy Type Theory ◽  
The Coq Proof Assistant ◽  
Homotopy Limits ◽  
Coq Proof Assistant

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

Sign in / Sign up

Export Citation Format

Share Document