1 Introduction

Developments in the applied sciences give new solutions to some practical problems and streamline old solutions to others. Similarly, developments in the formal sciences give new solutions to some conceptual problems and streamline old solutions to others. The recent confluence of algebraic topology, n-category theory, computer science, logic, and more into a mathematical research program called homotopy type theory (HoTT) offers tools for tackling a variety of conceptual problems.Footnote 1 Indeed, the subtle notions of sameness at play in homotopy theory and the abstract formality of type theory suggest that these tools can be profitably applied to any problems involving sameness that admit formal statements. In this paper I consider the problem of when two Lorentzian manifolds represent the same spacetime using tools from HoTT.

Specifically, I return to the problems posed by John Earman and John Norton in their influential discussion of this problem in the context of modern spacetime theories, particularly general relativity (GR) [12]. They are concerned to show that if you adopt a substantivalist account of spacetime, taking spacetime points to be real, then you are faced with two dilemmas. For if you are a substantivalist, they claim, you must take two Lorentzian manifolds to represent the same spacetime just in case they are identical.Footnote 2 But if this is so then for any Lorentzian manifold there is some other, isometric Lorentzian manifold that represents an empirically indistinguishable but metaphysically distinct way the world could be. Worse, these worlds are also dynamically indistinguishable: one satisfies the laws of GR just in case the other one does. So at any moment there are infinitely many distinct possible futures—a massive failure of determinism. The first problem presses a choice between verificationism and substantivalism and the second a choice between determinism and substantivalism. Even if you are happy to take the substantivalist horn of the verificationist dilemma, the extremity of determinism’s failure in the indeterminism dilemma should give you second thoughts about hanging on to substantivalism.

The most popular defenses of substantivalism respond to these dilemmas by supplying a sophisticated modal semantics in which distinct Lorentzian manifolds needn’t represent distinct spacetimes [3]. From the HoTT perspective, however, this response is underspecified; in particular, it leaves open physically significant questions about the ways in which the representatives of some spacetime are related. The verificationist dilemma is concerned with a yes-or-no question: “must distinct Lorentzian manifolds represent distinct spacetimes?” The indeterminism dilemma, by contrast, concerns the way in which the configuration of one region of spacetime depends on the configuration of other regions, and this is more than a yes-or-no question. So a response to the first dilemma requires more than an answer the second dilemma does. That is, two views can respond to the verificationist dilemma in the same way while disagreeing about the indeterminism dilemma.

In this paper I establish this by way of example. On the most straightforward reading of Earman and Norton’s arguments in HoTT, the verificationist dilemma does not go through but the indeterminism dilemma does. It therefore differs from popular responses that take both dilemmas to have similar resolutions. Sections 3 and 4 review these popular responses and compare them with the natural reading in HoTT. In short, the natural resolution of the verificationist dilemma from the HoTT point of view is essentially the same as the resolution recently argued for by Weatherall [27]. The verificationist dilemma fails because isometric Lorentzian manifolds represent the same physical state of affairs, so Earman and Norton’s putative counterexamples to verificationism aren’t mathematically distinct models after all. The indeterminism dilemma, on the other hand, takes a different form in HoTT than in other formalisms. This is because the notion of determinism depends on the notion of uniqueness, and thus on the notion of identity, which HoTT treats differently from other formalisms. On the natural formulation of determinism in HoTT, and supposing that the category of models of GR is the category of Lorentzian manifolds satisfying the Einstein equation, it follows that GR is indeterministic, regardless of whether one is a substantivalist or not. Since GR isn’t indeterministic, one of those suppositions must be wrong. In Sect. 5 I give an alternative category of models for GR and indicate one reason, independent of the hole argument, to think that this is the category of models that’s used in practice. So the reading of the hole argument that I give below is not just some position in logical space. Rather, on this reading, the hole argument draws attention to structure that can easily be—and often is—neglected by formal treatments that aren’t sensitive to the distinctions HoTT is designed to handle.

2 Tuples and Equality in HoTT

I have been referring to the “natural reading” of various claims in HoTT. The point of this section is to sketch the features of HoTT that make a difference in these readings—in particular, its treatment of identity.Footnote 3 I mean to use HoTT as a drop-in replacement for standard logics in the formalization of informal or semi-formal mathematical discourse. The debate over Earman and Norton’s arguments involves, in part, a distinction between straightforward and sophisticated formalizations of such discourse, and sophisticated formalizations are often required to justify their sophistication. But whether some formalization counts as sophisticated depends on the formal system it uses. In this paper I’m interested in straightforward formalizations in HoTT.

I am adopting HoTT both for reasons of convenience and reasons of substance. The convenience comes from economy of expression. The original motivation for HoTT was, in part, a desire for a formalism that more accurately represents the way higher category theorists and homotopy theorists reason about their domains and the phenomena they encounter there. In particular, the treatment of identity in HoTT gives a clean and concise expression of the features of identity found in these areas, and these are the features that interest me here. Thus, in using HoTT as a formal system I mean to avoid more complicated formal treatments, such as the n-category theory the title alludes to. A more substantial assumption I’m making is that straightforward formalization in HoTT is the proper formalization of the informal arguments below. This assumption needn’t make any reference to HoTT, strictly speaking; by design, straightforward formalization in HoTT reproduces the appropriate expressions in more traditional formalizations of higher category theory—expressions referred to in these contexts as “homotopically correct”. Justifying these expressions as appropriate is a project beyond the scope of this paper; I appeal to the authority of higher category theorists for this. The existence of HoTT as a formal system gives one way that this practice can be made precise and consistent.

Now Earman and Norton are concerned with what they call local spacetime theories. A model of such a theory is a tuple of the form \((M, g, g^{\prime }, \dotsc )\) for some smooth manifold M and geometric structures \(g, g^{\prime }, \dotsc \). The central example in our discussion is GR, whose models are usually formalized as a pair (M, g) with g a Lorentzian metric. We can formulate most other field theories using similar kinds of tuples. Much of Earman and Norton’s discussion goes through straightforwardly in HoTT, so we will confine our remarks to the most important differences. These are all concerned with equality, which differs in HoTT from the equality relation in first order logic that lies behind Earman and Norton’s formalization. Since these differences arise already in simpler non-geometric settings we take one of these (from [27]) as a toy example. Consider the theory of groups, which we can model with triples \((S, \times , e)\) of a set S, a group operation \(\times \) on S, and an element e of S that’s a unit for the group operation. We would like an analysis of when two groups are equal. Two groups \((S, \times , e)\) and \((S', \times ', e')\) should be equal if they have the same underlying set equipped with the same group operation and unit element. In this section we make this rough criterion precise.

Traditionally, mathematics is formalized using first order logic combined with a set theory like Zermelo-Fraenkel set theory (ZF). The language of ZF is untyped, so whether a formula is well-formed depends only on whether every logical operator that appears has been supplied the right number of arguments. HoTT, by contrast, is a type theory, which means that expressions can only be well-formed if they also respect the types of their subexpressions. In this sense, it is less flexible than traditional formalisms. For example, consider the following four expressions:

  1. 1.

    3 is prime.

  2. 2.

    4 is prime.

  3. 3.

    the set of real numbers is prime.

  4. 4.

    the set of all sets not containing themselves is prime.

Traditional formalisms and HoTT both agree that (1) is true, (2) is false, and (4) is ill-formed. They disagree on (3): while it is false in traditional formalisms—i.e., the set of real numbers is not contained in the extension of the primehood predicate—it is ill-formed in HoTT. A set is just not the type of thing that can be prime. This is just one of many calls that a formal system has to make. Any system must count (4) as ill-formed, on pain of Russell’s paradox, but some restrictions are negotiable. While I take it that (3) is mathematically meaningless, it’s obviously not a fatal problem if some formal system is liberal enough to grant (3) a truth value, as the success of traditional formalisms shows. HoTT is more restrictive, classing (3) with (4). This extra restriction means that the well-formation of some expressions depends on the truth of others: we can only intelligibly ask if x is prime if we know that x is a natural number.

The natural formalization of mathematical claims into HoTT in a way that respects typing restrictions is described by the propositions-as-types paradigm.Footnote 4 On this paradigm, mathematical statements are themselves types, alongside the types of natural numbers, prime numbers, Lorentzian manifolds, and so on. To assert that some proposition is true is to assert the existence of some term of the type representing that proposition. Write ‘p : P’ to mean that p is a term of type P; if P represents a proposition then ‘p : P’ formalizes the assertion that P. Logical constructions on statements are then of a piece with mathematical constructions on objects. So, for example, for any sets X and Y there is a set \(X \times Y\) of pairs (x, y) such that x is an element of X and y an element of Y. And for any propositions P and Q there is a proposition \(P \times Q\), the conjunction of P and Q. If p : P and q : Q then \((p, q) : P \times Q\), which formalizes the logical inference from P and Q to the conjunction \(P \times Q\). Similarly, the conditional “if P then Q” is formalized by the type \(P \rightarrow Q\) of functions from the type P to the type Q, and the statement ‘\(f : P \rightarrow Q\)’ formalizes the assertion that P implies Q.

Generalizing the propositions-as-types paradigm to quantified logic means introducing types that depend on terms of other types. The proposition “3 is prime” involves a term 3 of type \(\mathbb {N}\) and a predicate ‘is prime’ that takes one argument of type \(\mathbb {N}\). In the propositions-as-types paradigm the proposition “3 is prime” is thus represented by a type that is constructed from a term and a predicate of these types. This is where the typing restrictions play a role: you cannot combine a term representing a set with the ‘is prime’ predicate, for example, so there is no type that could represent a claim like “the set of real numbers is prime”. This statement is just ill-formed.

So in the propositions-as-types paradigm the claim that the groups \((S, \times , e)\) and \((S', \times ', e')\) are equal should be represented by a type, and the groups are in fact equal if this type has a term. The expression ‘\(x = y\)’ must be well-typed, and it is only meaningful if x and y have the same type. Similarly, if we would like to ask whether some structure on A is the same as some structure on B, that question depends on A and B being equal. So if we suppose for now that \(S = S'\), then we only need to check that the group structures are the same. But this question is only meaningful because we know that \(S = S'\), so the answer will depend on this fact. That is, our supposition amounts to the hypothesis that \(p : S = S'\). Since p is a term of an equality type, I will also call it an equality.

The logic of equality-dependence figures into the inference rules of HoTT alongside the inference rules for conjunction, disjunction, and so on [24, Sect. 1.12]. Equality is reflexive, so for any term x there must be an equality \(\mathsf {refl}(x) : x = x\) between x and itself. Symmetry and transitivity of equality give new equalities from old. The other rules implement equality’s usual substitutional inferential role. Take, for example, the indiscernibility of identicals. For any objects a and \(a'\) of type A and predicate P applying to elements of A, if a and \(a'\) are equal then P(a) implies \(P(a')\). More generally, suppose that P is instead some construction that takes an object a of type A as input and gives some collection P(a) as output. Then if a and \(a'\) are equal, any object in P(a) must be an object in \(P(a')\). So for any equality \(p : a = a'\) there is a function \(p_{*} : P(a) \rightarrow P(a')\) that sends each object in P(a) to the corresponding object in \(P(a')\), obtained by substitution of \(a'\) for a according to p. By the rules of equality dependence, the function \((\mathsf {refl}(a))_{*} : P(a) \rightarrow P(a)\) induced by the equality \(\mathsf {refl}(a) : a = a\) is just the identity function \(\mathsf {id}_{P(a)}\).

Applying the indiscernibility of identicals to our hypothetical equality \(p : S = S'\), we can sensibly ask and answer questions about whether they are equipped with the same structure. They have the same group operation if \(p_{*}(x \times y) = p_{*}(x) \times ' p_{*}(y)\) for all x and y in S, and they have the same unit element if \(p_{*}(e) = e'\). In order to complete this approach, then, we need some way of producing an equality of sets to use after discharging our hypothesis. In a traditional formalism, this is done with the axiom of extensionality: two sets are the same just in case they have all the same elements. But in HoTT this would require asking whether objects of S are also objects of \(S'\), and this question risks being ill-formed. Indeed, since the expression ‘\(x = y\)’ is only meaningful when x and y have the same type, if x is an element of S and y an element of \(S'\) then the meaning of ‘\(x = y\)’ depends on our already knowing that S and \(S'\) are equal, which is our question. And if this expression is meaningless, it can’t be used as a consequent in the axiom of extensionality. So phrasing extensionality in this way would be circular.

The extensionality principle in HoTT is the univalence axiom. For sets, this axiom says the following. Suppose that we had some bijection \(f : S \rightarrow S'\). Then each element s of S corresponds to a unique element f(s) of \(S'\). And it’s hard to say what more we could ask of an equality of type \(S = S'\). Any statement about s can be uniquely translated into a statement about f(s), and as such any statement about S can be uniquely translated into one about \(S'\)salva veritate. This arguably exhausts the content of an equality statement. So, more formally, we suppose

The univalence axiom (for sets) For every bijection \(f : A \rightarrow B\) of sets A and B there is an equality \(\mathsf {ua}(f) : A = B\) such that \((\mathsf {ua}(f))_{*} = f\).

So all it takes to get started in showing that \((S, \times , e) = (S', \times ', e')\) is to provide a bijection \(S \rightarrow S'\).

We now have all the tools necessary to show that two groups are equal. Applying this machinery to a concrete example, we can construct an equality of groups \((\mathbb {Z}, +, 0)\) and \((\mathbb {Z}, +', 1)\), where \(+'\) is defined by \(n +' m = n + m - 1\). These groups are equal just in case they have equal underlying sets equipped with equal group structures. To produce an equality of type \(\mathbb {Z} = \mathbb {Z}\), it suffices by univalence to give a bijection \(\phi : \mathbb {Z} \rightarrow \mathbb {Z}\). Take \(\phi : \mathbb {Z} \rightarrow \mathbb {Z}\) to be the map defined by \(\phi (n) = n+1\), giving a term \(\mathsf {ua}(\phi ) : \mathbb {Z} = \mathbb {Z}\). For any n and m in \(\mathbb {Z}\) we have

$$\begin{aligned} (\mathsf {ua}(\phi ))_{*}(n + m)= & {} \phi (n + m) = n + m + 1 = \phi (n) \\&+' \phi (m) = (\mathsf {ua}(\phi ))_{*}(n) +' (\mathsf {ua}(\phi ))_{*}(m) \end{aligned}$$

since \((\mathsf {ua}(\phi ))_{*} = \phi \) by univalence. And similarly

$$\begin{aligned} (\mathsf {ua}(\phi ))_{*}(0) = \phi (0) = 1 \end{aligned}$$

Taking these three together, we have a term

$$\begin{aligned} \left( \mathsf {ua}(\phi ), \mathsf {refl}(+'), \mathsf {refl}(1)\right) : (\mathbb {Z}, +, 0) = (\mathbb {Z}, +', 1) \end{aligned}$$

So \(\phi \) gives a standard of comparison according to which the underlying sets of the groups \((\mathbb {Z}, +, 0)\) and \((\mathbb {Z}, +', 1)\) are the same, and when we use this standard to compare the group structures on either group we have equalities \(\mathsf {refl}(+')\) and \(\mathsf {refl}(1)\) asserting that they have the same group multiplication and unit.

This result might surprise you. The integers 0 and 1 are different, and so (you might think) the groups \((\mathbb {Z}, + , 0)\) and \((\mathbb {Z}, +', 1)\) differ in their third entries and hence are different groups. But this inference fails. Recall that to even intelligibly ask the question of whether the third entries of some tuples are the same or different, we must know that they have the same type. And this depends on our knowing that the first entries of each tuple are the same. It depends on it in the strong sense that we use the equality of the first entries to compare the third entries. So it’s true that \(0 \not = 1\), but it’s false that \((\mathsf {ua}(\phi ))_{*}(0) \not = 1\), and the second statement is the relevant formalization of the statement “\((\mathbb {Z}, +, 0)\) and \((\mathbb {Z}, +', 1)\) differ in their third entries”. Appeal to \(0 \not = 1\) shows that there is no equality of the form \((\mathsf {refl}(\mathbb {Z}), -)\) between the groups \((\mathbb {Z}, +, 0)\) and \((\mathbb {Z}, +', 1)\). But this is not to say that there is no equality at all.

On a straightforward reading of the HoTT formalism, Earman and Norton’s verificationist is similar to the mistaken argument of the previous paragraph; it shows that there is no equality of tuples with a \(\mathsf {refl}\) in the first entry and concludes from this that the tuples are distinct. This inference fails in the case of GR just as it does in the case of groups. But this doesn’t mean that the indeterminism dilemma also fails. The same straightforward reading of HoTT leads right to indeterminism in exactly the places Earman and Norton say it does.

3 The Verificationist Argument

Earman and Norton pitch the verificationist argument as a dilemma for substantivalists: admit observationally indistinguishable but distinct states of affairs or deny substantivalism. However, subsequent philosophical work has shown that this argument is better thought of as a reductio, for there is more than one way to avoid both horns of the dilemma. In this section, I use HoTT to articulate one response to the verificationist argument, according to which diffeomorphic Lorentzian manifolds represent not only the same physical state of affairs but also the same mathematical object. Thus Earman and Norton’s argument does not give an example of observationally indistinguishable but distinct states of affairs. Weatherall has recently offered a similar response to Earman and Norton [27]. In this section I contrast his response and mine, and in subsequent sections I draw out some consequences of the difference.

Here is one way to state the verificationist argument. Suppose we take a model of GR to be a pair (M, g) of a smooth manifold M and a Lorentzian metric g on M. Let \(\phi : M \rightarrow M\) be any nontrivial diffeomorphism. Then Earman and Norton offer the following reductio:

  1. 1.

    Substantivalism is true.

  2. 2.

    By (1), distinct mathematical objects represent distinct possible states of affairs.

  3. 3.

    (M, g) and \((M, \phi _{*}(g))\) are distinct mathematical objects.

  4. 4.

    By (2) and (3), (M, g) and \((M, \phi _{*}(g))\) represent distinct possible states of affairs.

We have two reasons to reject this conclusion. First, everyone agrees that (M, g) and \((M, \phi _{*}(g))\) are observationally indistinguishable, since this is what the diffeomorphism \(\phi \) represents. So if (4) is right, then substantivalism leads to distinct but observationally indistinguishable states of affairs. And this raises epistemic concerns about what reasons could underwrite our belief that these unobservable distinctions exist. But substantivalists have lived with this problem since the beginning of (Newtonian) time, and I don’t suppose that this argument poses any new challenge. A second, more worrisome problem is that taking (M, g) and \((M, \phi _{*}(g))\) to be inequivalent situations is “at odds with standard modern texts in general relativity, in which this equivalence is accepted unquestioningly in the specific case of manifolds with metrics” [12, p. 522]. So while substantivalists might be able to avoid the first worry, this argument suggests that we have to choose between substantivalism and accord with the textbooks. This distinction is also the seed of the indeterminism argument of the next section, which is more devastating. So we have to reject one of (1)–(3), and since (1) looks the most controversial, it’s on the chopping block.

However, we might reject steps other than (1), as subsequent work has shown. Substantivalism is a metaphysical thesis about spacetime, and the conclusion of (2) is a thesis about how our mathematical representations relate to modal distinctness facts. This inference must be underwritten by some story about how mathematical representations relate to modal distinctness facts, and how these distinctness facts relate to a mere existence claim about spacetime. Perhaps on a straightforward reading (2) follows from (1), but it needn’t. There are various versions of substantivalism that are realist about spacetime points while regarding (M, g) and \((M, \phi _{*}(g))\) as two representations of the same possible world; call these “sophisticated”, following Belot and Earman [3, 4]. The details of such a view can be worked out in a number of ways (e.g., [5, 7, 13, 21]), but sophisticated substantivalists are united in their denial of the claim that distinctions in the mathematics must be reflected in the existence of corresponding metaphysically distinct states of affairs.

I agree that (2) can be rejected, and perhaps it ought to be. But developing a more sophisticated account of substantivalism seems to me to be treating a symptom of the conceptual problem with the verificationist argument, rather than the underlying disease. It seems to me that (3) is false, and there is no nearby true premise that can rescue the argument. I take it that this reaction is common, though by no means universal. Indeed, as Weatherall [27] argues, it seems to follow from relatively common principles of applied mathematics. And since HoTT was developed, in part, to codify some of these principles, it bears this reaction out in quite literal terms.Footnote 5 By univalence there is an equality \(\mathsf {ua}(\phi ) : M = M\), and we have \((\mathsf {ua}(\phi ))_{*}(g) = \phi _{*}(g)\) by the defining property of \(\mathsf {ua}(\phi )\) and the way that diffeomorphisms act on Lorentzian metrics (i.e., by pushforward). So we have an equality \((\mathsf {ua}(\phi ), \mathsf {refl}(\phi _{*}(g)))\) between (M, g) and \((M, \phi _{*}(g))\), and if they are equal they cannot be distinct, so (3) fails. The verificationist argument thus fails for reasons quite independent of modal semantics.

I want to be clear that I don’t think HoTT does much heavy lifting in this response to the verificationist argument. Assuming that the natural reading in HoTT gives the correct identity criteria, we should reject step (3) of the verificationist argument. But the only reason I’ve given to adopt the natural reading in HoTT is that it correctly captures certain mathematical practices, and these are independent of what formalism we choose to adopt. So you might run this argument by appealing directly to mathematical practice, avoiding any appeal to HoTT. I take Weatherall [27] to be making an argument along these lines. He explicitly adopts two positions on the application of mathematics to physics: that “the default sense of ‘sameness’ or ‘equivalence’ of mathematical models in physics should be the sense of equivalence given by the mathematics” and that “[i]n most cases, the standard of sameness for mathematical objects is some form of isomorphism” [27, p. 331]. Since (M, g) and \((M, \phi _{*}(g))\) are isomorphic as Lorentzian manifolds, these positions imply that (M, g) and \((M, \phi _{*}(g))\) should be the same for the purposes of mathematical physics. And so, like me, Weatherall denies (3) in the verificationist argument. Indeed, something like his first principle is implicit in my taking equal Lorentzian manifolds in HoTT to represent the same spacetimes, and univalence is something like his second principle.

But I do want to claim something stronger than Weatherall. HoTT isn’t necessary to deny (3), but adopting a straightforward reading in HoTT involves more than just the rejection of (3). Like Weatherall, I am appealing to mathematical practice, but I mean to appeal to a more particular mathematical practice than he. Suppose, for example, that we accepted Weatherall’s principles but opted for a traditional formalism. We might adopt a form of sophisticated substantivalism like Pooley’s [21, p. 103] on which “individual spacetime points exist as basic objects, but possible spacetimes correspond to equivalence classes of diffeomorphic models of GR”. Then isomorphic models like (M, g) and \((M, \phi _{*}(g))\) correspond to the same spacetime, in accordance with our principles, even when they are unequal (in the set-theoretic formalism). On this account, presumably, the various diffeomorphisms between different models wouldn’t matter; the only physically significant fact would be whether two models belong to the same isomorphism class. But on the HoTT account the differences between these isomorphisms makes a difference. So by appealing to HoTT I am committing myself to more than I would be with an appeal to Weatherall’s principles. In particular, I am adopting a position on how we ought to extend this view of isomorphisms to other concepts that depend on sameness.

In the next two sections I show that Earman and Norton’s indeterminism argument is one place where the isomorphism structure of GR makes a difference. The question of determinism is one important disagreement between my HoTT-based account and those like Pooley’s which take possible spacetimes to correspond to equivalence classes of diffeomorphic models of GR. One virtue of sophisticated accounts is that they avoid a second problem that threatens to sink substantivalism: wild and intuitively spurious indeterminism. On my HoTT-based picture, GR formulated using Lorentzian manifolds is indeterministic in this way. But I take this to be a virtue of the picture. There is a natural way to rectify this indeterminism, and if we do so then I claim we more faithfully capture textbook GR.

4 The Indeterminism Argument

The real star of Earman and Norton’s show is the indeterminism dilemma, which transposes the theme of underdetermination due to diffeomorphism from an epistemic to a metaphysical key. Sophisticated substantivalism has a blanket response to both problems: distinctions in the mathematics don’t force distinctions in the metaphysics. If we use a straightforward semantics for HoTT, though, this blanket response isn’t available. Indeed, even though the verificationist argument doesn’t go through on a HoTT reading, the indeterminism argument does.

Earman and Norton’s indeterminism dilemma tries to force a choice between substantivalism and a pathological kind of indeterminism. The technical core of the argument is the existence of “hole diffeomorphisms”, which differ from the identity only on some nice region. For example, consider Minkowski space \((\mathbb {R}^{4}, \eta )\). If \(\phi : \mathbb {R}^{4} \rightarrow \mathbb {R}^{4}\) is some diffeomorphism supported only on the unit ball centered at the origin on \(\mathbb {R}^{4}\), then \((\mathbb {R}^{4}, \eta )\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ))\) are both dynamically possible models of GR. But they are merely isometric, not equal, and so are distinct ways the world could be—or so the substantivalist must say, according to Earman and Norton. Generalizing this example, they claim that “the state within any neighborhood of the manifold can never be determined by the state exterior to it, no matter how small the neighborhood and how extensive the exterior specification” [12, p. 524]. Indeterminism this radical suggests that something has gone wrong in our understanding, given GR’s success in predicting gravitational phenomena.Footnote 6

In light of the discussion of Sect. 3, we need to be more careful about the definition of determinism. I will focus on the kind of determinism at issue in the initial value problem of GR [25, Sect. 10.2], since this is the kind of determinism I take to be at issue in Earman and Norton’s argument.Footnote 7 Determinism in this context is a claim about models satisfying physical laws. And, according to Earman and Norton, we needn’t be much more specific about what we mean by “determinism” for their argument to go through. As they say,

the hole corollary forces substantivalists to conclude that no non-trivial form of determinism can obtain in local spacetime theories. The state within any neighborhood of the manifold can never be determined by the state exterior to it, no matter how small the neighborhood and how extensive the exterior specification [12, p. 524].

In other words, no matter what else we mean by “determinism”, it must at least be the case that in a deterministic local spacetime theory the state of a sufficiently small neighborhood is determined by a sufficiently extensive exterior specification. In a slogan, the laws of a theory are deterministic if they imply that “agreement on regions of a certain kind... forces agreement elsewhere” [7, p. 7]. The focus on regions is due to relativity. In nonrelativistic theories, a theory is deterministic if any two dynamically possible models that agree at some time agree at all times. However, in GR there is not, in general, a well-defined notion of a “moment of time”, and so we cannot always make sense of two models agreeing at some time. So we generalize: if GR is deterministic, we should expect that fixing a dynamically possible state of the world everywhere outside of some “nice” region U should also suffice to fix a unique dynamically possible state of the world inside of U. Tolerable levels of indeterminism vary from person to person, thus so will the bounds of “niceness”. But surely the unit ball centered on the origin in Minkowski spacetime is about as nice as can be, and if some dynamically possible universe is Minkowski outside this ball it ought to be Minkowski inside, as well. So the example of the previous paragraph should be a legitimate candidate example of indeterminism on any generalization of “moment of time”. And this is why Earman and Norton take their counterexample to apply to all non-trivial forms of determinism.Footnote 8

The kind of determinism at issue in Earman and Norton’s argument is thus modal and semantic: determinism is a claim about how many ways some region could possibly be, if we hold fixed the state of the world outside that region. This approach to determinism is due to Montague [18], and was refined and reformulated in more explicitly modal terms by Earman [11]. The semantic aspect should be contrasted with characterizations of determinism in terms of which statements about the future are deducible, such as Nagel’s [19]. And the modal aspect should be contrasted with more recent arguments, like Dasgupta’s [9], that determinism is a hyperintensional concept. Much of the literature responding to Earman and Norton also takes on a modal, semantic analysis of determinism, often with explicit reference to Montague and Earman. So while this analysis of determinism is perhaps imperfect [2, 6, 7, 9, 17], it has been the notion of primary concern in this literature and seems to track something of physical significance.

Earman and Norton turn this feature of GR into a reductio against substantivalism by attributing a particular method of possibility-counting to substantivalists, and this method is what sophisticated substantivalists disavow. For Earman and Norton substantivalism is just the denial of the claim that isometric Lorentzian manifolds always represent the same spacetime. The indeterminism argument shows that if you take models of GR to be Lorentzian manifolds and you take some isometric Lorentzian manifolds to be distinct models of GR, then you are committed to the indeterminism of GR. The sophisticated versions of substantivalism that have been developed in light of Earman and Norton’s argument all deny this characterization of substantivalism—that is, they argue that one can be a substantivalist while still counting isometric Lorentzian manifolds as representing the same possible spacetime. What Earman and Norton really establish is that a certain method of reckoning possibilities leads to indeterminism, and that substantivalists are prima facie committed to this method of reckoning. And so as with the verificationist argument, the literature on the hole argument has mostly focused on the relationship between substantivalism and modal distinctness facts and whether this prima facie impression survives closer inspection. Indeed, from this point of view the verificationist and indeterminism arguments come down to essentially the same issue: can the substantivalist take isometric Lorentzian manifolds to represent the same physical spacetime?

As in the case of the verificationist argument, I find myself convinced that the sophisticated substantivalist needn’t adopt the problematic possibility-counting method that Earman and Norton think they must, but I also think that other features of the indeterminism argument deserve more scrutiny. In particular, I think that generalizing Montague’s analysis of determinism to theories like GR involves subtleties that HoTT makes plain. For a local spacetime theory to be deterministic by Earman and Norton’s lights, there must be some sufficiently small region whose state is uniquely fixed by the state exterior to it, by the contrapositive of the argument quoted above. If the state space for this small region is just a set the state is uniquely fixed if there is one element in the subset of states that are compatible with the exterior region. But if the state space is a type in HoTT, or a (higher) category, then uniqueness means something more. Recall that, in HoTT, reasoning with equalities requires an appeal to particular equalities. The indiscernibility of identicals is an inference rule that takes four things as inputs: objects a and \(a'\) of type A, a predicate P that applies to objects of type A, and an equality \(p : a = a'\). In order to conclude \(p_{*} : P(a) \rightarrow P(a')\), we must have a particular p on which to rely. Similarly, sentences involving equality statements refer to particular equalities. So when we consider a conditional in which two models agree on some region, we are considering some particular equality \(\phi \) witnessing the agreement. And when we ask whether the two models agree everywhere under this conditional hypothesis, we are asking whether they also agree outside the given region with respect to the same equality, which gives the standard of sameness for the underlying manifold.Footnote 9 So a theory is deterministic if any equality of regions of a certain kind induces a unique equality of the models, not just some equality or other.

Let me repeat this analysis without HoTT, since I claimed above that my use of HoTT is, in part, merely for convenience of expression. To translate out of HoTT and into category theory, we replace types with categories and equalities with isomorphisms. An equality of models in HoTT is an isometry of Lorentzian manifolds in the category-theoretic semantics. A pair of models that agree on some region consists of two triples (M, g, S) and \((M', g', S')\)—where (M, g) and \((M', g')\) are Lorentzian manifolds and S and \(S'\) are submanifolds of M and \(M'\), respectively—along with a diffeomorphism \(\phi : M \rightarrow M'\) such that \(\phi (S) = S'\) and \(\phi _{*}(g) = g'\) when restricted to \(S'\). The analysis of determinism given in the previous paragraph says that GR is deterministic if any such \(\phi \) is also an isometry between (M, g) and \((M', g')\). In other words, GR is deterministic by this criterion if the category of initial data is equivalent to the category of dynamically possible models of GR. This criterion is stronger than the requirement that isomorphism classes of initial data be in bijection with isomorphism classes of dynamically possible models, because every equivalence of categories induces a bijection on isomorphism classes but not vice versa. It’s also more appropriate: the standard of identity for categories is equivalence, not bijection of isomorphism classes.Footnote 10

For a sophisticated substantivalist like Pooley [21], for whom possible spacetimes are given by isomorphism classes of Lorentzian manifolds, Earman and Norton’s indeterminism argument does not go through on the analysis of determinism just given. If possible spacetimes are represented by isomorphism classes then there are no nontrivial equalities between spacetimes: two equivalence classes either have the same elements or they don’t. And the same goes for regions of spacetime. So there is at most one equality between any two isomorphism classes, making any uniqueness requirements on isomorphisms inert. The requirement that an equality of spacetimes induce an equality of regions of a particular kind is also trivialized—there is at most one equality between equivalence classes and it restricts to the only possible equality between an equivalence class of regions. Thus, if we assume that possible spacetimes are given by isomorphism classes of Lorentzian manifolds, the criterion of determinism I have just described essentially reduces to the analysis of determinism offered by Butterfield [7, p. 9] under the name “Dm2”. In this case there is no distinction between equivalence of categories and bijection of isomorphism classes, and so the analysis of determinism in HoTT coincides with the kind of analysis used by Earman and Norton and subsequent literature.

However, if we take the equalities of models of GR to be isometries then Earman and Norton’s example gives a counterexample to determinism in the sense I have been discussing. If \(\phi : \mathbb {R}^{4} \rightarrow \mathbb {R}^{4}\) is a diffeomorphism that is the identity outside of the unit ball centered at the origin, then the identity diffeomorphism \(\mathsf {id}_{\mathbb {R}^{4}} : \mathbb {R}^{4} \rightarrow \mathbb {R}^{4}\) gives an equality of the triples \((\mathbb {R}^{4}, \eta , B^{c})\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ), B^{c})\), where \(B^{c}\) is the complement of the unit ball centered at the origin. This is because \(\phi \) is the identity on \(B^{c}\), and so \(\phi _{*}(\eta ) = \eta \) there. But \(\mathsf {id}_{\mathbb {R}^{4}}\) is not an isometry between the Lorentzian manifolds \((\mathbb {R}^{4}, \eta )\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ))\), since \((\mathsf {id}_{\mathbb {R}^{4}})_{*}(\eta ) \not = \phi _{*}(\eta )\) in the unit ball. So on the analysis of determinism taken from HoTT, specifying the metric on almost all of Minkowski space does not suffice to fix it everywhere. This kind of example generalizes as Earman and Norton say, and so “the state within any neighborhood of the manifold can never be determined by the state exterior to it” [12, p. 524].

To be clear, this version of the hole argument isn’t Earman and Norton’s. Their argument is not about the difference between equivalence of categories and bijection of isomorphism classes, it is an argument against one method of possibility counting. The argument just given is an argument against a different method of possibility counting—one that a sophisticated substantivalist endorses, but also one that Earman and Norton themselves likely endorse. On their analysis of determinism it seems that a bijection of isomorphism classes suffices, and so the situation of the previous paragraph is not an example of indeterminism. After all, the diffeomorphism \(\phi : \mathbb {R}^{4} \rightarrow \mathbb {R}^{4}\) also gives an equality of the triples \((\mathbb {R}^{4}, \eta , B^{c})\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ), B^{c})\), and it is also an isometry between the Lorentzian manifolds \((\mathbb {R}^{4}, \eta )\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ))\). So the isomorphism class of the exterior specifications \((\mathbb {R}^{4}, \eta , B^{c})\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ), B^{c})\) corresponds to the isomorphism class of the Lorentzian manifolds \((\mathbb {R}^{4}, \eta )\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ))\) in a bijection between exterior specifications and Lorentzian manifolds satisfying the Einstein equation. But such a bijection between isomorphism classes of exterior specifications and isomorphism classes of spacetimes isn’t induced by an equivalence of categories, because there are more isomorphisms in the category of exterior specifications than there are in the category of Lorentzian manifolds. So if we take the category of models of GR to be the category of Lorentzian manifolds satisfying the Einstein equation then GR is indeterministic in the sense the sense appropriate to theories whose collections of models are categories.

Of course, GR isn’t indeterministic, so something has gone wrong in this analysis. On my view, the source of the error is that it has neglected the fact that GR is a gauge theory—a fact which plays a role in proofs that the initial value problem for GR is well-posed [25, p. 260]. Indeed, I take the indeterminism argument as I have just presented it to be a sign that “diffeomorphisms comprise the gauge freedom of general relativity” [25, p. 438], just as the similar failure of determinism in Yang–Mills theories is a sign that the gauge freedom there has been neglected. So in the next section I describe a theory in which diffeomorphisms are taken to be gauge structure and contrast it with the formulation of GR in terms of Lorentzian manifolds. Adding gauge structure in HoTT amounts to adding equalities between configurations of the metric tensor fields; in the categorical semantics this means adding isomorphisms, producing a gauge theory in the sense of Nguyen et al. [20]. In addition to fixing the indeterminism we just encountered, this gauge structure impinges on other parts of GR.

5 Generally Covariant Lorentzian Manifolds

We can regain determinism in GR by inserting the equalities that seem to be missing. This is a kind of quotient, since we are identifying possible futures if they restrict to equal initial data. This might sound like the version of sophisticated substantivalism that takes spacetimes to be given by diffeomorphism classes of Lorentzian manifolds. But it is importantly different. Taking equivalence classes in the usual sense eliminates any nontrivial equality dependence, since there is at most one equality between any two equivalence classes. If we apply a weaker quotient by inserting more equalities, then we can avoid the indeterminism of Lorentzian manifolds without completely collapsing the equality structure. This equality structure is used in GR—for example, in perturbation theory—so we ought to use these weakly quotiented models, instead.

A precise statement of the quotient procedure would require us to identify exactly which diffeomorphisms cause problems for determinism. I will call these hole diffeomorphisms, and I will take them to at least include those diffeomorphisms generated by a vector field. Exactly which diffeomorphisms are hole diffeomorphisms is a substantive question beyond the scope of this article. Leaving this unspecified, the result of the quotient is the following

Definition 1

A generally covariant Lorentzian metric on a manifold M is specified by a Lorentzian metric g, and an equality \(g = g'\) of generally covariant Lorentzian metrics on M is a hole diffeomorphism \(\psi : M \rightarrow M\) such that \(\psi _{*}(g) = g'\). A generally covariant Lorentzian manifold is a pair (M, g) of a smooth manifold M and a generally covariant Lorentzian metric g on M. Thus, an equality \((M, g) = (M', g')\) of generally covariant Lorentzian manifolds is a pair \((\phi , \psi )\) of a diffeomorphism \(\phi : M \rightarrow M'\) and a hole diffeomorphism \(\psi : M' \rightarrow M'\) such that \(\psi _{*}(\phi _{*}(g)) = g'\).

A generally covariant Lorentzian manifold is not the same thing as a Lorentzian manifold. For example, for any hole diffeomorphism \(\phi : M \rightarrow M\) there is an equality between (M, g) and \((M, \phi _{*}(g))\) given by \((\mathsf {refl}(M), \phi )\). So there is an equality of the form \((\mathsf {refl}(M), -)\), which there is not for Lorentzian manifolds, as we saw in considering the verificationist argument. And this allows generally covariant Lorentzian manifolds to avoid the refined indeterminism argument of the previous section. The problem, recall, was that the equality \((\mathsf {refl}(\mathbb {R}^{4}), \mathsf {refl}(B^{c}), \mathsf {refl}(g'))\) between \((\mathbb {R}^{4}, \eta , B^{c})\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ), B^{c})\) did not induce a unique equality between \((\mathbb {R}^{4}, \eta )\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ))\). But now it does: it induces the equality \((\mathsf {refl}(\mathbb {R}^{4}), \phi )\) of the generally covariant Lorentzian manifolds \((\mathbb {R}^{4}, \eta )\) and \((\mathbb {R}^{4}, \phi _{*}(\eta ))\). And indeed, one can show that any equality of models that agree on some nice region induces an equality of the entire generally covariant Lorentzian manifolds, so determinism is regained and the verificationist argument still fails at the third step.Footnote 11

I take generally covariant Lorentzian manifolds to be a better formalization of models of GR than Lorentzian manifolds. This isn’t only because they avoid the indeterminism of the refined indeterminism argument (though that helps), but also because they more accurately capture GR as found in textbooks. The difference between the two can be hard to find. While the indeterminism argument distinguishes them, the difference doesn’t much arise in everyday GR life. And for good reason: generally covariant Lorentzian manifolds are obtained by quotienting the type of Lorentzian manifolds, and we generally work with quotients by doing manipulations on the unquotiented objects and then showing that these manipulations are preserved by the quotient. We think nothing of treating a fraction as a pair of integers, even though it’s really an equivalence class of such. We just make sure not to manipulate them in a way that violates the equivalence relation: we allow definitions like \(a/b + c/d = (ad + bc)/bd\) but not like \(a/b \star c/d = (a + c)/(b + d)\). Since any Lorentzian manifold gives a generally covariant Lorentzian manifold, and any equality of Lorentzian manifolds gives an equality of generally covariant Lorentzian manifolds, we can usually work with regular Lorentzian manifolds, just as we work with pairs of integers when treating fractions. Moreover, if we have an equality \((\mathsf {ua}(\phi ), \psi ): (M, g) = (M', g')\) of generally covariant Lorentzian manifolds then there is a corresponding equality \((\mathsf {ua}(\psi \circ \phi ), \mathsf {refl}(g')) : (M, g) = (M', g')\) of Lorentzian manifolds, so if we only care about whether there is some equality or other between two objects, Lorentzian manifolds and generally covariant Lorentzian manifolds amount to the same thing. We can only see the difference if we pay attention to particular equalities.

Though the differences are inconspicuous in many contexts, they are crucial in others. The defining difference is that for a fixed manifold, two generally covariant metrics g and \(g'\) can be equal in more than one way. This feature is most familiar from classical gauge theories, and so we should expect the difference between Lorentzian manifolds and their generally covariant cousins to manifest wherever gauge structure manifests—e.g., in perturbation theory, in initial value problems, and in the structure of fields “at infinity”. Indeed, the claim that “diffeomorphisms comprise the gauge freedom of general relativity” [25, p. 438] is textbook GR, and this freedom is found in all three of these situations [25, Eqs. 4.4.9, 10.2.32, p. 467 fn. 2]. We lack the space to deal with all of these, so let’s consider just the first.

In the weak-field approximation of GR, we consider the infinitesimal neighborhood of a flat model like Minkowski space \((\mathbb {R}^{4}, \eta )\). To do this, we fix a background manifold like \(\mathbb {R}^{4}\) and some metric like \(\eta \), and we parametrize the space of configurations on \(\mathbb {R}^{4}\) by writing any metric g as \(g = \eta + \gamma \). If we are working with Lorentzian metrics, then the equality facts in this space are trivial: two metrics \(\eta + \gamma \) and \(\eta + \gamma '\) are equal just in case \(\gamma = \gamma '\). On the other hand, if we are working with generally covariant Lorentzian metrics, then the equality facts in this space are more complicated: an equality of metrics \(\eta + \gamma \) and \(\eta + \gamma '\) is a hole diffeomorphism \(\phi : \mathbb {R}^{4} \rightarrow \mathbb {R}^{4}\) such that \(\phi _{*}(\eta + \gamma ) = \eta + \gamma '\). This parametrizes the neighborhood of Minkowski space, so to restrict attention to infinitesimal perturbations we demand that \(\gamma \) be infinitesimal. If we are working with Lorentzian metrics, then the equality facts don’t change: two metrics are equal just in case \(\gamma = \gamma '\). But if we are working with generally covariant Lorentzian metrics, then the equality facts must also become infinitesimal. So an equality between \(\eta + \gamma \) and \(\eta + \gamma '\) with \(\gamma \) and \(\gamma '\) infinitesimal is given by a vector field \(\xi \) such that \(\gamma + \pounds _{\xi }\eta = \gamma '\), where \(\pounds _{\xi }\) is the Lie derivative along \(\xi \). To decide which of these is the correct space of infinitesimal perturbations off of Minkowski space we just need to check what the equality facts about perturbations are according to a GR textbook. As Wald [25, Eq. 4.4.9] says, a gauge transformation (in our parlance, an equality) in this context is a transformation taking \(\gamma \) to \(\gamma + \pounds _{\xi }\eta \). So the correct space of perturbations comes from generally covariant Lorentzian metrics.Footnote 12

6 Conclusion

I have argued that even if we take isomorphic models of GR to represent the same spacetime we have something to learn from Earman and Norton’s hole arguments. I do not think their verificationist argument goes through, for reasons similar to those recently advanced by Weatherall [27]. But, I have argued, a response to the verificationist argument needn’t directly carry over to a response to the indeterminism argument. If one attends to the isomorphism structure of the theory, and if one treats it in the spirit of HoTT, then the indeterminism argument still poses a problem.

The natural solution is to move to what I have called generally covariant Lorentzian manifolds. On this reconstruction, the hole argument shows that any diffeomorphism-invariant dynamics on an ordinary Lorentzian manifold will lead to indeterminism, and that a substantive notion of general covariance rectifies this problem. I take this to be an advantage of my account insofar as it corroborates the feeling many physicists have that general covariance is a substantive notion, and that the hole argument tells us something important about it [3]. In most cases, the difference between generally covariant Lorentzian manifolds and their plainer cousins is irrelevant. But when the difference makes a difference—for example, in perturbation theory—physicists use the generally covariant structure.