## October 30, 2013

### The HoTT Approach to Physics

#### Posted by David Corfield

Summer saw the foundations of mathematics rocked by the publication of The HoTT Book. Here we are a few months later and the same has happened to physics with the appearance on the ArXiv of Urs’s Differential cohomology in a cohesive infinity-topos.

Physics clearly needs more than the bare homotopy types of HoTT. Field configurations may be groupoids (1-types) under gauge equivalence, or indeed $\infty-groupoids$ (homotopy types) under gauge-of-gauge-of-… equivalence, but they also possess differentiable structure. The question then is how to cater for all of those principal bundles, connections, curvature forms, and in more recent times 2-bundles, orbifolds, Lie $\infty$-algebroids,…, while building on HoTT, or, in terms of the environments in which HoTT (or Univalent Foundations) functions, while adding structure to $(\infty, 1)$-toposes.

We’ve become rather used to caring little about how elaborate are the constructions we would need to place on our foundational language were we to formalize the mathematics of current theoretical physics. What does it matter if it would be a nightmare to go ahead and fully express the ingredients of, say, the Green-Schwarz mechanism in heterotic supergravity in the language of ZFC set theory?

But perhaps we should never have let ourselves fall into this state of indifference. One person who has fought against this trend is Bill Lawvere. His simple notion of cohesion, how bare points are held together in spaces, was just what Urs needed to add to the axioms for $(\infty, 1)$-toposes. Now all the differential cohomology you ever wanted to do can be done in the setting of cohesive $(\infty, 1)$-toposes, or, if you prefer a syntactic approach, through cohesive homotopy type theory.

I’m looking forward to cohesion cropping up in a wide range of places within mathematics over coming years. Perhaps we’ll start to understand why number theorists and physicists have so much to talk about together.

Posted at October 30, 2013 10:21 AM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2667

### Re: The HoTT Approach to Physics

Your link on cohesive homotopy type theory has an invisible Left-to-Right Mark at its end which keeps it from working. Did you copy and paste from near some Hebrew or Arabic text?

Posted by: RodMcGuire on October 31, 2013 4:30 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Fixed, thanks! That’s very odd. I think I googled the phrase and copied the address from the list.

Posted by: David Corfield on October 31, 2013 9:21 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

In your last post before this, a link to my blog was broken for some similar mysterious reason: extra characters at the end of the URL. Luckily an elf fixed it.

Posted by: John Baez on November 1, 2013 6:21 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

“We’ve become rather used to caring little about how elaborate are the constructions we would need to place on our foundational language were we to formalize the mathematics of current theoretical physics.”

What would the axioms for geometry be? Are they Tarski’s (1959) axioms? Or similar to Hilbert’s (1899) axioms? Are they like Field’s (1980) axioms? What is the language $\mathcal{L}$? What are the primitive symbols of $\mathcal{L}$? How do the axioms, e.g., guarantee that models all have the form $(M, g)$, where $M$ is a manifold and $g$ a (0,2) tensor field?

Just saying “Let $(M, g)$ be a semi-riemannian manifold with a metric” is surely not physics. Surely it is mathematics, and mathematics is not physics. If physics were simply mathematics, then Hilbert’s 6th problem would already have been solved, by Hilbert and Ackermann 1928!

The point is that physics makes claims that are contingent and vary from world to world. Such as

(Phys) Physical test particles move along geodesics.

These claims have empirical consequences that can be tested by experiment. But mathematics makes claims, such as,

(Mat) There are, up to isomorphism, two non-isomorphic groups of order 4.

And this kind of claim is modally necessary and is invariant across all worlds. (The statement (Mat) is a theorem of $Z$ set theory, with infinity removed.) One cannot perform experiments to test (Mat). One can show that (Mat) may be conservatively added to any non-mathematical theory $T$. That is, for any non-mathematical statement $\phi$,

If $T + (Mat) \vdash \phi$, then $T \vdash \phi$.

No experiment can refute (Mat).

But one can do experiments to test (Phys).

So, it seems to me that a theory of types, equipped with extra axioms for $\mathbb{N}$, etc., like HoTT does not begin to play a role in formalizing physics until one specifies

i. the primitive physical concepts

ii. the relevant comprehension principles for them.

So, e.g., the language $\mathcal{L}$ adopted might contain “$p$ is a spacetime point”, “$O$ is region of spacetime”, “$\gamma$ is a worldline of a point particle”, “the value of field $\Psi$ at point $p$ is $\mathbf{v}$”, etc.

Cheers,

Jeff

Posted by: Jeffrey Ketland on October 31, 2013 2:01 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks, Jeff.

If physics were simply mathematics, then Hilbert’s 6th problem would already have been solved, by Hilbert and Ackermann 1928!

There are many things that could be said in response. Let me begin with something rather pragmatic about cohesive HoTT in (1), and then in a later post something more closely related to what you’re actually asking for in (2).

(1) We can see what Hilbert meant by his sixth problem by taking a look at how he himself tried to answer it over the following decades by, e.g., his formulation of general relativity via variational principles, and his work on early quantum mechanics. His lectures on physics have little to do with his formalist project. He is seeking good mathematical formulations for those physical theories which involve mathematics. Doing mathematical physics isn’t just doing mathematics.

So the idea behind what Urs is doing is to find a mathematical framework in which many other frameworks for physics - symplectic geometry for classical mechanics, Riemann geometry for general relativity, differential cohomology for gauge theory, operator algebras for quantum mechanics, etc. - make sense. By ‘make sense’ I mean fit naturally so that the framework doesn’t just gather them, but provides useful guidance as to how to proceed.

And it does provide useful guidance about geometric quantization, higher gauge theory and so on. Even classical mechanics and field theory are cast in a different light. A huge amount of work in mathematical physics can be seen as part of a bigger picture, one which emerges out of some rather simple principles.

To the extent that this is valuable work (I fear we are treading close to the issue of the worth of much of modern mathematical physics, and we wouldn’t want the String Wars flaring up here), and that cohesive $(\infty, 1)$-toposes are excellent environments in which to find the corresponding constructions, then cohesive HoTT earns credit for being the internal language of these toposes. Whether one works better thinking in terms of the internal language or externally in specific toposes is not so important, just as one may reason about objects in the topos of sheaves over a space, or internally with higher-order intuitionistic logic and then interpret the reasoning in that topos.

But I think you’re after some other function of a foundational language, one which allows you to express what is the case in our world. If Quine is roughly on the right track with the idea that expression within logic reveals ontological commitment, then we should want to know what difference it makes using HoTT. That’s something for me to think on about for part (2).

Posted by: David Corfield on November 1, 2013 11:39 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks, David,

Yes, I think that’s basically right - I looked at Urs’ papers on this and the book you linked to: very cool and very impressive. (Though my knowledge of category-theory is not good…) A kind of translation into cat-lingo of the kind of thing one has in the more usual math physics textbooks I used to use (like Choquet-Bruhat et al, Wald, Schutz, Frankel, …).

But it still doesn’t seem to give a new insight into the foundational questions - it just seems to reformulate them. It doesn’t tell me something about, e.g., applicability. First I want to understand a falling apple, and soon I have a manifold $M = (A,\mathcal{C})$, with a point set $A$ and atlas $\mathcal{C}$ on $A$, and some tensors on $M$ and geodesics on $M$, etc. But why?

It doesn’t tell me about how, e.g., a space-time model $(M,g)$represents” a world, etc. I’d like to know why, e.g., if a space-time model $(M,g)$ is isomorphic to $(N,h)$, then they represent the same physical world.

To take the more standard case of em gauge theory, we know that $A$ and $A^{\prime} = A + d\Lambda$ “represent the same physical state”. In this case, everyone knows that $F := dA$; and so $F^{\prime} = d(A + d\Lambda) = dA + dd\Lambda = F$ (we can talk about cohomology for more complicated cases). So, there’s a class of gauge-equivalent fields. But why does Nature do something so weird?

Someone can tell me all about fibres, sections, vertical automorphisms, etc., etc.; but it doesn’t answer the question: why are $A$ and $A^{\prime}$ representations of the same physical state? Why are isomorphic copies $(M, g)$ and $(N,h)$ representations of the same physical world?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 1, 2013 6:09 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

If mathematical structures are models of the physical world, isomorphic mathematical structures are models of isomorphic physical worlds.

At least that’s how physics works these days. If this seems ‘weird’ and you want more insight into it, you’d probably better consult a philosopher: to a physicist or mathematician this probably seems ‘obviously right’, so they won’t have much to say. For them the fun starts when you pick a particular kind of mathematical structure and start working with it. And that’s what Urs is busy doing.

Posted by: John Baez on November 4, 2013 6:32 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks John. I think the principle you mean is that isomorphic models are models of the same world (according to physics). And that’s the thing that’s weird (the representation relation is not injective). It means, e.g., that you can’t really think of the world as a structured set - e.g., a set $A$ of spacetime points with differential structure, topology, metric $g$, matter fields, etc., on it. If you did, then permuting the set $A$ would give a distinct new (albeit permuted) world, but clearly physics says its the same world. (The idea goes back to Leibniz, btw.)

Yes, I totally agree with what you say on Urs’ stuff - which is cool! Though my knowledge of category theory is rubbish, I do get much of it. But Urs is sort of going “upwards” (reformulating the differential geometry in interesting category-theoretic terms); but the philosophical and foundational questions are “downwards”.

For example, how does the mathematical structure we pick, e.g., $(M^4, \phi)$ with $M^4$ Minkowski space and $(\Box + m^2)\phi = 0$, represent the physical world?

Jeff

Posted by: Jeffrey Ketland on November 4, 2013 10:14 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

I think the principle you mean is that isomorphic models are models of the same world (according to physics).

I actually meant what I said. Roughly speaking, I’d say two worlds are isomorphic if for each bunch of experiments in one there’s a corresponding bunch of experiments in the other that have the same results, or average results. This will happen iff the mathematical structures representing them are isomorphic.

If this seems weird, think of smaller physical systems. We could have two salt crystals that are isomorphic but not equal, sitting side by side. I’ll say two crystals are isomorphic if for each bunch of experiments in one there’s a corresponding bunch of experiments in the other that have the same results, or average results. This will happen iff the mathematical structures representing them are isomorphic.

If you insist on equality here, your notion of ‘world’ corresponds to what I’d call an isomorphism class of worlds—no big deal, just a different definition. But if you use this other definition, you shouldn’t be surprised that mathematically isomorphic structures give the same world. By working with equivalences classes you’ve turned isomorphic things into equal things.

Posted by: John Baez on November 5, 2013 3:20 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John,

Say we have, as in your example, crystals $t,u$ of salt, assumed distinct, and also some definition of a structure $\mathcal{M}_t$ assigned to $t$, and a structure $\mathcal{M}_u$ assigned to $u$. So, after lots of experimenting, we get the conclusions:

$t \neq u$

$\mathcal{M}_t \cong \mathcal{M}_u$

But, for the case of worlds, say $w_1, w_2$, with assigned structures $\mathcal{M}_{w_1}, \mathcal{M}_{w_2}$, then GR says that

$\mathcal{M}_{w_1} \cong \mathcal{M}_{w_2} \to w_1 = w_2$

So, unlike the case of distinct isomorphic crystals, isomorphic models of whole worlds are models of the very same world. (Basically, a modern version of Leibniz’s debate with Newton - Leibniz’s relationism vs. Newton’s absolute space.)

If one defines a world* to be an equivalence class of isomorphic worlds, then the principle is kind-of-trivial, yes. What’s weird on that way of putting it is that the physical world we live in is not a world (i.e., a bunch of spacetime points with properties and relations), but is a world* – that is, an equivalence class of isomorphic bunches of spacetime points with properties and relations.

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 12:28 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

the physical world we live in is not … a bunch of spacetime points with properties and relations … but … an equivalence class of isomorphic bunches of spacetime points with properties and relations.

I don’t see how that can possibly be true. One of the important features of the world is that we can distinguish between distinct spacetime points, e.g. we can say that a certain event happened here and not there. But it doesn’t make sense to speak of, e.g., the points of an isomorphism class of differentiable manifolds. An individual manifold has points, but an isomorphism class of them doesn’t, because any manifold has automorphisms that interchange some of its points.

Posted by: Mike Shulman on November 6, 2013 6:30 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

I don’t see how that can possibly be true. One of the important features of the world is that we can distinguish between distinct spacetime points, e.g. we can say that a certain event happened here and not there. But it doesn’t make sense to speak of, e.g., the points of an isomorphism class of differentiable manifolds. An individual manifold has points, but an isomorphism class of them doesn’t, because any manifold has automorphisms that interchange some of its points.

Yes, quite - that’s what I mean about it being weird! Naively, we’d like to say, roughly,

A physical world is a bunch of spacetime points with properties and relations.

And then, with modern physics, we have a differentiable manifold $M$ (maybe with other fields too) which “represents” such a world. The natural idea is that points in $M$ represent the genuine physical spacetime points.

But it seems that (LE) rules this out, because (LE) says

If $\mathcal{M}_1$ and $\mathcal{M}_2$ are isomorphic spacetime models, then $\mathcal{M}_1$ and $\mathcal{M}_2$ represent the same physical world.

According to (LE), the result of moving/pushing forward the properties and relations over the spacetime points, yielding a distinct but isomorphic copy, is the same world. (In fact, this is Leibniz’s view as well, against Newton, and the mapping is a “Leibniz shift”, modernized to talk of manifolds, fields, etc.)

I took John’s suggestion to be that, maybe we can interpret “physical world” to mean “equivalence class of bunches of points with properties and relations”. But this is weird, and faces the objection you give. So, how to understand what the world is like if (LE) is true is hard.

The upshot seems to be that: if (LE) is right, then isomorphic worlds have to be somehow be the same world – and that’s the link with the Univalence axiom that John suggested. And maybe that approach (which Steve discusses in the mathematical context in his recent paper on univalence and structuralism) does shed light on how to make sense of (LE) in physics.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 12:57 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Well, if that’s what (LE) says, then it clearly must be false. So why worry about understanding what the world would be like if it were true?

Unless, of course, we follow John’s suggestion and interpret “the same” univalently as meaning “isomorphic”, in which case there is no problem.

Posted by: Mike Shulman on November 6, 2013 7:56 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

Well, if that’s what (LE) says, then it clearly must be false.

Ok, but that’s definitely what (LE) says: “isomorphic spacetime models represent the same world”, where “the same” really does mean “the same”!

Just as the gauge potentials $A$ and $A + d\Lambda$ represent the same state in electromagnetism, in GR, the isomorphic spacetime models $\mathcal{M}_1$ and $\mathcal{M}_2$ represent the same world. It’s not that distinct isomorphic models represent distinct, but isomorphic, physically indistinguishable, worlds. On (LE), that cannot happen!

(And this is more-or-less what Leibniz said to Newton, but now dressed up in modern diff geometry lingo.)

This is why it’s weird … I accept it, and I think one can make sense of it. But it’s difficult. It tells us, I think, that a physical world cannot have a special carrier set of spacetime points. In some sense, the choice of some carrier set of spacetime points is itself a “gauge choice”.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 7, 2013 8:23 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

It tells us, I think, that a physical world cannot have a special carrier set of spacetime points.

The question then is do we next look to find an alternative carrier set for the physics, such as the equivalence classes of states under gauge equivalence. Or alternatively, is there something unhelpful about the drive to ground our structures in some specific things?

Perhaps we need a foundational language which doesn’t want us to look for carrier sets at all. Just as we’ve found in maths that it works just fine not to find a carrier set for the natural numbers.

Generally, why not say we have a type that interests us, and we then find out the structural features of the type, e.g., what homotopy level it has. If it turns out to have level 0, we can treat it informally as a set. But if it is of higher homotopy level, then we can’t treat it like a set. There is a 0-truncation of any type, but it’s a different type.

Posted by: David Corfield on November 7, 2013 11:48 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

The question then is do we next look to find an alternative carrier set for the physics, such as the equivalence classes of states under gauge equivalence.

The answer is no, as the argument suggests that the carrier set has to be eliminated somehow.

Generally, why not say we have a type that interests us, and we then find out the structural features of the type…

But what is the type here - some kind of type of spacetime points? The type of Possible Physical Worlds?

Jeff

Posted by: Jeffrey Ketland on November 7, 2013 9:33 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks very much for posing all these questions to us, Jeff. They’re just the sorts of issue I need to work out. I thought I had time to think up something sensible to say this morning, but time has fled by, so I’ll have to return to this later.

One consideration, if only briefly to remind myself, is that defining a type $\mathbf{Spacetime}$, we certainly needn’t restrict ourselves to sets (in the HoTT sense of homotopy level 0). Indeed, in string theory we don’t. There are orbifolds, orientifolds,…

Also, we’ll need to specify a range of other types and terms: $\mathbf{Fields}$, $\mathbf{Coefficients}$, an action as a dependent type between these,…

Posted by: David Corfield on November 8, 2013 10:02 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

So, unlike the case of distinct isomorphic crystals, isomorphic models of whole worlds are models of the very same world.

You keep saying this. If you have some argument for the claim, presenting it would make this conversation more interesting. Or maybe it’s just a definition?

Either way, we don’t really need to argue: what you’re calling a “world” is what I’d call an “isomorphism class of worlds”. So, if we have to keep talking to each other, we can make up terminology that makes us both happy. You suggested one approach, but how about this: I’ll use the term schmorld for my concept of world, and then we can agree that a world is an isomorphism class of schmorlds.

But from my long experience with category theory, I know that taking isomorphism classes (also known as decategorification) is a process that loses interesting information. So, I prefer to work with schmorlds than worlds.

(And indeed, when you’re not around I will secretly continue to call them “worlds”.)

For example, a schmorld can have symmetries, meaning that it is isomorphic to itself in more than one way. Indeed, there’s a groupoid of schmorlds. But when we take isomorphism classes, we squash this groupoid down to a mere set. That gives a lot less structure to work with, and it becomes more inconvenient to talk about symmetries. Groupoids are a better context for talking about symmetries.

(Cohesive $\infty$-groupoids are even better, but we’re stuck here at the bottom of the ladder, arguing about whether to start climbing.)

What’s weird on that way of putting it is that the physical world we live in is not a world (i.e., a bunch of spacetime points with properties and relations), but is a world* – that is, an equivalence class of isomorphic bunches of spacetime points with properties and relations.

So you continue to claim! But I don’t know what experiment, or act of introspection, you did to determine that you live in an isomorphism class. Please don’t tell me the reason is that you can’t tell which representative of this isomorphism class you live in… that’s just the meaning of ‘isomorphic’.

Posted by: John Baez on November 6, 2013 1:12 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John,

You keep saying this. If you have some argument for the claim, presenting it would make this conversation more interesting.

Here are some versions of the formulation of Leibniz equivalence (but there are lots of others):

For any spacetime model $(M, O_1, \dots, O_n)$ and any diffeomorphism $h$ on $M$, Leibniz equivalence asserts that the two models $(M, O_1, \dots, O_n)$ and $(hM, h^{\ast}O_1, \dots, h^{\ast}O_n)$ represent the same physical system. (Norton 2011, note 5.)

and

You will often hear it proclaimed that GR is a “diffeomorphism invariant” theory. What this means is that, if the universe is represented by a manifold M with metric $g_{\mu \nu}$ and matter fields $\psi$, and $\phi :M \to M$ is a diffeomorphism, then the sets $(M,g_{\mu \nu},\psi)$ and $(M,\phi_{\ast}g_{\mu \nu},\phi_{\ast}\psi)$ represent the same physical situation. (Carroll 1997: 138.)

and

Let $\mathcal{M}_1 = \langle M,g,T\rangle$ and $\mathcal{M}_2 = \langle M,d\ast g,d \ast T\rangle$ be two models of GR where $d$ is a non-trivial diffeomorphism, …

(LE) $\mathcal{M}_1$ and $\mathcal{M}_2$ represent the same possible world. (Pooley 2003, Sc. 5.1)

and

… if $\phi : M \rightarrow N$ is a diffeomorphism, then $M$ and $N$ have identical manifold structure. If a theory describes nature in terms of a spacetime manifold $M$ and tensor fields $T^{(i)}$ defined on the manifold, then if $\phi : M \rightarrow N$ is a diffeomorphism, the solutions $(M, T^{(i)})$ and $(N, \phi^{\ast}T^{(i)})$ have physically identical properties. Any physically meaningful statement about $(M, T^{(i)})$ will hold with equal validity for $(N, \phi^{\ast}T^{(i)})$. (Wald 1984: 438)

In these cases, the idea is that the isomorphic models represent the same world.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 1:47 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

Here are some versions of the formulation of Leibniz equivalence (but there are lots of others)…

But these are not arguments that it’s good to treat isomorphic models as models of the same world. They are just further restatements of this claim… or, perhaps, definitions.

I don’t really need more statements of this sort: I’m not a big believer in proof by repetition. What I’d really like would be more precision about what these statements are supposed to mean, and what is their logical status.

Are they claims of the sort we could argue about? Or are they just definitions? If they are claims, is there some evidence for them? What kind of evidence?

If I read this, for example:

For any spacetime model $(M, O_1, \dots, O_n)$ and any diffeomorphism $h$ on $M$, Leibniz equivalence asserts that the two models $(M, O_1, \dots, O_n)$ and $(h M, h^{\ast}O_1, \dots, h^{\ast}O_n)$ represent the same physical system. (Norton 2011, note 5.)

I see a precise mathematical phrase followed by the vaguer phrase ‘represent the same physical system’. So, I’d naturally take the precise phrase as a definition of the vaguer phrase. And then the question is not whether this definition is ‘true’ or not, but merely: when is it a useful definition, and when is it not?

It’s also interesting that you seem to interpret ‘same’ as meaning ‘equal’. But there’s no need to do that: ‘same’ is often used to mean ‘isomorphic’.

For example, if we say “all these sandwiches are the same”, we don’t mean they’re all equal, in the sense of there being just one sandwich. We mean they’re isomorphic in some way.

And if we take this quote by Norton as a definition of ‘the same physical system’, then he’s defining ‘same’ to mean isomorphic!

That would be fine with me.

The most important recent thought on this subject is Voevodsky’s univalence axiom, which is one of the key ideas in homotopy type theory. This axiom asserts that isomorphic mathematical structures (or more generally ‘equivalent’ ones, in a certain precise technical sense) are equal.

The fascinating thing is that this axiom does not cause trouble! You might think it would mess things up to assert that all isomorphic groups are equal. But it doesn’t! Instead, it formalizes common practice in mathematics, where we use ‘the same’ to mean either isomorphic or equal.

So it’s possible that Norton and the other people you’re quoting are secretly believers in the univalence axiom — but perhaps only for ‘worlds’, not mathematical structures!

I have no problem with the univalence axiom: it shocked me at first, but now I see it’s a great idea. However, it seems to me that if you adopt this idea for one kind of thing (‘worlds’), it makes a mess if you don’t also adopt this idea for another related thing (‘models’). It creates a false puzzle, which is why worlds act differently than models.

It works more smoothly to either adopt univalence in a uniform way, or not at all.

Posted by: John Baez on November 6, 2013 4:06 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks, John - yes, they’re formulations of LE (since Earman and Norton’s first discussion of this in 1987, it’s been called “Leibniz equivalence”), not arguments for the principle. Some people, of course, disputed the principle. Back them, it was a premise in the so-called “the Hole argument”, which aimed to show that GR leads to indeterminism; but everyone now agrees (with Einstein) that this argument isn’t right. The Wald quote does hint at a kind of argument - isomorphic models $(M, g)$ and $(N, h)$ are physically indistinguishable, and so “represent the same world”, “same situation”, etc. That’s similar to the point you make a bit earlier (i.e., how would we know which representative of the equivalence class we’re in?). As you say, the phrase

“represent the same world”

is not a mathematically precise one, and that’s actually where all the action is, yes. So, thinking about this, one wonders what “represents” means and what “world” means, in this context.

The person who originated the argument was Leibniz, in his debate with Newton’s advocate, Samuel Clarke. It’s now called a “Leibniz shift argument”, and goes a bit like this:

Suppose God picks up all the matter in the word and moves it smoothly one metre in some direction relative to Absolute Space. The result is indistinguishable. And so, it is not even a different world. It’s the same world. And therefore Absolute Space is imaginary; all there is are “relations”.

Then, about 200 years later, Leibnizian relationism seems to be vindicated in Einstein’s theory. This debate continues (e.g., Rovelli, Smolin, and people who write on philosophy of spacetime), and various people insist that it’s intimately connected to questions about background independence and QG.

Maybe Voevodsky’s Univalence axiom gives the right way to think about this. A year ago, Steve Awodey told me that Univalence gives us isomorphic structures which are identical. Still, I think the problem in the case of physics involves this puzzling notion “represents the same world”, and the purely mathematical issue is not the same as the physical one. I think we shouldn’t think of a world as a “bunch of things with properties and relations”. I think we should think of a world as a bunch of properties and relations, related logically, saying how they’re interconnected. (This is a kind of relationism.)

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 5:43 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Hi John,

The univalence axiom seems very strict to me since it sounds like it says we should treat isomorphic objects as equal. I haven’t been able to understand why this doesn’t go against all the principles of categorification!

Could you say a few words about why it actually works out well?

Posted by: Tom Ellis on November 6, 2013 10:18 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

The univalence axiom is often advertised as saying “isomorphic types are equal” – but that has to be understood in the general context of intensional type theory. For one thing, it already implies that two types can be equal in two essentially different ways. It is less confusing if one does not think of intensional equality as equality as classically understood, but instead as paths: because it is not surprising that there can be two essentially different paths between two things!

Posted by: Zhen Lin on November 6, 2013 5:47 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

The key point which I generally emphasize is that univalence identifies isomorphism with equality not by strictifying isomorphism to become equality, but by broadening the meaning of “equality” to include “isomorphism”. So isomorphic types are equal, but not because we’ve collapsed the isomorphism, but because we’ve changed the meaning of “equal”!

Posted by: Mike Shulman on November 6, 2013 7:58 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Would you say, then, that univalence makes equality a weaker notion rather than isomophism a stronger one? Or perhaps more helpfully, prevents equality from becoming too strong a notion?

Posted by: Tom Ellis on November 6, 2013 8:59 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Yes, I think that’s roughly accurate.

Posted by: Mike Shulman on November 6, 2013 10:07 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

In fact I think this is what you are alluding to when you say

“in category theory we avoid distinguishing between isomorphic objects, whereas when we translate into set theory, it always becomes possible to distinguish between them in some way”

Posted by: Tom Ellis on November 6, 2013 9:00 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Right, so we need to deal with the issue of what the Vienna Circle called coordination, the mediation between scientific theory and empirical data. That was to be my (2) from above.

There’s a tradition in analytic philosophy which sees coordination as a straightforward process. A physical theory says that when certain things (bodies, fields, forces…) are present and arranged in certain ways, that they will evolve according to certain equations with initial conditions, so that some time later we will be able to predict the new configuration. Experiments will test these predictions. Enough successful predictions, and we may be inclined to take our theory to be true (or approximately true), suggesting to us that those bodies, fields and forces exist as stated in the theory. Of course, with an eye on the history of science, we may choose to be wary about being lured into believing the absolute truth of claims such as that there are forces acting instantaneously at a distance. Indeed, continual changes in science incline some people to be sceptical about any claims involving unobservables. Maybe then our theories can work as good instruments for prediction without telling us how things ultimately are.

Various issues now become the focus of realist/instrumentalist debate. The existence of many different competing theories making the same predictions (underdetermination) provides support for the instrumentalist, to which the realist demands “Show me serious cases where we really have such rival theories”.

Then there’s the case of symmetries, such as the gauge equivalence you mention, to which one may say that it’s not a specific field value that counts, but rather the equivalence class of fields under gauge symmetry. There’s a redundancy in the representation, such that two gauge equivalent fields refer to the same state. [Note to self: somewhere on the nLab (general covariance) it argues that this is the wrong construction. We don’t want a simple quotient, $Fields/G$, of orbits, but rather the orbit groupoid, $Fields//G$.]

One step further, Dean Rickles has a paper – The Interpretation of String Dualities – which presents another problem to this view that we can read off the ontology of a theory straightforwardly. What to make of dual string theories which make identical predictions and yet say very different things about the fundamental constituents of the world?

Dual theories provide distinct but ultimately physically equivalent representations. Do they thereby amount to underdetermination? I would argue that there are crucial and subtle differences. The dual theories are not in competition: they are complementary. They are both true in a sense, and the practice of physics suggests, in many cases at least, a pluralistic stance with respect to the dual theories. However, in many cases (perhaps, ultimately, all) the cases point to a deeper underlying structure, and in that sense neither dual theory is true in anything but an approximate sense.

But there are traditions other than the analytic one. Some would take us back to the 1920s to see if the Vienna Circle didn’t lead us astray with their radical anti-Kantianism. I mean by this various strands of Neo-Kantianism being explored today by Thomas Ryckman, Robert DiSalle, Michael Friedman (cf. Discourse on a New Method, Domski and Dixon (eds.), Open Court 2010). I find Ryckman very interesting. In his The Reign of Relativity he shows how deeply Husserlian Hermann Weyl was, and that one can’t understand the latter’s formation of gauge theory without this philosophical underpinning.

Friedman is (or maybe was) trying to return us to something more like the early Reichenbach, of the relativised a priori, before the latter later turned empiricist and realist. Ryckman objects:

Highly sympathetic to Friedman’s goal of showing that the constitutive office of transcendental philosophy has lost none of its relevance for philosophical understanding of modern science, I nonetheless have reservations regarding his attempt to refashion a contemporary transcendental idealism on the basis of Reichenbachian coordination principles. Thus, I shall project a somewhat different genealogy and role for the “relative a priori” in physical theory. (Domski & Dixon, p. 456)

What if the rise of HoTT is telling us that philosophy has taken the wrong path? Why were we pressing on endlessly with unabashed admiration for untyped predicate logic and set theory? If HoTT turns out to be the way forward, why has analytic philosophy played so small a role in its rise? Why did Martin-Löf find inspiration in Husserl? Was it because

…on Husserl’s view, logic (and mathematics) are not to be accepted “at face value” but like all objectivities (objects of knowledge or subjects of rational propositions) are to be considered as founded on subjective acts of thought, ultimately rooted in the analysis of pre-predicative intentional experience. It should be pointed out that such phenomenological analyses are to be regarded, neither as a metaphysics nor an empirical psychology, but as purely descriptive of the intentional contents and structures of cognizing consciousness. (Ryckman in Domski & Dixon, 461)

Does this also account for HoTT’s use in physics? Have we fundamentally misunderstood the role of mathematics (and its subpart logic) in the constitution of physical knowledge?

Posted by: David Corfield on November 4, 2013 11:57 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David, thanks …

What if the rise of HoTT is telling us that philosophy has taken the wrong path?

Yes, I know … philosophers are all wrong! :)

I think I’ll see you in Kent in a couple of months for a talk Julien invited me to, and maybe talk about Leibniz equivalence, as it’s connected to what I said to John and your point about “covariance” above, and see what you say. Actually, for the case of spacetime models $(M, g, T, \dots)$, I think the transformation group is not $Diff(M)$ (i.e., the automorphism group of $M$), but it is, rather, $Sym(A)$, the symmetric group of permutations of the carrier set $A$ of points in $M$. For under any permutation $\pi : A \to A$, we have,

$(\pi_{\ast}M, \pi_{\ast}g, \pi_{\ast}T, \dots) \cong (M, g, T, \dots)$.

And, therefore, these isomorphic models represent the same world.

On type theory, historically, I think the path of logic was dominated by type theory (e.g., see Godel 1931 and Tarski 1936); and later the relevant separation between first-order logic, higher-order logic and type-theory became clearer.

… which presents another problem to this view that we can read off the ontology of a theory straightforwardly.

I think I’d dispute that anyone believes this “view”. Quine stressed over and over again against his opponents that reading off ontological commitments is extremely difficult. A good standard work on this is Burgess & Rosen 1997, A Subject with No Object, which gives a variety of methods for showing how to translate one theory $T$ in $L$ into another $T^{\circ}$ in $L^{\circ}$. There are many methods for doing this. Quine discusses such cases – it’s what lies behind his arguments about indeterminacy of translation and referential instructability. Certainly, the standard authors - Quine, Putnam, etc. - all talk in detail about translations between theories.

E.g., in an unpublished short paper on arithmetic I wrote last year, we show how to translate second-order arithmetic $Z_2$ into the theory $PAF$ of arithmetic extended with “mereological fusions” of numbers. These theories seem to have different “ontologies”, but are inter-translatable.

So, for the physics case, consider a Lagrangian formulation and a Hamiltonian formulation of classical mechanics. In some sense, there is a translation (a syntactic mapping, preserving logical compounds and relativizing quantifiers). But because we lack a precise, first-order, formalization of classical mechanics, we can’t yet see how the translations work.

Suppose one just says, “Let’s start with a symplectic manifold $(M, \omega)$, …”, that doesn’t really help. Extremely serious and difficult conceptual work has to be done.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 4, 2013 11:35 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Yes, I know … philosophers are all wrong! :)

Well if HoTT wins out, Michael Dummett’s going to be in line for a reputation boost. And we can always stress the philosopher in Martin-Löf :)

I look forward to your visit to Kent. Maybe I could get something sensible together to say about (cohesive) HoTT on gauge equivalence by then. Already, I imagine there will be a difference about your $Sym(A)$ suggestion. I believe the symmetry is to be built into spacetime as an object of a certain category of smooth spaces, not as built up on the set of spacetime points.

Sure, the reading off of ontology is made tricky by the existence of translations. But there seems to be a difference in attitude between those using the tradition logical tools of philosophy and those using category theoretic ones. This contrast came nicely into focus in that discussion between Hellman and Awodey (e.g., Awodey’s reply). One thing is a difference in direction, cf. Awodey’s section ‘Top-down versus bottom-up’. (His latest on this theme, from a HoTT perspective, is Structuralism, Invariance, and Univalence.)

Regarding the alternative Lagrangian/Hamiltonian pictures, cohesive HoTT does have an account of the translation, so maybe a fruitful area to compare. But again here maybe we bump into the Awodey-Hellman issue.

So, there’s plenty to keep us busy!

Posted by: David Corfield on November 5, 2013 2:29 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks, David,

You can read my note on Leibniz equivalence here if you like. Given a spacetime model $(M, g, T, \dots)$, with carrier set $A$, there is no need to restrict to diffeomorphisms

$\phi: M \to M$

to generate gauge-equivalent models. Any permutation $\pi : A \to A$ of the carrier set (no matter how wild) yields an isomorphic copy of the original spacetime model, so long as everything is “pushedforward” under $\pi$. And therefore represents the same physical world. The group of such mappings is $Sym(A)$, not $Diff(M)$.

But there seems to be a difference in attitude between those using the tradition logical tools of philosophy and those using category theoretic ones.

Why not use both? Logicians use category-theoretical tools. Visser does for example. Visser has done a huge amount of work on interpretability between theories, by the way.

This contrast came nicely into focus in that discussion between Hellman and Awodey (e.g., Awodey’s reply).

One problem here is that Steve (Awodey) advocates an “if-thenist” philosophy. For example, Steve states:

Every mathematical theorem is of the form “if such-and-such is the case, then so-and-so-holds”. (p. 6)

This kind of “if-thenism” is a very old-fashioned view (as Steve goes on to note, citing Russell). But it faces serious problems. It cannot deal with the applicability of mathematics. For example, when I assert the existence of a set of apples, I do not mean a conditional claim,

If $ZFU$ holds, there is a set of apples.

I just mean the straight-out claim:

There is a set of apples.

Similarly, when I assert the mathematical claim,

There is a proof $P$ of $\phi$ in $PA$

I do not mean the conditional claim,

If such-and-such is the case, then there is a proof $P$ of $\phi$ in $PA$.

If I assert,

There is a bijection $f : \{x \mid Beatle(x)\} \to \{x \mid Kink(x)\}$

then I mean that there is a bijection. I do not mean,

If such-and-such holds, then there is a bijection $f : \{x \mid Beatle(x)\} \to \{x \mid Kink(x)\}$

The problem here is that “if-thenism” is incompatible with the applicability of mathematics.

Jeff

Posted by: Jeffrey Ketland on November 5, 2013 11:49 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

What does the applicability of mathematics have to do with Steve’s observation, which is a statement about mathematics in its own right?

Posted by: Mike Shulman on November 6, 2013 4:24 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, in the section in Steve’s reply to Hellman, Steve mentions that it’s a form of “if-thenism”, like Russell’s. So, the idea is that the true mathematical claims we should accept all have the form

if such-and-such axioms hold, then $\phi$.

(People find this philosophical view attractive because it is epistemically weak. To check such a thing holds, you only need to write down the axioms, and see if you get $\phi$ out. Consequently, on this view, maths can be reduced to making almost arbitrary stipulations, and then working through the consequences. So, it’s sometimes called “deductivism” too.)

But if-thenism has a problem dealing with mathematical statements required in applications like,

(i) There is a set of Fs.

(ii) If there is exactly one apple and exactly one orange, then $\{x\mid Apple(x)\} \cong \{x \mid Orange(x)\}$.

where “$Fx$” is a predicate for some kind of physical thing to which we want to apply maths: e.g., assign a cardinal number to $\{x \mid Fx\}$, or we might want to assign masses to the elements of $\{x \mid Fx\}$, and define “the average mass of an $F$”.

But these mathematical statements (they called “mixed-mathematical statements” by people who write about applicability) aren’t of the “if certain axioms hold, then $\phi$” form required by if-thenism. In applications, we assert them outright, rather than conditionally.

So then do these mixed statements like (i) and (ii) that we use in applications count as mathematical statements? If they do, then if-thenism doesn’t work for them. If they’re not mathematical statements, then what to say about them!

But, having said all that, now I’ve just reread Steve’s section again for the third time, and maybe his “if-thenism” isn’t what Russell’s was. I think (but I’m not sure) he does want to avoid asserting the axioms outright, and only state conditional claims. If so, then it is the usual “if-thenism” view, which faces the applicability problem. On the other hand, there’s some further structuralist point about the indeterminacy of the objects referred to, a bit like Hilbert’s “table, chairs and beer mugs” statement on geometry.

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 6:40 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Right, so Steve’s is not a Russellian if-then-ism, but rather a ‘whenever this is the situation, that holds’.

Thinking about your apples and oranges, we have a result in unapplied HoTT which says informally that whenever we have two types which are sets, and where both have the same cardinality, then there is an isomorphism between the types. Indeed, this isomorphism would even be constructed and depend on the isomorphisms of each type with whatever was being used as standard cardinality.

Presumably then to apply this to the contents of my kitchen, I say to myself something like, I’m framing the situation as involving a type $Thing$, which may need to encode a range of assumptions, individuation (I’m not including things like the heat of the room), stability (so I can leave out time considerations, that is, it’s not a dependent type on time), and so on, so that in particular this type $Thing$ satisfies the $IsSet$ property.

Then I can form $Apple$ and $Orange$ as subtypes of $Thing$, as Mike explained above. I should have already proved that a subtype of a set is a set. Now my unapplied result can be used to assure me that if the cardinalities of the apples and oranges match, then there’s an isomorphism between them.

So I think we’re still dealing with a Steve-like whenever-ism. If apples and oranges are the kinds of things that behave as though they constitute sets, then…

On the other hand, raindrops running down my window don’t behave like this.

Posted by: David Corfield on November 6, 2013 10:23 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

Yes, that sounds the right way to build applicability into the HoTT approach. So, the idea is to postulate a type PhysThing.

But then it seems to me this has only to satisfy the quite general Quinian condition:

Is the content of any portion of spacetime, no matter how irregular.

Then the four-dimensional raindrop-content of spacetime, no matter how higgledy-piggledy the motion, will count as being of type PhysThing.

(Whether PhysThing is called a “set” or a “type” I don’t care much. It’s pretty much a verbal issue, I think.)

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 1:17 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

(Whether PhysThing is called a “set” or a “type” I don’t care much. It’s pretty much a verbal issue, I think.)

I think I’d disagree with this.

That a type is a set in HoTT’s sense means something quite considerable. We have as a type construction rule that given any two terms, $a$ and $b$ of a type, $A$, there is a new type $Id_A (a, b)$. We can only say that $A$ is a set (hlevel = 0) if for any such terms, $Id_A (a, b)$ is a proposition (hlevel = -1).

Now this is intuitively saying that there’s a yes or no answer to whether $a$ and $b$ are the same. So a set is the kind of type for which terms are either the same or different. If they are the same, so the identity type is inhabited, that’s contractible.

Apples are just like this: for any two apples, either they’re the same or they’re different. If they are the same, they’re the same in one way.

But some types are not like this. The type of types itself isn’t. Treating it like a set is wrong in HoTT.

It’s reasonable then for there to be types relevant to physics which are not sets. The moduli spaces of values of QFTs that Urs discusses, for example, are not sets.

Posted by: David Corfield on November 7, 2013 12:25 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

So a set is the kind of type for which terms are either the same or different.

While I agree with the general point you’re making, I think this way of phrasing it is confusing, because it seems to conflate 0-truncation with decidability/LEM. I would say rather that a set is the kind of type for which if two terms are the same, then they are the same in a unique way.

Posted by: Mike Shulman on November 7, 2013 5:51 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

If apples and oranges are the kinds of things that behave as though they constitute sets, then…

Yes, exactly. The defining thing about an if-then statement is that if you can check (or believe) the hypotheses, then you have (or believe) the conclusion. A statement about apples and oranges manifestly cannot be a mathematical statement, because apples and oranges are not mathematical objects. But if we believe that they satisfy the axioms of ZF (or more precisely, that it’s reasonable to model them with mathematical objects satisfying the axioms of ZF), then we should believe that they also satisfy the theorems of ZF. I don’t see any problem.

Think of it this way: we have a collection of things we believe about the world. An if-then statement is a function that takes as input some collection of things we believe and produces as output something else that we should believe. Saying that all mathematical statements are if-then statements doesn’t prevent the non-mathematical things we believe about the world from being absolute.

Posted by: Mike Shulman on November 6, 2013 7:52 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

Surely, apples and oranges don’t constitute sets! They are urelements, i.e., non-sets, to which we apply set theory, using comprehension. But the set of apples is a set, by definition. And the set of spacetime points is a set, even though the spacetime points are not sets (spacetime points are urelements).

Suppose I am doing a physics problem, and I want to define the average mass of a US citizen. I apply comprehension and define

$C = \{x \mid Citizen(x)\}$

Then, given that, for each physical thing $x$, we have its mass, $m_{kg}(x) = r$, we can define,

$\overline{m}_C = \frac{\sum_{x \in C} m_{kg}(x)}{|C|}$

This number $r = \overline{m}_C$ is the average mass (in kg) of a US citizen.

But the problem with “if-thenism” is that $ZFU$, say, doesn’t imply, e.g., $\overline{m}_C = 75$. Rather, the mixed statement,

$\overline{m}_C = 75$

is contingent: its truth or falsity varies from world to world, depending on how many US citizens there are, and what their distribution of masses is.

$ZFU$ doesn’t imply anything contingent! In the case of set theory, it is applied via comprehension axioms (which allow us to assert the existence of sets of non-mathematical things) and certain primitive predicates (e.g., of physics) relating physical things to, e.g., numbers (as their masses), or to vectors (as field strengths), etc.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 7, 2013 7:23 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Well, apples and oranges are not sets, but they constitute sets, i.e. together all the apples form a set. Or, at least, they would if apples were mathematical objects. ZFU can’t actually talk about real-world apples, since they are physical objects and not mathematical ones, but there can be urelements that we call “apples”.

You then go on to say “the problem is”, but I don’t see a problem. (-:

Posted by: Mike Shulman on November 7, 2013 6:08 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

MIke, thanks - actually, on the basic issue about applicability, the method works similarly in both cases, as you said earlier: one way, by set-theoretic comprehension, or on the HoTT way, by postulating “physical types”.

But I still think the issue with mixed statements of science and “if-thenism” does remain a problem. For almost all the contingent statements/laws etc, of physics and applied mathematics are mixed statements, e.g.,

(1) There is a bijection $f : \{x \mid Apple\} \to \{x: Orange\}$.

(2) For each point mass $b$ and time instant $t$, $\underline{F}_b(t) = m_b(t) \times \underline{a}_b(t)$.

(3) at each spacetime point $p$, $(\nabla \cdot B)(p) = 0$.

These differ from pure statements of mathematics, such as,

(4) $|\mathcal{P}(\mathbb{N})| > |\mathbb{N}|$.

We expect any decent foundational theory $\mathbb{F}$ to be able to formalise (4) and give (4) as a theorem. So, the “if-thenist” might insist that they don’t believe (4) to be true; rather, they believe

$\mathbb{F} \vdash (4)$.

In other words, they believe that there is a derivation of (4) from the axioms of $\mathbb{F}$. This means that they needn’t in fact be committed to thinking there is an infinite set. They merely think,

IF there is an infinite set, then its power set is larger.

But neither ZFU nor HoTT implies (1), (2) or (3)–because they’re about non-mathematical entities. They’re not theorems of mathematics. But nonetheless, they use both mathematical predicates (e.g., “set”, “bijection”, “sequence”, “vector”, etc.) and non-mathematical predicates (e.g., “spacetime point”, “point mass”, etc.).

The underlying point is that physical laws are mixed mathematical claims, using both mathematical and non-mathematical predicates in their formulation, and they’re contingent – they’re not theorems of one’s favourite foundational theory $\mathbb{F}$, per se.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 8, 2013 3:29 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Ah, I think I see. I think the problem lies in a confusion between mathematical objects and what they model. On the face of it, statements like (1)–(3) are meaningless because, for instance, a mathematical function like $F$ cannot be evaluated at a non-mathematical object like a particle; it would be like writing “$Jeff^2+2$”. Instead, the sense in which they are true is that we construct mathematical structures containing mathematical objects which we call “point masses” and “time instants” and “spacetime points” because we are thinking of them as representing something or other in reality, and then (1)–(3) become true mathematical statements about these structures (relative to some foundational mathematical system). But the statements don’t make sense if we forget the step of mathematical modeling and think that the word “spacetime point” refers directly to something in physical reality.

Posted by: Mike Shulman on November 8, 2013 7:29 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

I agree, I can’t be squared!

On the face of it, statements like (1)–(3) are meaningless because, for instance, a mathematical function like $F$ cannot be evaluated at a non-mathematical object like a particle.

Isn’t this what applied mathematics is? Consider, e.g., the mass-in-kg function, $m_{kg}$. This function applies to a physical thing, and outputs a non-negative real. So, e.g.,

$m_{kg}(Jeff)$ > $m_{kg}(Mike)$

is a perfectly fine, meaningful statement of applied maths. People who work on the topic of applicability call predicates like

$r = m_{kg}(x)$

“mixed” predicates (I think this terminology comes from Quine). They relate non-mathematical and mathematical things.

So, e.g., Maxwell’s equations are contingent claims, about certain fields on space-time. E.g.,

at each spacetime point $p$, $(\nabla \cdot B)(p) = 0$.

Talk about “modelling” is useful, but it’s confusing. There is no precisely defined notion,

Mathematical model $\mathcal{M}$ models physical system $P$

But if one attempts to define it, it turns out to involve all these mixed-functions, i.e.,

(i) quantity functions, like $m_{kg}$,

(ii) field functions on spacetime, like $E,B,J,\rho$, etc.

Jeff

Posted by: Jeffrey Ketland on November 8, 2013 8:55 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

That is correct, it is not precisely defined, because it is not part of mathematics; it is part of the application of mathematics to something. It’s semantic whether you consider “applied mathematics” to include the application or only the mathematics that is applied, but whatever you call it, the process of application is not part of the actual mathematics and hence does not need to be described precisely by a mathematical foundational theory.

Posted by: Mike Shulman on November 9, 2013 3:44 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David, I should have added - the underlying sub-issue here is not really about “co-ordination”. This is a separate, epistemological, issue that was of interest, as you rightly say, to the logical empiricists, and earlier figures (like Mach, Helmholtz, Poincare, Russell) who influenced them. This involves some kind of “theory/observation” split. But what is being discussed here is not connected to “theory/observation”, or any epistemological issue, or anything to do with “realism/instrumentalism”. The foundational issue I mentioned is not epistemological.

The issue concerns applicability and representation, rather than (epistemological) co-ordination. So, e.g., I have an apple. This is something I can pick up, throw up in the air and so on. Ten minutes later, I am talking about a trajectory

$\gamma : [0,1] \to \mathbb{R}^4$.

But then why? This is a difficult foundational question in physics. How do theories, etc., represent the world. Why should $\mathbb{R}^4$ be connected to apples? For a really trivial example, it’s not clear to me how I express, say,

$|\{x\mid apple(x)\}| \geq 3$

in HoTT? Or can I assert,

$\exists z \forall x(x \in z \leftrightarrow apple(x))$

in its language? I searched the book for “comprehension axioms” and couldn’t see how this is meant to work. (Admittedly, maybe this is my fault and I’m looking in the wrong place, or for the wrong kind of thing.)

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 5, 2013 2:29 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

In set theory, you can get the set of apples by taking the set of all things that happen to be apples, but in type theory, there is no “type of all things” — everything that exists, exists with some type. However, if you have (say) a type of all fruit, then you can build from it the subtype of all apples:

$Apple \coloneqq \sum_{X:Fruit} IsApple(X)$

This is in section 3.5 of the book. Cardinalities of sets are discussed in section 10.2. There is no very extensive discussion of finite sets and their cardinalities, mainly because it doesn’t look any different from the classical (structural) case. For instance, you would say that $Apple$ has cardinality at least 3 by (merely) asserting an injective function from the standard 3-element set $\sum_{n:\mathbb{N}} (n\lt 3)$ into $Apple$.

Posted by: Mike Shulman on November 5, 2013 6:24 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks, Mike -

Does this mean, for any predicate $P(x)$ applied to non-mathematical entities, we always have a corresponding type? E.g., in set theory with urelements, $ZFU$, in a language $L$, we assert the existence of a set $U$ of all urelements (all satisfying “$x$ is an urelement”), we state that urelements have no members, and we restrict extensionality to sets,

$\forall x \notin U \forall y \notin U (\forall z(z \in x \leftrightarrow z \in y) \to x = y)$

Then, for any formula $\phi(x)$ whatsoever in $L$ (e.g., applying to urelements or not), we have by separation, the existence of the set $\{x \in U \mid \phi(x)\}$ by applying separation,

$\exists z\forall x(x \in z \leftrightarrow (\phi(x) \wedge x \in U))$

It’s this comprehension principle which allows us to assert the existence of sets of physical things: e.g., sets of spacetime points, regions, and so on.

But in type theory this works somewhat differently: what is the comprehension principle stating what types exist?

Jeff

Posted by: Jeffrey Ketland on November 5, 2013 10:57 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Yes, it’s correct that in type theory, for every predicate $P(x)$ the variable $x$ has a specified type, so that $P$ can only be applied to objects of that type. Types in type theory are not “cut out” of a universe of everything by a comprehension principle. Rather, they are “built up” using rules of type construction. For instance, one of the rules says that we have a type $\mathbb{N}$ of natural numbers. Another of the rules says that if $A$ and $B$ are types, then we have a type $A\to B$ of functions from $A$ to $B$. Thus, we have types such as $\mathbb{N}\to\mathbb{N}$ of functions from naturals to naturals, or $(\mathbb{N}\to\mathbb{N}) \to (\mathbb{N}\to\mathbb{N})$ of functionals acting on such functions, etc.

I would personally shy away from making any claims about predicates applied to non-mathematical entities, since type theory is a mathematical theory (as is set theory, for that matter) and so all objects involved are mathematical. But I could imagine that in type theory used to model, say, natural language or human reasoning, you would have (say) a type of people, and a type of boulders, and a type of houses, and so on, and in a predicate like $P(x)=$$x$ is friendly” the variable $x$ would have type $Person$, since saying that a boulder is friendly is not very sensical. I’m sure there are people who’ve thought about this a lot more, like David here.

Posted by: Mike Shulman on November 6, 2013 4:38 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks - yes, I’m clearer now about how this works in HoTT, in principle. For informal set theory in applications, the comprehension assumptions for non-mathematical predicates are considered kind of obvious, so people don’t stop to write them down explicitly. In the type-theory adopted in HoTT, there are the basic types (e.g., $\mathbb{N}$, and universes), and then you can introduce further basic types for non-mathematical predicates, if you wish.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 8:10 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

But it still does not seem to give new insight into foundational questions – it just seems to reformulate them.

One curious thing about field theory is that one tends to forget what the glaring foundational questions are. For instance it’s a habit of adopting perturbation theory, both in $\hbar$ and in the coupling, and make global obstructions a side issue – verbatim an “anomaly” – to be treated by those esoteric articles that one points to but never reads. But in a fundamental description of quantum field theories anomalies, gauge reductions and similar global effects must be part of the foundations, not the add-on. Perturbation theory emerges as the infinitesimal approximation to a globally well defined fundamental structure, not the other way around.

These issues happened to become more pronounced and more recognized with the study of string theory due to the more pronounced role that higher gauge principles play there, but since string theory is a big dictionary of quantum field theory, it applies to the latter just as well.

I am familiar with the superficial attitude voiced in some comments here that “none of this solves anything”, but the fact is that when we started working on this, nobody knew the answers that now are sometimes claimed to be so obvious. Such as “What is a higher nonabelian twisted gauge field, such as the supergravity C-field?”

That’s the kind of concrete questions that had motivated the development of some machinery to attack it. That this machinery then eventually turned out to be more fundamental than one had had any right to expect when we started is a happy byproduct that wasn’t intended. For the description of higher nonabelian differential cohomology I had started to consider higher moduli stacks which were equipped with a notion of higher fundamental groupoids. That there is a natural axiomatization of this which not only axiomatizes differentialy cohomology neatly, but which also, as if out of itself, produces an axiomatization of a good bit of non-perturbative field theory generally is something that wasn’t intended, it just happened.

Physics comes out like this. Cohomology is mapping spaces in homotopy toposes. Differential cohomology is mapping spaces in cohesive homotopy toposes. Regarding a cocycle in such a differential cohomology theory as an object in the slice over its codomain in the natural way turns out to define a pre-qauntized local Lagrangians. Regarding such as an object in the homotopy n-category of correspondences in a slice defines a non-perturbative topological field theory. Its boundary data defines non-topological field theories. The non-perturbative globally well defined formulation of Hamilton-de Donder-Weyl covariant field theory just drops out this way, for each such local action functional. All anomaly cancellation and global higher gauge transformations inclusive. Quantization is given by the natural cohesive motivic linearization and captures the plenty of the subtle aspects usually ignored.

Posted by: Urs Schreiber on November 5, 2013 8:20 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Urs, thanks - yes, so all that is conceptually unifying, and it means that smaller bits of the picture fit into a bigger picture. Maybe a simple historical analogy is that, pre-SR, space and time were treated separately and then “combined”; we get Minkowski space; and we can then see that classical Newtonian mechanics can be reformulated as a kind of approximation (where there is a single special foliation of spacetime: absolute simultaneity). Or, in GR, we realise that the Newtonian gravitational potential $\Phi$ corresponds to $g_{00}$, to first approximation. So, your monograph both reformulates and generalizes, going up a kind of “ladder”, in John’s phrase. And those are related to some foundational questions, because they unify seemingly different phenomena into a single bigger picture.

But other foundational questions remain! Not about what happens “higher-up”, but, in a sense, lower down. So, I mentioned applicability/representation. In set theory, one takes sets of urelements and all is ok. But how this works in HoTT is not so clear – because it’s not clear what types can be asserted to exist. (In set theory, these are comprehension axioms.) And “gauge equivalence” (or “Leibniz equivalence”, or “diffeomorphism covariance”) in GR is still quite puzzling. Does HoTT help here? Maybe it does.

(One might prefer an approach to Hilbert’s 6th problem that wrote everything down in standard first-order predicate logic, making it absolutely clear what the basic predicates are, what the comprehension axioms are, etc.)

Another aspect of HoTT approach is that the background logic here is intuitionist, which involves the intuitionistic assumption that each truth is knowable:

(K) If $\phi$ then it’s knowable that $\phi$.

and the related BHK interpretation of the connectives. E.g., a proof of $A \vee B$ is, roughly, a proof of $A$ or a proof of $B$. But this is a pretty strong assumption. Are non-constructive proofs illegitimate?

Again, related to HoTT, is structuralism: this is the topic of the recent nice paper, “Structuralism, Invariance and Univalence” by Steve Awodey that David mentions a bit above. In 1965, Paul Benacerraf published a famous article, “What Numbers Could Not Be”, noting that you can implement the natural numbers in set theory in various, mutually incompatible, ways; but it’s a matter of indifference in practice. So, numbers aren’t sets. And Benacerraf suggested that numbers aren’t even objects at all! So, the idea being mooted now is that category theory, along with Univalence, sheds light on this. And that is something that is still very unclear.

So, overall, whether HoTT specifically helps with all this (i.e., applicability, representation, underlying logic, structuralism) – either in foundations of mathematics or in the foundations of physics – is something I’m not sure about at all. (David thinks it does.)

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 3:22 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

HoTT logic does not have to be intuitionist. It’s perfectly fine to add LEM as an axiom. Taking the basic logic to be intuitionist just gives us more freedom, to choose to assume LEM or not as we please. Non-constructive proofs are not necessarily illegitimate, they’re just not constructive, and if we only want constructive proofs then we choose a logic which ensures all our proofs are constructive. Using an intuitionistic logic doesn’t automatically entail any particular ontological assumptions about truth; avoiding LEM when you don’t need it is just going for a bit more generality, like stating a theorem about all monoids rather than about all groups.

Posted by: Mike Shulman on November 6, 2013 5:00 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, I agree with all of that - but that’s the classicist’s attitude!

Intuitionism places constraints on truth and proof, e.g., “each truth is knowable”,

If $\phi$, then it’s knowable that $\phi$

and on how proof relates to the connectives (BHK: roughly “proof commutes with logical connectives”). From these, we get that non-constructive proofs are somehow illegitimate (and the model theory - e.g., using Kripke models - shows how to give counter-examples to LEM).

The classicist responds to this by saying, e.g., that LEM is legitimate, but non-constructive. So the classicist has a liberal view, and the intuitionist imposes restrictions - “don’t use LEM!”. So, e.g., Douglas Bridges in his SEP on “Constructive Mathematics”, writes,

Thus just as mathematicians will assert $P$ only when they have decided that $P$ holds by proving it, they may assert $P \vee Q$ only when they either can produce a proof of $P$ or else produce one of $Q$. (First section)

But maybe that’s not what you mean by intuitionism; then I can’t quite figure out what you mean by classicism about logic. The classicist says you can choose to use LEM, or not. The intuitionist (e.g., Dummett, Bridges, others) says you cannot use LEM, because - on their philosophical view abut “proof” - to assert $A \vee \neg A$, you must have already proved either $A$ or $\neg A$.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 2:23 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

The statement “HoTT logic is intuitionist” is a mathematical statement, and therefore does not say anything about an attitude. It merely states that the default logic of HoTT lacks LEM. One can approach this mathematical fact from the philosophical perspective of an intuitionist, saying “excellent, this is the One True Way to do mathematics”; or from the philosophical perspective that I would call “classical”, saying “that’s dumb, but fortunately we can just add in LEM”; or from the philosophical perspective I advocate and call “pluralist” or “relativist”, saying “that’s good, so we can put in LEM or not, as needed or appropriate for the particular application”. The point I’m making is that there’s nothing intrinsic about the mathematics of HoTT that mandates approaching it with an intuitionist philosophy.

Posted by: Mike Shulman on November 6, 2013 7:45 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

But it seems like the “propositions as types” view, where one says “a proposition is the type of its proof”, is a philosophical view? And isn’t the BHK interpretation of “proof” also a philosophical claim?

Suppose a mathematician is told the basics of HoTT (or intuitionistic type theory), and simply denies that a proposition is the “type of its proof”. They argue like this:

We only have proofs for a tiny proportion of mathematical claims! So, infinitely many mathematical propositions lack a proof. For example, the class $Th(\mathbb{N})$ of arithmetic truths is highly non-recursive (not even arithmetically definable). Even the $\Pi_1$-truths are not r.e. - so what/where are the corresponding “proofs”? And so there’s no reason to suppose every arithmetic truth has a proof.

So, isn’t the claim that a mathematical proposition is “the type of its proof” a philosophical view, and one that can be disputed?

The point is that there is a philosophical view here about “proofs” and “propositions” and about the relation between the meanings of the connectives and the notion of “proof” – this eventually tells us that LEM is illegitimate, because to prove $A \vee \neg A$ one must already have proved $A$ or $\neg A$. So, it seems that HoTT, being based on Martin-Löf intuitionistic type theory, is presupposing a certain philosophical view.

Your response to this is eminently sensible! – “Oh, we can add LEM when we like …”. Which is actually the classical view; but then it’s not so clear that your liberalism about LEM is compatible with the underlying philosophy, of “proposition = type of its proof”. An intuitionist/constructivist (e.g., Bridges, Dummett; maybe Martin-Löf too) is going to be unhappy about this … and say,

How can you assume there’s a determinate fact about Goldbach’s Conjecture, say, until you’ve decided it one way or the other?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 7, 2013 5:44 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

But it seems like the “propositions as types” view, where one says “a proposition is the type of its proof”, is a philosophical view?

I would say, absolutely not. There is a true mathematical difference in the way that type theory and set theory deal with logic, and that’s what I refer to as “propositions as types”.

In set-theoretic foundations, one first formulates the deductive system of first-order logic, and then describes set theory by giving axioms within this system. Thus, logic is “outside” the foundational theory, existing at a “lower level”. By contrast, in type-theoretic foundations, the type theory is itself the basic deductive system. One then finds logic inside of type theory, by identifying certain types to call “propositions” and whose elements we call “proofs” (or, less confusingly, “witnesses”).

Propositions-as-types, in this sense, is not tied to an intuitionistic logic or philosophy. It remains true if we add LEM as an axiom to type theory; in that case it just so happens that the type $\prod_{(A:Type)} A\vee \neg A$ has an inhabitant. It’s only when you combine the mathematical description of propositions as types with the philosophical position that all elements of types must be computable that you reach the philosophical position of intuitionism in its BHK form.

It might be the case that some people use the phrase “propositions as types” to also encompass this philosophical attitude. But the mathematical fact that HoTT is based on MLTT, and treats propositions in the particular way described above, doesn’t require it to accept any philosophical attitude.

Posted by: Mike Shulman on November 7, 2013 5:47 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

What I rather suspect will happen as we proceed is that the tasks you describe as philosophical will be modified. Many of the puzzles that have arisen have done so because the picture provided by set theory and first-order logic has been so strongly internalised.

For example, you frequently resort to the language of ‘up’ and ‘down’, and that philosophy needs to resolve issues downwards. I suspect we’ll find this drive arises from a set-theoretic outlook. For example, the Benecerraf problem (about there being different set theoretic manifestations of the natural numbers) fades away if we adopt a HoTT approach. The natural numbers are no longer to be seen as built up from elements we’ve already constructed. Doing it that way, of course we will wonder what to make of alternative constructions leading to isomorphic entities. Again thinking set theoretically, we may try the equivalence relation idea in order to group together isomorphic structures, but then this is unsatisfactory in other ways.

Doing things the HoTT way, we just don’t run into that problem. I define the natural numbers as an inductive type. If you now can form a type that is equivalent (in the technical sense) to mine, then everything we are allowed to say in HoTT about each others’ types is the same. They’re just not rooted downwards in some underlying stuff.

I think maybe something similar is happening with regard to some questions about physics.

One odd thing that has transpired over the past century is this sense of a division of labour between the practitioners (mathematicians, physicists, etc.) getting on with their thing, and then the philosophers doing something very different, by trying to make sense of what the former are doing. I suspect again that this in an effect of a belief that a certain foundational language is here to stay.

It was partly through the recognition that set theory is inadequate as a language for mathematics, that (some) practitioners have been led to devise alternatives, resulting today in HoTT. And it was quite possible for philosophers to have joined in on this task. Indeed some did!

Similarly working out the meaning of gauge equivalence is not a task handed onto the philosopher by the physicist. They themselves needed to work out what was going on with higher equivalences, why they were being forced to resort to ‘ghost’ fields, etc. They are the ones most likely to get their house in order, if ideally with some philosophical prompting, and if this takes them in the direction of higher groupoids and dovetails with HoTT then what won’t profit anyone is to pose a range of set-theoretic inspired questions on gauge equivalence.

This certainly doesn’t render philosophers useless, but it’s much more likely to be a collaborative process. Gauge theory begins with Weyl being thoroughly Husserlian. Now with the idea of cohesive $\infty$-toposes the very notion of space is coming under scrutiny. There are very rich traditions in our past, going back to Leibniz and further, and even to be found in Hegel. Go to the nForum and you see Urs is reading The Science of Logic, just as Lawvere had earlier, inspiring him to the notion of cohesion. How much better had Hegel teamed up with Cauchy to codify his ideas!

Posted by: David Corfield on November 6, 2013 12:35 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

It was partly through the recognition that set theory is inadequate as a language for mathematics.

Isn’t set theory simply a theory of sui generis mathematical entities, $\varnothing, \mathcal{P}(\varnothing), \dots$, forming a very large structure $(V, \in)$, the cumulative hierarchy of pure well-founded sets?

The foundational point, which became clear during the crucial foundational period from Frege (1879) to von Neumann (1925), say, is that all mathematical structures of interest can be interpreted in $V$. That is, there is a translation that maps all the axioms of one’s favourite theory into $L_{\in}$ so that they become theorems of $ZFC$, say.

Is something wrong with this mathematical discovery?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 6, 2013 1:37 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Is something wrong with this mathematical discovery?

Nothing wrong with it at all. The discovery that all of mathematics could be done in one system was very beneficial.

The problem comes from taking the inconveniences Mike mentions below as problems that philosophers should deal with independently of mathematicians, rather than joining in the search for a more convenient foundation. The latter is overwhelmingly likely to be being forged in the daily practice of the discipline, even if it’s only a few who explicitly contribute.

Keeping an eye on what Grothendieck was doing would have been a good idea for philosophy, even if rather challenging!

Posted by: David Corfield on November 7, 2013 1:01 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

Keeping an eye on what Grothendieck was doing would have been a good idea for philosophy, even if rather challenging!

Ah - I think the situation is the reverse. :)

Mathematicians and theoretical physicists interested in foundations need to study the works of Quine, Kripke, Putnam, Benacerraf, Field, Shapiro, Burgess et al, in order to make progress with their problems. So far as I can see, Grothendiek is irrelevant to any issue that arises with applicability, representation, coding, logic, modality, translations between theories, etc. But Quine, Kripke, Putnam, Benacerraf, Field, Shapiro, Burgess, etc., are extremely important.

So, I think that, instead of ignoring all of this important foundational work, people interested in these topics should study the research literature. For example, Field’s Science Without Numbers or Burgess & Rosen’s A Subject with No Object. This is hard, admittedly. But if one wants to make progress with, say, Hilbert’s 6th Problem, I think one must read the relevant research literature on foundations.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 8, 2013 3:50 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mathematicians and theoretical physicists interested in foundations need to study the works of Quine, Kripke, Putnam, Benacerraf, Field, Shapiro, Burgess et al, in order to make progress with their problems.

Gosh! There is a clash of intuitions.

Of course, much will hang on what you mean by ‘foundations’. But I hope you’ll agree that were HoTT to succeed in its ambition to become the language of choice for mathematics, one for which no doubt an informal variant will emerge, but close enough to the formal version that coding it for a machine is feasible, then this would concern the foundations of mathematics. But HoTT owes a huge amount to Grothendieck and very little, if anything, to any of the people you mention (Kripke for presheaf semantics for modal logic providing a line to toposes might be the biggest exception).

I would agree that Benacerraf drew attention to the oddity that the official foundational language of the day allowed questions to be posed which had no sensible answer, e.g., “Does $0$ belong to $1$?”, but where has the effective work been done in generating a system which enshrines the principle that isomorphic structures are to be treated identically? Type theory, categorical logic, topos thery, abstract homotopy theory,… It’s not by chance that Voevodsky, Awodey, Shulman are key players now, and, looking back, Grothendieck is revered.

But perhaps HoTT could not in principle satisfy you as a foundation for maths, or only with a overlay of genuinely philosophical interpretation?

Relating to physics and Hilbert’s 6th problem, you can’t mean for physicists to read Field, Burgess and Rosen to help them resolve their conceptual problems, can you? Perhaps you mean there’s an extra philosophical task of understanding how application and representation work. I could see an engagement with Norton and Butterfield as more likely to lead somewhere.

Perhaps a useful thing for me to do would be to present some of the bold claims we have on the nLab into something that a philosopher of physics might want to engage with.

E.g., at general covariance we have

principle of equivalence in mathematics $\Rightarrow$ principle of general covariance $\Rightarrow$ principle of equivalence in physics.

Posted by: David Corfield on November 9, 2013 11:46 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

That isomorphic models $\mathcal{A},\mathcal{B}$ are structurally the same is agreed by everyone, and the idea that mathematics only deals with such things “up-to-isomorphism” is a common theme to all structuralist views, going back to Dedekind and Hilbert. But making precise sense of this is by no mean done and dusted.

As far as I understand it, the Univalence axiom does not say that isomorphic objects are the same (which is astonishing); rather, it says that isomorphic objects bear some “indiscernibility” relation–with respect to certain properties (that there exist certain paths), which is not astonishing at all; that’s something everyone already agrees with. For example, in higher-order logic, if $\mathcal{A} \cong \mathcal{B}$, then $\mathcal{A} \models \phi$ iff $\mathcal{B} \models \phi$, for any formula $\phi$.

Here are a few recent contributions to Hilbert’s 6th problem, in connection with formalizing relativity. The authors are generally from, or connected to, the Eotvos Lorand University, Budapest.

1. Szekely, G. 2009: “First Order Investigation of Relativity Theory with an Emphasis on Accelerated Observers” (PhD dissertation.)

2. Andreka, H., Madarsz, J. Nemeti, I, & Szekely, G. 2012 “A Logic Road from Special Relativity to General Relativity” (Synthese 2012)

3. Hoffmann, B. 2013: “A Logical Treatment of Special Relativity with and without faster than light observers”.

The formalizations take place in first-order predicate logic.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 1:15 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I would say that the univalence axiom suggests that the phrase “the same” should be redefined to mean “isomorphic”.

Posted by: Mike Shulman on November 10, 2013 5:33 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

As far as I understand it, the Univalence axiom does not say that isomorphic objects are the same (which is astonishing)…

I really recommend this paper:

Near the end he concludes:

In sum, the Univalence Axiom is a new axiom of logic that not only makes sense of, but actually implies, the Principle of Structuralism with which we began,

Isomorphic objects are identical.

This seems quite radical from a conventional foundational point of view, and it is indeed incompatible with classical foundations in set theory. It is, however, fully compatible and even natural within a type-theoretic foundation, and that is part of this remarkable new insight.

That’s why earlier in this conversation I called the univalence axiom the most important recent thought when it comes to the subject of equality, isomorphism, equivalence, and other concepts of ‘sameness’. It’s a very exciting shift in views.

Posted by: John Baez on November 10, 2013 6:49 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks, John. Yes, I know Steve’s paper. He showed me an earlier version (in 2012, I think) in Munich, and I linked to it here a couple of months ago.

I think, though, that the univalence axiom is changing what $=$ means, to something weaker. That we might have,

If $A \cong B$ then $A \equiv B$

for some interesting equivalence relation $\equiv$ is not so surprising.

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 12:47 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

I think, though, that the univalence axiom is changing what = means

Yes.

… to something weaker.

I wouldn’t say that.

Remember: even before the univalence axiom comes along, equality already means something very different in homotopy type theory than it did in set theory. In homotopy type theory you shouldn’t think of equality as a relation between sets.

For starters, to get your intuition going, you should think of types as more like spaces.

Second, for any type $X$ there’s a identity type $id_X$. You can think of this as the space of paths in $X$. Given terms $x,y$ of type $X$, there is a type $id_X(x,y)$. You can think of this as the space of paths from $x$ to $y$.

Alternatively, you can think of $id_X(x,y)$ as the space of proofs that $x$ and $y$ are equal. This takes a while to get used to, but in homotopy type theory proofs are ‘first-class’ mathematical objects, not merely something up in the metalanguage.

All this is before univalence comes along.

Posted by: John Baez on November 10, 2013 4:51 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John,

Remember: even before the univalence axiom comes along, equality already means something very different in homotopy type theory than it did in set theory.

But why should the concept of identity,

$x = y$

have anything to do with sets? Why is it not simply a primitive notion applicable to whatever $x$ and $y$ are? So, $x$ and $y$ can be spaces, or apples, or infinite cardinals, or anything one likes. One can introduce other equivalence relations or indiscernibility relations, if one likes.

For example, if one has a relational model $\mathcal{M} = (A, R_1, \dots)$, then one might wonder if $=$ is definable in $\mathcal{M}$, and then prove various results about this.

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 6:04 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

An updated version of the SIU paper is now available here:

http://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf

it corrects a few typos, expands on a few points, and adds a few references.

Posted by: Steve Awodey on November 14, 2013 5:26 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

[See edit below]

Jeff,

Maybe we’re interpreting Hilbert’s 6th problem differently. Actually I think this came up before.

I take it that Hilbert formulating GTR in terms of an action and variation principles in 1915 is paradigmatic work answering his own problem, not Hilbert when working with Ackermann. And Leo Corry is with me on this, e.g., in his ICM talk. There he warns of confusing Hilbert the formalist with Hilbert the axiomatiser.

As he worked on the different branches of physics, and he taught at least one every semester over very many years, he was trying to do just what he did for algebraic number theory and the theory of integral equations, that is, sort out the best conceptual organisation of the field.

EDIT; sorry, looking back I misrembered what you said about Ackermann. your point was that foundational work in physics wasn’t just about formalisation. But I still feel there’s a difference between us that I’m trying to put a finger on. For me quintessential 6th problem work today is sorting out how to organise QFT well, e.g., the contributions to this book.

Posted by: David Corfield on November 10, 2013 2:23 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David, right - the idea of Hilbert being a “formalist” is sometimes played up in a way that isn’t quite accurate. The 1899-1900 Hilbert-Frege correspondence focuses on their differing views of the role of an axiom system. For Frege, the axioms (e.g., of arithmetic) are to embody foundational truths, perhaps perceived a priori (“logically” a priori for Frege; “intuitively” a priori for Hilbert later). For Hilbert (1899), the axioms are “implicit definitions”. Later, Hilbert developed his finitistic position (partly in response to Brouwer et al.), as he wanted to clarify what is meant by definite “contentual” mathematics, as opposed to “ideal mathematics” (e.g., infinite sets): for Hilbert, this “contentual mathematics” consists in knowledge of finite mathematical objects and computations on them, and this is usually taken to be PRA (Tait) (but I think PA for Kreisel). The theory of hereditarily finite sets turns out to be all-but-equivalent to PA; as does the theory of concatenation of strings.

However, the consistency problem seems to be a contentual question: “is there a derivation of $0=1$ from $PRA$?”. Godel 1931 showed that, if $PRA$ is consistent, then $PRA$ is not strong enough to answer this question… So, contentual mathematics must go beyond PRA. This then leads one up a ladder of increasing consistency strength.

I think of Hilbert 6th problem as asking for an axiomatic presentation of the basic principles of physics, just as one gives an axiomatic presentation of number theory in $PA$, or set theory in $ZF$, or geometry in Hilbert’s 1899 version (or Tarski’s 1959 first-order version). Reichenbach and Carnap were both interested in these problems. But it turns out to be very tough. For example, one wants to be clear about what physical quantities are. There is a literature on this, largely coming from work in the theory of fundamental measurement. The classic being the 1971 Krantz et al. volume Foundations of Measurement.

Field 1980 (Science Without Numbers) and a number of papers by Burgess (as well as the longer monograph, Burgess & Rosen 1997, A Subject with No Object), use and develop this material. But, sadly, it’s hard to get other people interested in this kind of topic. Occasionally I see bits and pieces on this kind of thing. E.g., the papers on relativity theory (from Budapest) that I linked to earlier. This 2008 posting “What is a Gauge?” by Terry Tao contains some very neat insights.

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 6:57 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

Mathematicians and theoretical physicists interested in foundations need to study the works of Quine, Kripke, Putnam, Benacerraf, Field, Shapiro, Burgess et al, in order to make progress with their problems.

David wrote:

Gosh! There is a clash of intuitions.

I think both of you are right: mathematicians and theoretical physicists interested in foundations need to understand how analytic philosophy deals with foundations, but also take on board ideas from category theory, especially topos theory, homotopical algebra and higher category theory: roughly, the lines of thought coming from the work of Lawvere, Quillen and Grothendieck.

In college I read Quine, and took a course from Kripke—though that was more about mathematical logic than philosophy. My senior thesis advisor was Burgess. So I think I imbibed that worldview reasonably well, at least for a mathematician.

But later I lost interest in logic and foundations: quantum field theory, general relativity, and the project of combining them were just too much more interesting.

However, my attempts to understand quantum gravity eventually led me to higher categories, largely thanks to some papers by Louis Crane. I started talking about 2-categories on the internet, and that’s how I met James Dolan. Then I discovered categorical logic, largely thanks to conversations with him.

This made all the old questions in analytic philosophy vibrant and new, by suggesting radically different approaches that investigate notions like ‘sameness’ just as rigorously but more deeply—and in a way more in line with how mathematics is actually done.

I’m so happy that homotopy type theory has become a hot topic and is luring more people to learn about topos theory, homotopical algebra and higher category theory. It would be nice if some experts in analytic philosophy decided to extend their empire to include these ways of thinking. That’s where the real potential for growth lies. It would offer such immense room for really new thoughts.

Posted by: John Baez on November 9, 2013 5:46 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John, your honors thesis teacher John Burgess just finished a book, Rigor and Structure, on pretty much all of this (well, there’s no quantum gravity), about mathematical practice and discussing category-theoretic foundations too. He’s on the set theory side, of course, of the Set/Cat War. :)

My colleagues Øystein Linnebo and Richard Pettigrew just published something “Category Theory as an Autonomous Foundation” you might like to read too (it appeared in Philosophia Mathematica, 2011).

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 2:09 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Perhaps rather than “inadequate” it would be better to say “inconvenient”. I think it’s still true, as far as we know, that all mathematics can be interpreted into set theory (although some of the boundaries of HoTT might push that close to debate). But there are some problems with making practical use of this interpretation, such as:

• The distance between the foundational set theory and some parts of mathematics built on it is large. In other words, the translation is a lot of work. This is a problem when trying to formalize math in a computer, which has to be taught every detail of the translation into whatever foundational system you use.

• Set theory is not natively computational, which makes it less convenient to use for formalizing correctness proofs of computer programs, and other related things.

• The translation into set theory introduces new meaningless or undesirable statements and truths. Benacerraf’s complaints fall under this heading, but more recently and relevantly, we have the issue that in category theory we avoid distinguishing between isomorphic objects, whereas when we translate into set theory, it always becomes possible to distinguish between them in some way.

• The construction of new models of mathematics from old ones is more artificial in set theory. For instance, new toposes arise naturally from old ones by constructions of sheaves and realizability, and we can interpret all of mathematics in any topos. But if this interpretation is to go by way of set theory, then we have to go through a laborious process of constructing a model of set theory with its intricate $\in$-structure out of the objects of any topos — only to mostly discard that structure when we start interpreting the rest of mathematics! Type theory (and “structural” or “categorical” set theory) avoid this detour.

• Not all models of mathematics can be regarded as models of set theory. Higher toposes do contain models of set theory, but not all objects therein can be built out of the resulting sets. It’s still true that the higher topos itself can be built out of the sets in the ground model, so that ultimately everything can be reduced to set theory, but restricting ourselves to set theory as the foundation prevents us from working inside the higher topos as a world of mathematics in its own right.

Posted by: Mike Shulman on November 6, 2013 8:11 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, thanks. Yes, I agree with all of that.

The whole Set/Cat debate is something I find a bit too boisterous :)

On how the set theorist deals with the Benacerraf problem, for example, take ordered pairs. In set theory, one says:

“Suppose we have $x,y$ and we consider the ordered pair $(x,y)$. This isn’t the same as $\{x,y\}$. We need something that satisfies the ordered-pair abstraction principle,

(OP) $(x,y) = (a,b)$ if and only if $x = a$ and $y = b$.

Now consider the set $\{\{x\},\{x,y\}\}$. It turns out that,

$\{\{x\},\{x,y\}\} = \{\{a\},\{a,b\}\}$ if and only if $x = a$ and $y = b$.

So, we can represent, or “implement”, $(x,y)$ as $\{\{x\},\{x,y\}\}$. In fact, this choice is not unique: there are countless implementations. But it doesn’t matter which implementation we select, so long as it satisfies (OP).”

I think the main background suggestion (of many working on the HoTT project - Steve and yourself and others) is that HoTT will provide a new, maybe in some sense better, foundation for mathematics, which brings together type theory, category theory and constructive/computational mathematics. Some of the announcements related to the monograph were in this kind of vein.

The gap from the first appearance of axiomatic set theory (Zermelo 1908) to common-practice in mathematics departments, in core mathematics, and part of the standard undergraduate presentation of foundations (let’s say mid 1940s), was about 40 years.

Is the expectation that, by 2050, say, mathematics departments will standardly be presenting HoTT as its basic foundation to its first-year undergrads?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 7, 2013 6:54 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Is the expectation that, by 2050, say, mathematics departments will standardly be presenting HoTT as its basic foundation to its first-year undergrads?

I wouldn’t personally call it an expectation. I think it’s a possibility. It might happen but take longer than that. In any case I wouldn’t expect it to be exactly the HoTT we use nowadays that undergrads would be learning in 2050; there are plenty of things that I hope we’ll figure out how to improve by then.

Another possibility is that rather than becoming the new orthodoxy itself, HoTT leads us to a more “relativist” or “pluralist” situation, as advocated by Andrej here. Or, I suppose, the set-theoretic monopoly might win out in the end, although I hope not.

Posted by: Mike Shulman on November 7, 2013 5:36 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote to Mike:

Is the expectation that, by 2050, say, mathematics departments will standardly be presenting HoTT as its basic foundation to its first-year undergrads?

It’s worth noting that most math departments currently don’t present any basic foundation to their first-year undergrads. They launch into calculus, multivariable calculus, differential equations, linear algebra, etcetera without any foundation.

Later, math majors often take a course on set theory, but it’s usually informal. And when they take advanced calculus, they usually learn some axioms for the real numbers… but the infrastructure underlying these axioms (e.g., set theory) is usually taken for granted.

In places I’ve been, only students especially interested in foundations learn the ZFC axioms. Even most math grad students never see these axioms.

And that’s probably fine! Since I’m interested in foundations it makes me a bit sad—but there’s a lot for mathematicians to learn, and the axioms of set theory, or homotopy type theory, are not what they most need to know. They just pick up enough rigor to satisfy their teachers when they write proofs.

And that won’t change by 2050.

Posted by: John Baez on November 9, 2013 6:09 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

It makes me a bit sad not just because I’m interested in foundations, but because a lot of mathematicians grow up with a fear of set theory, a vague feeling that when you do certain sorts of things you have to worry about it, and therefore an aversion to doing those sorts of things.

Posted by: Mike Shulman on November 10, 2013 4:33 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, here’s some cheerful philosophical reading by Putnam,

Hilary Putnam 1994; “Philosophy of Mathematics: Why Nothing Works

The sections where Putnam discusses formalism and intutionism seem somewhat relevant to what we were discussing earlier (i.e., applied mathematics within physics).

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 9:46 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

“I don’t see how that can possibly be true. One of the important features of the world is that we can distinguish between distinct spacetime points, e.g. we can say that a certain event happened here and not there. But it doesn’t make sense to speak of, e.g., the points of an isomorphism class of differentiable manifolds. An individual manifold has points, but an isomorphism class of them doesn’t, because any manifold has automorphisms that interchange some of its points.”

Although I ‘understand’ this I find it hard to stomach. Points seem (at least in the usual definition of manifolds) to be essential to defining manifolds it seems rather incredible that one can just magic them away by considering an isomorphism class. Plus points seem on the face of it useful pieces of fiction to obtain local properties.

Does this mean we need to find a different idea of a point suitable for an isomorphism class? Perhaps rather than consider the isomorphism class (which omits the specifics of which morphism makes two manifolds isomorphic) we consider it as a groupoid of manifolds and consider a generalised point to be a point on each manifold together with the morphism that identifies them. This does sound reminiscent of some kind of categorical construction, but I’m probably way off here.

Posted by: Mozibur Ullah on November 7, 2013 5:31 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Does this mean we need to find a different idea of a point suitable for an isomorphism class?

I think it means that isomorphism classes are the wrong thing to use. As you said: we need to consider the groupoid of manifolds instead.

Posted by: Mike Shulman on November 7, 2013 6:03 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Is this then OK, or unnecessarily elaborate?

Think of a fibre above a manifold $M$, comprised of $\langle M, x \rangle$ for all points $x$ in $M$. A point is a section of the full bundle above the groupoid of manifolds isomorphic to $M$.

Alternatively, form the type, $Mfd(M)$ of manifolds diffeomorphic to $M$. There is a dependent type

$m : Mfd(M) \vdash P(m): Type,$

of points for each manifold. An invariant point is a term of the dependent product

$p: \product_{m: Mfd(M)} P(m).$

Posted by: David Corfield on November 8, 2013 1:09 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

We’re considering spacetime models

$\mathcal{M} = (M, g, T, \dots)$,

with $M$ a differentiable manifold, and the fields $g,T$ satisfying Einstein’s equations. Suppose $Iso(\mathcal{M})$ is the groupoid of spacetime models isomorphic to a given one.

David and Mike, I suspect one will probably be able to run a “hole argument” against any such attempt to “abstract” away from the particular carrier sets of each $\mathcal{M}$ in the groupoid. Earman (1989), for example, tried to replace $Iso(\mathcal{M})$ with an “Einstein algebra”, using ideas from Geroch. But Rynasiewizc (1992) pointed out that the same problem that arose for the original manifolds approach arises for the Einstein algebra approach. See Norton (2011), “The Hole Argument”, for a summary of all this.

I think one has to do something very different. I don’t think it’s a mathematical problem. It’s a conceptual one: about what “represents” and “world” mean.

For a fixed model/structured set $\mathcal{A}$, one can define its “abstract structure” $\hat{\Phi}_{\mathcal{A}}$ to be a certain categorical propositional function, using infinitary logic. This implements the abstraction principle,

$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A} \cong \mathcal{B}$.

Saturating any such abstract structure with some primitive relations, $R_1, \dots$, yields a (categorical) proposition, $\hat{\Phi}_{\mathcal{A}}[R_1, \dots]$.

If one now defines a (physical) world $w$ to be $\hat{\Phi}_{\mathcal{M}}(R_1, \dots)$, for some physical relations $R_1, \dots$, then one can show that,

If $\mathcal{M}_1$ represents $w_1$ with respect to $\vec{R}$ and $\mathcal{M}_2$ represents $w_2$ with respect to $\vec{R}$, and $\mathcal{M}_2 \cong \mathcal{M}_2$, then $w_1 = w_2$.

So, when we fix the “interpretation” of the models (via the physical relations $R_1, \dots$), isomorphic spacetime models do indeed represent the same world. And that’s (LE) as usually formulated.

Jeff

Posted by: Jeffrey Ketland on November 8, 2013 6:00 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

So there’s a task for me to do: relate the nLab entries on the Hole Argument and general covariance to what’s happening in the philosophical literature.

Posted by: David Corfield on November 9, 2013 7:49 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Well, if we’re not thinking about an isomorphism class but about an actual manifold $M$ (as an object of the groupoid of manifolds), then we can just talk about the points of $M$!

Posted by: Mike Shulman on November 9, 2013 3:43 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

For a fixed model/structured set $\mathcal{A}$, one can define its “abstract structure” $\hat{\Phi}_{\mathcal{A}}$ to be a certain categorical propositional function, using infinitary logic. This implements the abstraction principle,

$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A} \cong \mathcal{B}$.

But why does Nature do something so weird? Someone can tell me all about fibres, sections, vertical automorphisms, etc., etc.; but it doesn’t answer the question: why are $A$ and $A'$ representations of the same physical state? Why are isomorphic copies $(M,g)$ and $(N,h)$ representations of the same physical world?

Here’s my answer: it’s not Nature that’s doing it. It’s you! You’re building this into your mathematical setup! In your ‘abstraction principle’ you are decategorifying: brutally turning isomorphisms into equations. You had a groupoid, but you crushed it down into a set.

It’s a bit like stepping on a flower, and then wondering why Nature made it so flat.

(The univalence axiom in homotopy type theory also turns isomorphisms into equations, but in a non-brutal way, because it uses a more subtle kind of logic: it doesn’t crush groupoids (or more general homotopy types) down into sets.)

Posted by: John Baez on November 9, 2013 4:16 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I hadn’t realised until know how much Urs has done putting covariance into shape. Impressive stuff! We get to see the configuration space in its rightful groupoidal shape:

$[\Sigma, \mathbf{Fields}]//\mathbf{Aut}(\Sigma),$

and its HoTT rendition.

Posted by: David Corfield on November 10, 2013 12:06 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks, David (and Urs)

$[\Sigma,Fields]//Aut(\Sigma)$

Perhaps - in the paper “A Note on Leibniz Equivalence” I mentioned earlier, I argued that it should be $Sym(\Sigma)$, rather than $Aut(\Sigma)$. That is, the permutation group of the carrier set of $\Sigma$.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 1:44 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

But (as pointed out on that page) for the physics to work we need the smooth structure in place. You’re not going to be able to reimpose it after the quotienting process of forming the action groupoid.

Posted by: David Corfield on November 10, 2013 9:25 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

But (as pointed out on that page) for the physics to work we need the smooth structure in place.

Suppose $\Sigma = (A,C)$, where $A$ is the carrier set and $C$ is the smooth structure (maximal atlas on $A$). Any permutation $\pi : A \to A$ maps a chart $(U,\phi)$ in $C$ to $(\pi[U],\phi \circ \pi^{-1})$. Let $\pi_{\ast}C$ be the resulting system of charts. Then:

$(A,\pi_{\ast}C) \cong (A,C)$

So, the smooth structure “stays in place”, up to isomorphism, because under any permutation $\pi \in Sym(A)$, the image $(A,\pi_{\ast}C)$ (the result of pushing forward the smooth structure) is an isomorphic copy of $(A,C)$, by construction. In other words, the orbit of $\Sigma$ under the action of any permutation of the carrier set is the groupoid of all manifolds isomorphic to $\Sigma$, on the same fixed carrier set $A$.

Do you think there is a physical objection to this? I have asked quite a few of my colleagues, in both physics and philosophy of physics, and some say “Yes” and some say “No”.

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 1:36 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Is this even mathematically correct?

For an $n$-dimensional manifold, normally we need a topological space (Hausdorff) equipped with an atlas of charts, i.e., homeomorphisms from open subsets of $\mathbb{R}^n$ patched together to form a cover.

Is your topology included in your $C$ somehow?

Posted by: David Corfield on November 10, 2013 3:05 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Yes, the atlas $C = \{(U_{\alpha},\phi_{\alpha})\}_{\alpha}$, and the charts cover $A$, and their transition maps $\phi_{\alpha \beta}$ are diffeomorphisms between open sets in $\mathbb{R}^n$. Then, the topology $\mathcal{T}$ on $A$ is determined by the atlas $C$ as follows:

$\mathcal{T} := \{O \subseteq A \mid \phi_{\alpha}[O \cap U_{\alpha}]$ is open (in $\mathbb{R}^n$), for all charts $(U_\alpha,\phi_{\alpha}) \in C\}$

Then $(A,\mathcal{T})$ is a topological space such that each chart $(U_{\alpha},\phi_{\alpha})$ is a local homeomorphism to an open set $\phi_{\alpha}[U_{\alpha}] \subseteq \mathbb{R}^n$.

The definitions used here (i.e., how we define the topology $\mathcal{T}$ from the atlas) are from Robbin & Salamon’s notes “Introduction to Differential Geometry” (pp. 59-61). Frankel’s textbook, The Geometry of Physics (pp. 19-20) is similar. (But note that Robbin & Salamon don’t require $(A,\mathcal{T})$ to be Hausdorff or second-countable in their definition of “manifold”.)

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 3:52 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

You can transport the smooth structure along a bijection $A\cong A$, but then you’ll get a different manifold, not the one $\Sigma$ you started with. So $Sym(A)$ doesn’t act on $[\Sigma,Fields]$ and you can’t quotient by it. So it would not be mathematically correct to write $[\Sigma,Fields]// Sym(A)$. By contrast, a diffeomorphism $\Sigma\cong\Sigma$ respects the (same) given smooth structure on both sides, so it does act on $[\Sigma,Fields]$ and you can write $[\Sigma,Fields]// Aut(\Sigma)$.

It is also possible to consider a groupoid of manifolds diffeomorphic to $\Sigma$ and all diffeomorphisms between them. If you like, you could restrict to those that have the same carrier set, but mathematically that is an irrelevant distraction. Then you would have a functor $[-,Fields]$ defined on this groupoid, and you could consider its colimit, and that would yield an equivalent result. But it still shouldn’t be written as $[\Sigma,Fields]// Sym(A)$, because $Sym(A)$ is not the name of that groupoid.

Posted by: Mike Shulman on November 11, 2013 12:41 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

You can transport the smooth structure along a bijection $A \cong A$, but then you’ll get a different manifold, not the one $\Sigma$ you started with.

It’s extensionally different, yes. But it’s still an isomorphic copy of $\Sigma$. If the carrier set of $\Sigma$ is $A$, and we have a bijection $\pi : A \to A$, then the result is the pushforward of the smooth structure under $\pi$, and I call it $\pi_{\ast}\Sigma$.

(We have $\pi \in Aut(\Sigma)$ just if $\pi_{\ast}\Sigma = \Sigma$.)

Then, if $\mathcal{M} = (\Sigma, g, T, \psi, \dots)$ is a spacetime model of some kind, with carrier set $A$, then we can apply any $\pi \in Sym(A)$ as above, getting $\pi_{\ast}\mathcal{M} = (\pi_{\ast}\Sigma, \pi_{\ast}g, \pi_{\ast}T, \pi_{\ast}\psi, \dots)$ and the result $\pi_{\ast}\mathcal{M}$ is an isomorphic copy of the original model $\mathcal{M}$.

Then (LE) says that $\pi_{\ast}\mathcal{M}$ and $\mathcal{M}$ are physically equivalent. And so, really one should quotient by $Sym(A)$, not $Aut(\Sigma)$.

(I realise this is a rather dramatic conclusion!)

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 2:41 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I just explained why it is mathematically meaningless to quotient by $Sym(A)$. Passage across the diffeomorphism from $\Sigma$ to $\pi_*\Sigma$ is not quotienting by $Sym(A)$, it is considering the groupoid of manifolds as I described.

Posted by: Mike Shulman on November 11, 2013 6:34 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Ok, yes – but suppose we define $Mn(A)$ to be the groupoid of all manifolds on a fixed carrier set $A$ of points (and morphisms all diffeomorphisms). Objects in $Mn(A)$ have the form $(A,C)$, with $C$ a maximal atlas, and they count as identical when they have the same $C$ (even though distinct $(A,C_1)$ and $(A,C_2)$ can be diffeomorphic).

Then $Mn(A)/Sym(A)$ is meaningful, right?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 4:59 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Yes, it is meaningful — but it’s not what you want. A permutation $\pi$ of $A$ acts on $Mn(A)$ by sending each manifold $(A,\Sigma)$ to the manifold $(A,\pi_\ast \Sigma)$, so you can quotient by this action. However, since $\pi$ also supplies a diffeomorphism $(A,\Sigma) \cong (A,\pi_\ast \Sigma)$, the action of $\pi$ on $Mn(A)$ is naturally isomorphic to the identity functor, and so the action of $Sym(A)$ is (naturally isomorphic to) the trivial action. Therefore, its (homotopy) quotient is just the cartesian product $Mn(A) \times \Sym(A)$.

Posted by: Mike Shulman on November 11, 2013 9:55 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Stripping this down to a simpler case of topological spaces over sets, we can have the Sierpinski topology, $T$, on $\{0, 1\}$, with open sets $\empty$, $\{0\}$ and $\{0, 1\}$. The set mapping which permutes $0$ and $1$ gives rise to a homeomorphism of topological spaces, but it’s between $T$ and another topological space $T^{\ast}$ with the same underlying set and open sets $\empty$, $\{1\}$ and $\{0, 1\}$.

Were I to take a configuration space of continuous functions out of $T$, I can’t then quotient by the symmetries of the underlying set of $T$, since it sends a continuous function on $T$ to one on $T^{\ast}$.

If I want that permutation feature in an action on something above, I can form the groupoid, $G$, with objects $T$ and $T^{\ast}$ and homeomorphisms between them, but then the quotient I carry out will be denoted in terms of $G$ rather than $Sym (\{0, 1\})$.

Posted by: David Corfield on November 11, 2013 1:57 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

So suppose $A = \{0,1\}$ and we have topologies $T_1 = \{\varnothing, \{0\}, \{0,1\}\}$ and $T_2 = \{\varnothing, \{1\}, \{0,1\}\}$, which are homeomorphic under the transposition $\pi$ that swaps $0,1$. Suppose

$\mathcal{M}_1 = (A, T_1, f_1)$,

is my “spacetime model”, where

$f_1: A \to \mathbb{R}$

represents my “physical field”, say. Let $f_2 : = f_1 \circ \pi^{-1}$. So, $f_2(0) = f_1(\pi^{-1}(0)) = f_1(1)$, and $f_2(1) = f_1(0)$. Then let the new model be

$\mathcal{M}_2 = (A, T_2, f_2)$.

So, $\mathcal{M}_2 = \pi_{\ast}\mathcal{M}_1$. I.e., $\mathcal{M}_2 \cong \mathcal{M}_1$. So, $\mathcal{M}_1$ and $\mathcal{M}_2$ are “gauge equivalent”, and, assuming a more general version of (LE), are physically equivalent, because Nature doesn’t care what $0$ and $1$ “really are” (or “really correspond to”), so long as there are two of them.

Keeping the carrier set $A$ fixed, the orbit of gauge equivalent models is given by the action of each $\pi \in Sym(A)$.

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 5:31 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

And here’s exactly the point: Nature does care about distinguishing between 0 and 1, because one of them has to be “here” and one of them has to be “there”. If you swap 0 and 1 in the mathematical model, then you have to also swap the points in Nature, because (in our strange little world) Nature can tell the difference between an open point and a closed point. That’s why isomorphisms of models have to correspond to isomorphisms of worlds.

Posted by: Mike Shulman on November 11, 2013 9:58 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Just to be clear, Mike’s talking about active transformations (strangely we don’t seem to have anything on this on the nLab). If I think I’m in $\mathcal{M}_1$, then you say we’re in $\mathcal{M}_2$, it might just be because our labelling differs. Once we’ve sorted that out, we can agree about the model.

On the other hand, if a divine agency intervenes to make $\{1\}$ rather than $\{0\}$ an open set according to my labelling, I’ll notice the world has changed.

Posted by: David Corfield on November 11, 2013 10:39 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike and David, yes, sure – this is all about active mappings, considering genuine maps that move the points around in the carrier set of the model $\mathcal{M} = (A, \dots)$ used to represent worlds, and “pushingforward” the corresponding fields/structure around accordingly.

I say (on my Leibnizian, relationist view) that Nature can’t tell the difference: isomorphic worlds are literally the same; so, $0$ and $1$ here, in the carrier set of David’s 2-element topological spacetime model $\mathcal{M} = (A, T, f)$, are just gauge-dependent pegs or labels. What matters is the “global relational structure” of the model $\mathcal{M}$ of the (a) world.

But this is certainly the interpretative issue behind the Leibniz equivalence debate, and the relationist conclusions are rather dramatic!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 12, 2013 12:26 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John,

You had a groupoid, but you crushed it down into a set.

But I think that’s not what happens here. In a sense, almost the opposite happens! The abstract (“relational”) structure of the isomorphic models in the groupoid is preserved, encoded in the corresponding formulas $\Phi_{\mathcal{A}}(\vec{X})$. What has been “abstracted away” are simply the specific carrier sets. This is a kind of “structuralism”, which eliminates the elements of the carrier sets, leaving behind only the structure they all share.

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 4:09 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A} \cong \mathcal{B}$.

John wrote:

You had a groupoid, but you crushed it down into a set.

Jeffrey wrote:

But I think that’s not what happens here.

Yes, it is. You had a bunch of entities of type $\mathcal{A}, \mathcal{B}, \dots$ and isomorphisms between them. These form a groupoid. Then you define new entities $\hat{\Phi}_{\mathcal{A}}, \hat{\Phi}_{\mathcal{B}}, \dots$ and decree that

$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A} \cong \mathcal{B}$

So, these new entities are isomorphism classes of the old ones. When you do this to a groupoid, or category, it’s called decategorification, and the result is a mere set.

You were acting puzzled that isomorphic models describe equal universes. I claim the reason is that you’re treating universes as forming a set (or class) rather than a groupoid, or homotopy type. When people get used to homotopy type theory, they’ll stop doing this, and the puzzle will evaporate. Isomorphic models will describe isomorphic universes, and everything will make sense.

Posted by: John Baez on November 10, 2013 5:07 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John,

I think maybe you took it that the entity $\Phi_{\mathcal{A}}(\vec{X})$ that I mentioned above is a set or an equivalence class? No, these entities are formulas of infinitary logic: omitting the reference to the sequence $\vec{X}$ of free second-order variables, $\Phi_{\mathcal{A}}$ is a kind of linguistic diagram of $\mathcal{A}$, analogous to the notion of a diagram in model theory. Its most important property is its categoricity:

$\mathcal{B} \models \Phi_{\mathcal{A}}$ iff $\mathcal{B} \cong \mathcal{A}$.

So, yes, moving to an equivalence class is “decategorification”, just as in the example of moving from FinSet to $\mathbb{N}$.

But this isn’t decategorification. For example, the formula $\Phi_{\mathcal{A}}$ (omitting the reference to the free variables) can be “skolemized”, written $sk_{\alpha}\Phi_{\mathcal{A}}$, where the map $\alpha$ replaces each bound variable in the formula by some new constant. Any pair of skolemizations $\alpha, \beta$ corresponds to a permutation $\pi: A \to A$ of the carrier set of $\mathcal{A}$. Then one can show that:

$\pi \in Aut(\mathcal{A})$ iff $sk_{\alpha}\Phi_{\mathcal{A}} \equiv sk_{\beta}\Phi_{\mathcal{A}}$.

This shows how automorphisms of $\mathcal{A}$ correspond to logical equivalence, under linguistic relabellings of the formulas that describe $\mathcal{A}$.

The formula $\Phi_{\mathcal{A}}$ isn’t an equivalence class; it’s a formula which encodes all the structural information about $\mathcal{A}$, but throws away its carrier set. This idea isn’t decategorification; it’s decarriersetification!

The propositional content of the formula $\Phi_{\mathcal{A}}$ is called $\hat{\Phi}_{\mathcal{A}}$; and then, with some mild assumptions about propositional content, one can prove, rather than decree, that

$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A} \cong \mathcal{B}$.

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 5:47 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I don’t quite understand what $\Phi_{\mathcal{A}}$ is, but I think the set which is doing the decategorification is the set of which $\widehat{\Phi}_{\mathcal{A}}$ and $\widehat{\Phi}_{\mathcal{B}}$ are elements. Essentially by definition, the isomorphism class of a thing $A$ is a thing $[A]$ with the property that $[A]=[B]$ iff $A\cong B$. Thus, the proof that $\widehat{\Phi}_{\mathcal{A}} = \widehat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A}\cong \mathcal{B}$ is a proof that $\widehat{\Phi}_{\mathcal{A}}$ is, essentially, the isomorphism class of $\mathcal{A}$.

Posted by: Mike Shulman on November 11, 2013 12:42 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, for a given structured set (model) $\mathcal{A}$, then $\Phi_{\mathcal{A}}$ is a formula which defines $\mathcal{A}$ up to isomorphism.

For a simple example, consider the graph $G = (V,E)$ with $V = \{0,1,2\}$ and $E = \{(1,2),(2,1)\}$. The “diagram formula” $\Phi_G(X,Y)$ for $G$ is this complicated mess:

$\exists x_0 \exists x_1 \exists x_2[x_0 \neq x_1 \wedge x_0 \neq x_2 \wedge x_1 \neq x_2 \wedge X(x_0) \wedge X(x_1) \wedge X(x_2) \wedge$

$\neg Y(x_0,x_0) \wedge \neg Y(x_0,x_1) \wedge \neg Y(x_0,x_2) \wedge \neg Y(x_1,x_1) \wedge \neg Y(x_1,x_0) \wedge Y(x_1,x_2) \wedge$

$\neg Y(x_2,x_0) \wedge Y(x_2,x_1) \wedge \neg Y(x_2,x_2) \wedge \forall z(X(z) \to (z = x_0 \vee z = x_1 \vee z = x_2))]$

(Here, $X,Y$ are free second-order variables.) The crucial property is categoricity. If $G^{\ast} = (V^{\ast}, E^{\ast})$ is some model, then

$G^{\ast} \models \Phi_{G}(X,Y)$ iff $G^{\ast} \cong G$.

If you look at the subformulas of $\Phi_G(X,Y)$, you see that there is a sequence of inequations of variables (corresponding to the distinct elements in $V$), and there are “literals” describing how the elements are related, and there is a formula saying that everything in $X$ is one of these elements.

There’s nothing particularly deep about this; it’s well-known to model theorists, and is, more or less, the diagram of the model $G$, except that it has been turned into a single formula and the constants have been existentially quantified.

One can then read the formula $\Phi_G(X,Y)$ as saying:

There are exactly three things in $X$ such that the first is not $Y$-related to anything, and the second and third are $Y$-related to each other, but not to anything else.

The propositional content of this I call $\hat{\Phi}_G$. Because of categoricity, if $G$ and $G^{\ast}$ are isomorphic models, they will give rise the same propositional diagram, i.e., $\hat{\Phi}_G = \hat{\Phi}_{G^{\ast}}$.

All of the “structural content” of the original graph $G = (V,E)$ is encoded into the diagram formula $\Phi_G(X,Y)$, but there is no longer a special carrier set.

This construction can be extended to arbitrary models (i.e., structured sets), using infinitary logic. For each $\mathcal{A}$, one gets its “abstract structure” $\hat{\Phi}_{\mathcal{A}}$, and this implements

$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A} \cong \mathcal{B}$.

which is one of the principles that Steve discusses in his “Univalence, …” paper. I think Steve writes it as,

$Str(A) = Str(B)$ iff $A \cong B$.

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 2:14 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks, but I wasn’t asking what $\Phi_{\mathcal{A}}$ is — I was trying to explain that that whatever it is, what you’re doing with it is decategorifying.

Posted by: Mike Shulman on November 11, 2013 6:30 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Yes, my bad. You and John are right – on the definition, that’s what I’m doing in constructing this $\Phi_{\mathcal{A}}$-thing for each $\mathcal{A}$. But I’m not constructing it by taking an equivalence class: rather it’s more like a logical picture of $\mathcal{A}$, but with the carrier set dumped.

Cheers.

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 4:43 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John,

Isomorphic models will describe isomorphic universes, and everything will make sense.

This sort of view was defended about 20 years ago (e.g., Maudlin 1990 and Butterfield 1989).

But I think it’s fair to say that no one defends it anymore. Your distinct-but-isomorphic-universes would be physically indistinguishable (like Leibniz’s original “shifted worlds”, in Leibniz’s argument against Newton’s absolute space), but the physical principle involved suggests that there cannot be such distinct, isomorphic universes. The isomorphic models are representations of the same universe!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 10:25 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Well, evidently whoever decided not to defend it any more messed up, and should reconsider. (-: What is this “relevant physical principle”?

Posted by: Mike Shulman on November 11, 2013 12:48 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, it’s usually called “Leibniz equivalence” (and sometimes “Diffeomorphism invariance”) and it’s discussed in John Norton’s article here,

Norton 2011: “The Hole Argument”.

But what the exact formulation should be is of course a matter of dispute!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 1:29 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

In an earlier comment you called “Leibniz equivalence” precisely the claim that isomorphic models describe the same world. Invoking that claim as a reason not to defend John’s proposal is pretty circular! Unless I misunderstood you and you weren’t trying to give a reason. But there has to be a reason, right? Or have all philosophers just decided to accept the principle that “isomorphic models describe the same world” for no particular reason?

Posted by: Mike Shulman on November 11, 2013 6:32 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, suppose we have spacetime models $\mathcal{M}$ and $\mathcal{N}$, and associated with them, the physical worlds $w(\mathcal{M})$ and $w(\mathcal{N})$ they represent. Naively, one might think that the mapping is injective, so that distinct $\mathcal{M}, \mathcal{N}$ go to distinct worlds $w(\mathcal{M}), w(\mathcal{N})$. This is called “manifold substantivalism” (it corresponds roughly to Newton’s Absolute Space, as opposed to Leibniz’s “relationism”).

But the gauge equivalence principle in GR, stated in, e.g., Wald and Carroll that I quoted upthread, says that,

if $\mathcal{M} \cong \mathcal{N}$, then $w(\mathcal{M}) = w(\mathcal{N})$.

According to Norton (see below), it’s a “standard presumption in the modern mathematical physics literature”. The principle is from physics itself. It’s not really a “decision by philosophers”–it’s assertions by physicists! As for the argument against manifold substantivalism, there are, mainly, two, I think. The first is the original Leibnizian thought experiment that the physical indistinguishability of “isomorphic worlds” implies strict identity of those worlds. The second, which was set out in Earman and Norton 1987, is that manifold substantivalism leads to indeterminism, if the distinct mathematical representations are treated as physically distinct (and this kind of situation, the original “hole argument”, was what puzzled Einstein in 1913-1915). Still, here’s a recent summary by John Norton, in his “Hole Argument” article (2011):

The simplest challenge notes that Leibniz equivalence is a standard presumption in the modern mathematical physics literature and suggests that even entertaining its denial (as manifold substantivalists must) is some kind of mathematical blunder unworthy of serious attention. While acceptance of Leibniz equivalence is widespread in the physics literature, it is not a logical truth that can only be denied on pain of contradiction. That it embodies non-trivial assumptions whose import must be accepted with sober reflection is indicated by the early acceptance of the hole argument by David Hilbert. (See Section 8.2 above.) If denial of Leibniz equivalence is a blunder so egregious that no competent mathematician would make it, then our standards for competence have become unattainably high, for they must exclude David Hilbert in 1915 at the height of his powers.

Another challenge seeks principled reasons for denying general covariance. One approach tries to establish that a spacetime can be properly represented by at most one of two intertransformable systems of fields on some manifold. So Maudlin (1990) urges that each spacetime event carries its metrical properties essentially, that is, it would not be that very event if (after redistribution of the fields) we tried to assign different metrical properties to it. Butterfield (1989) portrays intertransformable systems as different possible worlds and uses counterpart theory to argue that at most one can represent an actual spacetime.

These responses are just a few of a large range of responses of increasing ingenuity and technical depth. In the course of the scrutiny of the argument, virtually all its aspects have been weighed and tested. Is the indeterminism of the hole argument merely an artifact of an ill-chosen definition of determinism? Is the problem merely a trivial variant of the philosophical puzzle of inscrutability of reference? Or are there deep matters of physics at issue? The debate continues over these and further issues. To enter it, the reader is directed to the bibliography below.

There have been some recent responses/discussions involving category-theory too. By Bain and Wuthrich, I think. But I’d have to look them up.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 3:17 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Hmm. Maybe John can chime in here, but I suspect the point is that if physicists say that, then they’re wrong too, for the reasons described above.

Posted by: Mike Shulman on November 11, 2013 9:43 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, here’s a quick version of the hole argument (slightly different from the way Norton describes it). Let

$(M,g, T)$

be a spacetime model and suppose it has a foliation $\{\Sigma_t\}_{t \in \mathbb{R}}$, where each $\Sigma_t$ is a spacelike hypersurface. Suppose we focus on $\Sigma_0$ as the $t=0$ hypersurface. Let

$\phi : M \to M$

be a diffeomorphism such that $\phi(p) = p$, for all $p$ lying in the past of $\Sigma_0$, but (smoothly) $\phi(p) \neq p$, for $p$ in the future. Consider the shifted model,

$(M,\phi_{\ast}g,\phi_{\ast}T)$

This model is distinct from, albeit isomorphic to, $(M,g, T)$.

On John’s proposal as I understand it–“isomorphic models represent isomorphic worlds”—the models $(M,g, T)$ and $(M,\phi_{\ast}g, \phi_{\ast}T)$ represent distinct (but isomorphic) physical solutions, which agree up to $t=0$, but then smoothly disagree afterwards.

But if this is possible, then this is physical indeterminism.

Eventually, after puzzling about this sort of problem for about two years, Einstein realised that this “indeterminism” is “pure gauge”, as it were, and came to adopt the view that $(M,g, T)$ and $(M,\phi_{\ast}g, \phi_{\ast}T)$ represent the same physical world (i.e., what Earman and Norton later dubbed “Leibniz equivalence”).

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 10:43 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

But once your models of reality are objects of a groupoid, rather than just elements of a set, the correct notion of “determinism” should be that the past determines the future up to isomorphism! Experience shows that in mathematics, no object of a category is ever determined more than up to (unique) isomorphism, and that this sort of determination is always sufficent. So we should expect the same to be true in physics.

Posted by: Mike Shulman on November 12, 2013 4:15 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, thanks - right, ok, now I am beginning to see what you (and John) have in mind. You interpret the non-uniqueness that Einstein noticed category-theoretically, and conclude that it doesn’t violate determinism—because while determinism as normally defined requires literal uniqueness, you can weaken this to uniqueness-up-to-isomorphism.

This, I guess, is analogous to the situation with structural set theory - where, e.g., one only has an empty-set-up-to-isomorphism, etc. (For me, and in ZF of course, there’s exactly one empty set, $\varnothing$; as extensionality is definitional of what it is to be a set!)

Maybe one can still argue that, even if one redefines “deterministic” to mean “deterministic-up-to-isomorphism”, there’s something (physically) unsatisfactory about having countlessly many isomorphic copies of physical worlds around, like a cloud of ghostly indistinguishable copies, none of them quite real–but I can see how it fits naturally with the category-theoretic view of mathematics you describe.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 12, 2013 5:31 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Is there a danger here of mixing up dynamics within a model which itself is an object in a groupoid, and dynamics within a configuration space which is a groupoid?

Where have the physicists gone when we need them?

I mean, the configuration space for GTR in a spacetime $\Sigma$ is the groupoid

$\mathbf{Riem}(\Sigma)//\mathbf{Diff}(\Sigma).$

I then define the Hilbert-Einstein action (let’s say the version coupled with matter), which as a map to the discrete groupoid on $\mathbb{R}$ must be constant on components. I then minimise (everything should be smooth) the action and this gives me physically possible universes. If one object is physically possible, then so is anything isomorphic to it.

There’s no dynamics within the configuration space, like the solution of a hanging chain out of all possible curves. However, once I select a specific object, then dynamics within that Riemannian manifold is fixed. There’s no indeterminism inside the manifold.

On the other hand, when working out the dynamics of QFT, I do this in a patch of spacetime. I’ll take an evolution mapping from the input state to the output state. If the state space is a groupoid, then evolution will be a functor.

Posted by: David Corfield on November 12, 2013 12:19 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

If one object is physically possible, then so is anything isomorphic to it.

Do you mean the physical world or the model of the physical world? Einstein eventually realised that the apparent differences were not physically real: i.e., one can’t have “distinct but isomorphic copies” of the physical world; and physicists in GR like Wald and Carroll put it by saying that the $\phi$-shifted model $(M, \phi_{\ast}g, \dots)$ represents the same world as $(M, g, \dots)$ does. The physical world should be unique; one shouldn’t have indistinguishable copies of it.

So, if category-theoretic physics is in conflict with Leibniz equivalence (which is a big if), it is committed to a kind of haecceitism–the existence of distinct indiscernible worlds. (There is a subtext here which I can’t quite put my finger on: perhaps it’s the idea of a global, type-free identity predicate “$x = y$”.)

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 12, 2013 6:41 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I think I need to go and have a hard think about the relationships between the physical world, its models and the mathematical structures appearing in them. I need to see how univalence plays out in applications.

Posted by: David Corfield on November 13, 2013 8:43 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

So, if category-theoretic physics is in conflict with Leibniz equivalence … it is committed to a kind of haecceitism—the existence of distinct indiscernible worlds.

I don’t agree. I would say instead that the structure of “modeling the real world” on a manifold entails some sort of correspondence between the points of the manifold and locations in reality. Then if we have an isomorphism between manifolds, we can transport such a “modeling reality” structure from one of them to the other one. But the real world doesn’t have to change.

I don’t know exactly what John had in mind when he spoke of “isomorphic worlds”, but I interpreted it as speaking of possible worlds, rather than asserting that there are actually more than one physical world. (It should be pointed out, though, that even if there is only one physical world, it can have nontrivial automorphisms and so we could still speak of “isomorphisms between worlds”.)

Posted by: Mike Shulman on November 14, 2013 4:52 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

Then if we have an isomorphism between manifolds, we can transport such a “modeling reality” structure from one of them to the other one. But the real world doesn’t have to change.

Right, so this treats the isomorphism

$\phi: M \to N$

as a passive change of representation of the possible (physical) world $w$. Let $PP_w$ be the set of physical points of $w$. The very natural underlying representation idea is that there is a (bijective) representation mapping

$\rho : M \to PP_w$,

so that a manifold point $x \in M$ represents some physical point $p = \rho(x)$ in the world $w$, and, this representation mapping preserves relations, so that when manifold points are related in a certain way (e.g., they lie on a mathematical geodesic), then their images will be too (e.g., they lie on a genuinely physical geodesic). This is essentially the idea adopted in representation theorems in the foundations of measurement, though one usually doesn’t demand a bijection: normally, it’s a homomorphism of the physical system to the mathematical representation, e.g., $(\mathbb{R}, <, +)$, and a measurement scale, like $mass_{kg}$ is a function analogous to $\rho^{-1}$.

But with this assumption about representation in hand, one can use the isomorphism $\phi$ to induce an “active change” of the world $w$ itself, giving an “isomorphic copy”. So, define

$\pi : = \rho \circ \phi \circ \rho^{-1}$.

I.e., $\pi : PP_w \to PP_w$ (which is a permutation of the physical points in $w$). So, e.g., if $R$ is some physical binary relation in $w$, then let

$\pi_{\ast}R = \{(\pi(p),\pi(q)) \mid (p,q) \in R\}$.

Doing this to all the physical relations $R, \dots$ in $w$ yields a bunch of new physical relations, $\pi_{\ast}R, \dots$, together isomorphic to the original! (And yet, usually, extensionally distinct: i.e., usually, $\pi_{\ast} R \neq R$.) So, we have a new world, call it $\pi_{\ast}w$, which is a distinct isomorphic copy of $w$.

But this violates Leibniz equivalence, which says that “if spacetime models are isomorphic, they represent the same world”. For example, if $\mathcal{M} = (M, g, T)$ is some spacetime model, and $S_{EH}(\mathcal{M})$ is the Einstein-Hilbert action for this model, then,

If $\mathcal{M}_1 \cong \mathcal{M}_2$, then $S_{EH}(\mathcal{M}_1) = S_{EH}(\mathcal{M}_2)$.

So, we don’t want to count isomorphic models $\mathcal{M}_1, \mathcal{M}_2$ twice. Physical quantities should be invariant across the models from the isomorphism class.

If there really are distinct isomorphic (and therefore physically indistinguishable) copies of physical worlds, then there is a strange indeterminism involved, as Einstein noticed, and as Earman and Norton wrote about in their 1987 paper. I was taught to think of this (and I think this is the received view amongst physicists) as a “purely representational” indeterminism.

Jeff

Posted by: Jeffrey Ketland on November 14, 2013 7:32 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I thought we already reached the conclusion that the category-theoretic point of view does not adopt the decategorifying version of “Leibniz equivalence”. (I put it in quotes because I am unsure that this is what Leibniz would have meant even if he knew the modern concept of “isomorphism”.) The resulting “indeterminism” is only apparent because the correct notion of “uniqueness” is “uniqueness up to isomorphism”.

The point I’m making here is different: when you say that we have “distinct indiscernible worlds”, you’re conflating mathematical/possible worlds with physical ones. When you say “we have a new world $\pi_\ast w$”, you’re making a mathematical construction. There’s no reason that you should expect to be able to “transport” the real world across an isomorphism to get a new “real” world!

Posted by: Mike Shulman on November 14, 2013 8:35 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

when you say that we have “distinct indiscernible worlds”, you’re conflating mathematical/possible worlds with physical ones. When you say “we have a new world ”, you’re making a mathematical construction.

No, really, I promise – that’s not what I’m doing. The mathematical models, referred to by the calligraphic variables “$\mathcal{M}_1$”, “$\mathcal{M}_2$”, etc., are indeed mathematical. The worlds, however, i.e., the things referred to by lower case variables “$w_1$”, “$w_2$”, etc., are physical. They’re being sharply distinguished. It’s crucial to avoid conflating models of worlds with worlds. By “distinct indiscernible worlds” I mean the usual meaning in the literature on the topic: $w_1$ and $w_2$ are distinct possible (physical) worlds, but are indiscernible (as in Leibniz’s example against Newton, where the Deity picks up all the matter in the universe and moves it one metre in some direction relative to “absolute space”).

David Lewis, for example, thinks of these possible worlds $w$ as mereological sums of all the physical stuff there. Others think of worlds as maximal states of affairs in some way. They are not the same as their mathematical representations. Here’s a nice survey article, just published, by my MCMP colleague Chris Menzel,

Menzel, C. 2013: “Possible Worlds”. (Stanford Encyclopedia of Philosophy)

Perhaps one can think of all possible worlds as forming a category; perhaps by a partial ordering of some kind on them.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 14, 2013 10:45 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Well, I guess we use the word “possible” in different ways (or maybe it’s the word “physical”). I wouldn’t have thought to call a world which is only possible physical, since the physical world is actual, not just possible. But anyway, if by “world” you mean only possible world, then I withdraw my objection.

Posted by: Mike Shulman on November 15, 2013 5:55 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike, on David Lewis’s view, which has countless concrete, physical possible worlds, there is a possible (physical) world where, e.g., there are talking donkeys! Lewis, in fact, rejects the idea of an “actual” world: all of his possible concrete worlds are on a par, and the inhabitants of any world will indeed call their world “actual”, just as the inhabitants of a temporal moment call their current moment “now”. But this needn’t imply there is a special Now.

In physics, we’ve always been talking of possible (physical) worlds in some sense: e.g., when we consider the configuration space of a system. The puzzle that arises with diffeomorphism invariance (= Leibniz equivalence) is always phrased in terms of whether diffeomorphically shifted models represent the same world or not. Carlo Rovelli’s Quantum Gravity monograph, Sc 2.2.5 (“General Covariance”, pp. 47-51), and then Sc 2.3 (“Interpretation”), have a nice account of his take on the matter. E.g.,

The two solutions $(e,x_a,x_b)$ and $(\tilde{e},\tilde{x}_a, \tilde{x}_b)$ are only distinguished by their localizations on the manifold. They are different in the sense that they ascribe different properties to manifold points. However, if we demand that localization is defined only with respect to the fields and particles themselves, then there is nothing that distinguishes the two solutions physically. In fact, concludes Einstein, the two solutions represent the same physical situation. The theory is gauge invariant in the sense of Dirac, under active diffeomorphisms: there is a redundancy in the mathematical formalism: the same physical world can be described by different solutions of the equations of motion.

It follows that localization on the manifold has no physical meaning. The physical picture is completely different from the example of the temperature field on the Earth surface illustrated in the previous section. In that example, the cities of Paris and Quintin were real distinguishable entities, independently from the temperature field. In GR, instead, general covariance is compatible with determinism only assuming that individual spacetime points have no physical meaning by themselves. It is like having only the temperature field, without the underlying Earth. (p. 50).

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 15, 2013 3:39 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

Mike, thanks - right, ok, now I am beginning to see what you (and John) have in mind. You interpret the non-uniqueness that Einstein noticed category-theoretically, and conclude that it doesn’t violate determinism—because while determinism as normally defined requires literal uniqueness, you can weaken this to uniqueness-up-to-isomorphism.

Right. Category theorists like Mike and I take it for granted that if you’ve got one of two isomorphic things, it doesn’t matter which one you’ve got.

This is almost the definition of ‘isomorphic’. The definition of ‘isomorphic’ is an efficient way of saying ‘anything you can do with this, you can do just as well with that’. So in category theory, for someone to complain that two things are merely isomorphic, not equal, is regarded as gauche—or even ‘evil’, though since I left the scene everyone else has become scared of that jokingly over-the-top characterization.

Posted by: John Baez on November 16, 2013 1:25 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John,

So in category theory, for someone to complain that two things are merely isomorphic, not equal, is regarded as gauche—or even ‘evil’, though since I left the scene everyone else has become scared of that jokingly over-the-top characterisation.

Yes (I think that’s amusing, btw!). But to try and pin down the debate here, consider the case of diffeomorphically-shifted spacetime models (not worlds yet!). Suppose we have the Schwarzschild solution $\mathcal{M} = (M,g,T)$, and a diffeomorphism $\phi : M \to M$, and let $(M,\phi_{\ast}g,\phi_{\ast}T)$ be the result of shifting the fields $g,T$ under $\phi$. Let me call this shifted model $\phi_{\ast}\mathcal{M}$. Then, all agree, we have:

$\mathcal{M} \neq \phi_{\ast}\mathcal{M}$

$\mathcal{M} \cong \phi_{\ast}\mathcal{M}$

In physics, we’re meant to think of these mathematical models as representing (possible) physical worlds, call them $W_{\mathcal{M}}$ and $W_{\phi_{\ast}\mathcal{M}}$. And the standard interpretation of diffeomorphism invariance (or (LE)), in Einstein, Wald, Carroll, Rovelli, …, is that the represented physical worlds are identical:

$W_{\mathcal{M}} = W_{\phi_{\ast}\mathcal{M}}$

But you seem to be saying that, on the category-theory view, they’re non-identical:

$W_{\mathcal{M}} \neq W_{\phi_{\ast}\mathcal{M}}$

Jeff

Posted by: Jeffrey Ketland on November 16, 2013 1:02 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I would be inclined to say rather that they’re isomorphic (by a specified isomorphism):

$W_{\mathcal{M}} \cong W_{\phi_\ast\mathcal{M}}$

and that one shouldn’t ask whether or not they are “identical” in any stronger sense than this. (Indeed, under the univalence axiom, there is no stronger sense.)

Posted by: Mike Shulman on November 17, 2013 7:50 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks Mike (and John).

I would be inclined to say rather that they’re isomorphic … and that one shouldn’t ask whether or not they are “identical” in any stronger sense than this.

Right - to begin with, I’d thought John’s idea, “isomorphic models represent isomorphic worlds” was a version of the original Maudlin-Butterfield approach (to the Hole argument given in Earman & Norton 1987), which said that when we have distinct isomorphic spacetime models $\mathcal{M}_1 \cong \mathcal{M}_2$, then there are two distinct, but isomorphic worlds, $W_1,W_2$. This is problematic, because of the physical indistinguishability of $W_1,W_2$ and because it would violate strict determinism. (I’m probably not being entirely fair to the original detailed lines of argument by Maudlin and Butterfield, but that’s how I’ve always understood the main ideas.)

But now I see that this isn’t quite the CT-view at all. The plausible CT-approach is to say that these possible worlds $W_1$ and $W_2$ are themselves isomorphic, and that is all one can say about them, and that determinism can be understood CT-ally as meaning “determinism-up-to-isomorphism”, as you suggest. But, to avoid saying that $W_1 \neq W_2$, there can’t be a general or global notion of identity on worlds,

$W = W^{\prime}$

much as in ETCS and SEAR, one does not have a global notion of identity for objects (structural sets). So, this seems to me to analogous to the CT situation where primitive identity is restricted to morphisms, because to define a category, one needs to say things like (when the sources/targets match),

$f \circ (g \circ h) = (f \circ g) \circ h$

and here $=$ is primitive and not defined.

So, on a CT view of mathematical representation of possible physical worlds, the worlds do not bear a primitive global identity relation, “$W = W^{\prime}$”. One can only ask questions about the morphisms between the worlds. Then one can perhaps bring in the apparatus of type theory, identity types and Univalence to make sense of all this.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 17, 2013 8:02 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

That’s more or less right. I should say that the lack of an identity relation (other than isomorphism, which univalence rechristens “identity”) is still a bit more radical a position, even among category theorists, than you might suspect from listening only to the Cafe regulars. Many or most category theorists, I think, still consider that there is a relation of equality on the objects of their categories; they just generally avoid using it. From that perspective, it is still meaningful to ask whether $W=W'$, and (if you accept LEM) then it’s either true or false, but the answer is essentially irrelevant. Even if $W=W'$, what matters (e.g. for transferring physical statements from one to the other) is the isomorphism $W\cong W'$, and this might not be an identity isomorphism even if it happens that $W$ and $W'$ are the same object.

Posted by: Mike Shulman on November 18, 2013 6:49 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Ok, thanks Mike.

Even if $W=W'$, what matters (e.g. for transferring physical statements from one to the other) is the isomorphism $W \cong W'$, and this might not be an identity isomorphism even if it happens that $W$ and $W'$ are the same object.

Right – because $W$ might have some non-trivial automorphisms.

Jeff

Posted by: Jeffrey Ketland on November 18, 2013 10:07 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

And the standard interpretation of diffeomorphism invariance (or (LE)), in Einstein, Wald, Carroll, Rovelli, …, is that the represented physical worlds are identical:

$W_{\mathcal{M}} = W_{\phi_{\ast}\mathcal{M}}$

But you seem to be saying that, on the category-theory view, they’re non-identical:

$W_{\mathcal{M}} \neq W_{\phi_{\ast}\mathcal{M}}$

I sure hope I didn’t say that! In category theory, it’s gauche to talk about whether objects are equal or not: it gets you in lots of trouble. What matters is whether they’re isomorphic… and you want to actually keep track of these isomorphisms, by giving them names.

In Makkai’s approach to category theory, called FOLDS, it’s actually forbidden to be gauche: you just can’t assert an equation between objects in a category! This is like preventing bad manners by making them physically impossible.

In homotopy type theory, equality is ‘rehabilitated’: in crude terms, we say that whenever two things are isomorphic, they are equal. This is kind of like preventing bad manners by making them mandatory, so they don’t count as bad manners anymore.

But both these approaches are a bit futuristic: a lot of smart people don’t know about them. Your typical ‘working-class’ category theorist simply learns good manners and avoids making proclamations like

$W_{\mathcal{M}} \neq W_{\phi_{\ast}\mathcal{M}}$

or

$W_{\mathcal{M}} = W_{\phi_{\ast}\mathcal{M}}$

when the gadgets in question are objects in a category. In ordinary math, as opposed to FOLDS or homotopy type theory, it causes nothing but trouble to make statements of this sort.

So, taking this tack, I was complaining that you said

$W_{\mathcal{M}} = W_{\phi_{\ast}\mathcal{M}}$

because I could see how it was getting you into a big mess: you were asking stuff like “why does Nature do something so weird?”

But my point was definitely not that

$W_{\mathcal{M}} \ne W_{\phi_{\ast}\mathcal{M}}$

Saying that would be like complaining of your rudeness and spitting in your face while doing so.

My point was that if you treat mathematical models of worlds as forming a category, you should treat worlds with same consideration, and keep track of the isomorphisms between them, instead of thinking about a set of worlds and worrying about whether they’re ‘equal’ or not.

Posted by: John Baez on November 19, 2013 2:28 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John,

My point was that if you treat mathematical models of worlds as forming a category, you should treat worlds with same consideration, and keep track of the isomorphisms between them, instead of thinking about a set of worlds and worrying about whether they’re ‘equal’ or not.

Yes, it took a while to dawn on me that you were thinking of the (physical, possible) worlds represented by the models category-theoretically too. This would be mean somehow rejecting the notion of a global (strict) identity relation on them.

I’m still not convinced with this category-theoretic approach to the Hole argument though. The physical intuition here is that physical worlds represented by isomorphic models are literally identical; this tells us something important about physics: that individual spacetime points have no “independent meaning by themselves”, as Rovelli puts it. This is weird! But it’s important too: it tells that worlds that are “structurally the same” are “the same” simpliciter. Indiscernible copies simply cannot exist.

That a world $W$ can be isomorphic to itself in many ways (i.e., $W$ has symmetries) seems to me quite separate from the claim that if $W_1$ and $W_2$ are isomorphic then $W_1 = W_2$. The first tells us something only about a particular world $W$; whereas the second tells us how to count all the distinct physical possibilities.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 19, 2013 6:33 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

As soon as we take something to form a groupoid, as with our models (and to the extent they model well, perhaps our worlds), then all kinds of questions become unanswerable. For example, we can’t ask how many different objects it contains.

There’s been plenty of talk of treating isomorphic objects in a category or groupoid as the same, but a further level up and we must treat groupoids themselves up to equivalence.

So, we might imagine that a groupoid with one object and two morphisms differs from one with 26 objects, between any two of which there are two morphisms. But it does not.

There is a concept of groupoid cardinality, but it’s invariant under equivalence of groupoids. In the case mentioned in the previous paragraph, both have cardinality $\frac{1}{2}$.

Posted by: David Corfield on November 19, 2013 10:59 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

The physical intuition here is that physical worlds represented by isomorphic models are literally identical

As we’ve said before, the idea is that that’s the wrong physical intuition.

As David says, once things form a groupoid, it’s best not to worry about whether they’re literally equal or not. One can demand that a groupoid be skeletal, but usually that’s not a productive thing to do. One can also consider the set of isomorphism classes in a groupoid, which is a set and hence has a cardinality in the ordinary sense; that might be what you want if you want to “count the distinct physical possibilities”. But the worlds themselves are not isomorphism classes; that would lose too much information.

Posted by: Mike Shulman on November 19, 2013 6:03 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Mike,

But the worlds themselves are not isomorphism classes; that would lose too much information.

Right, the worlds are not isomorphism classes.

So, on the approach I like, the worlds are the result of saturating the abstract structure of the spacetime model in question with intensions (physical relations). In general, the abstract structure of a model $\mathcal{A} = (A, \dots)$ loses no information except the “identity” of the elements of the carrier set $A$. It encodes all structural information about $\mathcal{A}$. E.g., as I mentioned before, automorphisms of $\mathcal{A}$ correspond to logically equivalent skolemizations of the formula $\Phi_{\mathcal{A}}(\vec{X})$.

And it then follows that when the spacetime models are isomorphic, the corresponding worlds are literally identical.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 20, 2013 7:56 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

As I said above, you’re forming the skeleton. The question then is what is gained by it.

Mike just said:

One can demand that a groupoid be skeletal, but usually that’s not a productive thing to do.

A groupoid and its skeleton are equivalent. In homotopy type theory one can not distinguish them. If you can establish a real gain by skeletonizing, that’s a blow to HoTT.

That gain had better persist when you extend to think about what’s needed in further developments of physics. Look at 1.1.1 of Urs’ paper.

Entities of general gauge theory $\infty$-Lie algebra $\mathfrak{g}$ with gauge $\infty$-Lie group $G$ – connection with values in $\mathfrak{g}$ on a $G$-principal $\infty$-bundle over a smooth $\infty$-groupoid $X$.

But skolemising is just dealing with first-order structure. That concerns only the lowest homotopy levels of HoTT, like dependent types from sets to propositions. How will you cope when you need your spacetimes to be objects of higher groupoids?

Posted by: David Corfield on November 20, 2013 9:15 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Even worse, we’ve been forgetting the smoothness of $[\Sigma, \mathbf{Fields}//Diff(\Sigma)$. As a smooth groupoid this is not equivalent to its skeleton as an ordinary groupoid. But we need the smooth structure in order to work the variational principle for the Einstein-Hilbert action whose critical points give Einstein’s equations.

Posted by: David Corfield on November 20, 2013 9:45 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

The idea is that the map

$\mathcal{A} \mapsto \Phi_{\mathcal{A}}$

is a skeleton? No, it’s not a skeleton, or anything like that, as far as I can tell.

It is a mapping from the proper class $Mod$ of relational models (of arbitrary relational signature) to the proper class of “categorical diagram formulas” over the infinitary language $L_{\infty,\infty}$.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 20, 2013 2:29 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

In a trivial sense, of course you’re not forming a skeleton, since you don’t even mention categories. I was just trying to jump the gap of incommensurability to understand from our side what the effect is of what you are doing.

If what you are doing is taking a class of things with for each pair a set of compatible equivalences. And if for each class of objects with mutual equivalences between objects, you use something to label that class, in such a way that its self-equivalences match up with those of the original corresponding objects, then from our perspective that’s forming a skeleton. We doubt you gain anything by this in comparison to the original, since we see them as equivalent groupoids (to the extent at least that we’re not concerned with smooth structure).

If this is right, then still from your side of the gap, it may be important the actual elements of the classes involved. You may have a reason to prefer having some one thing stand in for the class. If it’s a set, you may care what its elements are.

Aside from whether or not we are satisfied or dissatisfied with each other’s presentation of cases of gauge invariance, there’s also what comes next practically. One thing is to deal with what we call 2-groupoids, and we have to do this to cater for the field configurations of the Kalb-Ramond field and other higher gauge fields. There we need to represent not only gauge equivalences, but also gauge-of-gauge equivalences.

Posted by: David Corfield on November 20, 2013 5:50 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Jeffrey wrote:

I think maybe you took it that the entity $\Phi_{\mathcal{A}}(\vec X)$ that I mentioned above is a set or an equivalence class?

I don’t really care what it is. I just care what it does. All that really matters to me is this remark of yours:

$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}} iff \mathcal{A} \cong \mathcal{B}$

This says that the $\hat{\Phi}_{\mathcal{A}}$ thingies are in 1-1 correspondence with isomorphism classes of the $\mathcal{A}$ thingies.

And that means you’re decategorifying! You are starting with a groupoid whose objects are the $\mathcal{A}$ thingies. They have lovely and interesting isomorphisms between them. And then you’re stomping these isomorphisms into the dirt, crushing them into mere equations, by turning your attention to the $\hat{\Phi}_{\mathcal{A}}$ thingies. The $\hat{\Phi}_{\mathcal{A}}$ thingies are in one-to-one correspondence with the isomorphism classes of objects in the groupoid you should be studying. They form a mere set.

When you do this sort of thing, you lose lots of important information. The whole idea behind modern physics is that we should keep track of isomorphisms (aka ‘symmetries’), not crush them down to equations.

I know you’re doing it with the best of intentions. Leibniz was a smart dude, and his principle of ‘identity of indiscernibles’ was a great idea. But he didn’t have category theory at his disposal. Now we do, and homotopy type theory lets us implement his idea in a less destructive manner.

And it’s the univalence axiom that does this: it says that equivalence is equivalent to identity.

This implements ‘identity of indiscernibles’ without losing track of the isomorphisms between those indiscernibles.

Posted by: John Baez on November 11, 2013 4:02 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

John, yes, I get the point you’re making, but I’m not sure the structural information that you mean, about automorphisms and isomorphisms, is actually lost— … or “crushed” !

You (and Mike) rightly say that there’s a one-to-one correspondence between the $\hat{\Phi}_{\mathcal{A}}$-thingies and the equivalence classes of $\mathcal{A}$-thingies. That’s right. With abstraction principles like “the direction of line L = the direction of line M iff L is parallel to M”, or “the cardinal of $X$ = the cardinal of $Y$ iff there’s a one-to-one correspondence between $X$ and $Y$”, the idea is to abstract away from something one wishes to “get rid of”: in the case that’s interesting for structuralism, what one wants to “get rid of” is the carrier set, while retaining all structural information common to the isomorphic models/structures (in the groupoid).

But the $\Phi_{\mathcal{A}}$-thingies are themselves logically structured. For example, automorphisms of $\mathcal{A}$ correspond to logical equivalence between skolemizations of the formula $\Phi_{\mathcal{A}}$ (roughly, relabelling the first-order variables with constants). So, this information isn’t lost at all! It’s encoded into the formula. So, only the various carrier sets have been thrown away–which is what the structuralist intended, in trying to make sense of the notion of “the structure” of the original object.

[By a coincidence, after I’d been thinking about this kind of thing for about a year, I met Steve (Awodey) when he visited Munich, and he mentioned the HoTT stuff and Univalence. That’s why I’ve wondered since then how this stuff, and Aczel’s “structure identity principle”, is all connected to other accounts of abstract structure.]

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 6:21 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Maybe what’s at stake is the difference between decategorification and forming a skeleton.

Let’s keep it simple and consider a groupoid with two models as objects and two isomorphisms between them. Taking equivalences classes we find there is just a single class. I just have a singleton set. Now, I can’t retrieve the original information, e.g., that there’s a nontrivial automorphism on a model.

Unless, and it sounds like this is happening, what I really do is retain enough information in what one of those models is, that I can know it has a nontrivial automorphism.

If that’s what’s happening, it isn’t forming equivalence classes/decategorifying. It’s forming a skeleton of the groupoid.

The skeleton of my groupoid above has a single object and two automorphisms.

Forming skeletons comes with its own issues, e.g., it may require the axiom of choice, but at least it retains information.

On the other hand, there’s something category-theoretically unnatural about singling out an entity from another entity it’s equivalent to. Let’s see what the HoTT book has to say about it:

There is not really any notion of “skeletality” for our categories, unless one considers Definition 9.1.6 itself to be such. (p. 302)

Obviously, Mike could explain what this means.

Posted by: David Corfield on November 11, 2013 9:34 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David, my fault here, as I’m not sufficiently familiar with the notion of decategorification, but it seems intimately related to what in logic & philosophy gets called an abstraction principle. Suppose we have some entities which bear an equivalence relation $\equiv$. Suppose we have some sort of function $\alpha$ on these entities taking us from $X$ to $\alpha(X)$. A principle of the form:

$\alpha(X) = \alpha(Y)$ if and only if $X \equiv Y$

is usually called an abstraction principle in the philosophy literature (usually connected to structuralism, logicism and Frege). That’s what corresponds here to “decategorification”? Reading the nLab notes on this, an abstraction principle seems to be decategorifying a setoid. Is that right?

So it seems right then to say that pretty much all the constructions that give us ordered pairs, the natural numbers, the integers, the rationals and the reals (these are examples of abstraction principles) are decategorifications of setoids. For example,

Ordered pairs (OP): $op(x,y) = op(w,z)$ iff ($x = w$ and $y = z$)

Integers (INT): $z(n_1, n_2) = z(k_1,k_2)$ iff $n_1 + k_2 = k_1 + n_2$

etc.

In many cases, abstraction principles are proof-theoretically harmless: e.g., if one doesn’t like the implementation of the ordered pair $(x,y)$ as Kuratowski’s $\{\{x\},\{x,y\}\}$, because of the pointless/redundant information involved, then one can simply add (OP) as a primitive axiom, to $ZF$ set theory, treating $op(-,-)$ as a new binary function symbol. Call this $ZF^{op}$. Then one shows that $ZF^{op}$ is a conservative extension of $ZF$.

Is that roughly right? – abstraction principles like these are examples of decategorification of setoids?

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 3:52 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I think setoids are spoken about in constructivist circles. The page on them seems to have become Bishop set.

Decategorification applies to any category. It throws away all but isomorphisms, and then forms the equivalences classes of objects related to each other by an isomorphism.

We can think of this process happening to an ordinary set and equivalence relation. We just form the groupoid whose objects are the set’s elements, and for each pair of objects an isomorphism if they’re related. This forms a groupoid, and its decategorification is the set of equivalence classes.

Decategorification in that case isn’t so violent since the resulting set (with identity morphisms) is equivalent to the groupoid I mentioned.

The damage happens when we have more structure. So take the category of finite sets and isomorphisms. Decategorification gives the set of natural numbers. Now ‘2’ no longer remembers that it came from a set with two permutations.

Forming the skeleton on the other hand, reduces the category of finite sets so that there is one object for each connected component. I.e. here, an exemplar for each cardinality. This retains the automorphisms.

From what you wrote above, you’ve retained some logical equivalences on whatever it is that standing for a class, so I suspect you’re looking for a skeleton.

Posted by: David Corfield on November 11, 2013 6:22 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I wonder if you’re doing something like the following.

Take a formula to express cardinality 2:

$\exists x \exists y (x \neq y \wedge \forall z(z = x \vee z = y)).$

Skolemize

$a \neq b \wedge \forall z(z = a \vee z = b)).$

Take this to represent the class of all 2 element sets, but then notice there’s a nontrivial automorphism on exchanging $a$ and $b$.

If so, that is forming a skeleton. It’s not part of the Zen of HoTT, but it hasn’t lost the automorphism.

Posted by: David Corfield on November 12, 2013 8:43 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

Right - pretty much, yes. The propositional function here expressed by the formula is the “abstract cardinality structure” for $2$ and logically equivalent skolemizations of it correspond to automorphisms. This generalizes for any $\mathcal{A}$, using infinitary logic if need be, when the carrier set of $\mathcal{A}$ is infinite.

Jeff

Posted by: Jeffrey Ketland on November 12, 2013 10:27 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

We can illustrate the difference between forming the action groupoid and forming the set of equivalence classes in this example:

Imagine we can look into a space where we see two objects. Each of them can have its light on or off. Now we report what we see to each other. I can tell you I see two, one or no lights. In cases where there’s one light, I can refer to it, knowing you’ll know which I mean. Otherwise I won’t be able to single one out. No other information is available, such as relative positions.

So what’s the configuration space? If I opt for the equivalence class approach, I find

$[Balls,2]/Sym(Balls)$

a set of cardinality 3.

On the other hand, the action groupoid is

$[Balls,2]//Sym(Balls).$

(Up to equivalence) this is a groupoid with four objects. The 2 light object has a non-trivial automorphism, as does the 0 light object. The other two objects have a single arrow from one to the other.

There’s more information in the latter, in that I can decategorify to the former, but I can’t reconstruct the latter from the former.

Hmm, maybe this bears on the discussions around covariance and whether and how spacetime can be said to exist. With the extra information in the action groupoid, am I then able to reconstruct the objects (or manifold in the GTR case) in a way that I couldn’t if I had collapsed to equivalence classes?

Posted by: David Corfield on November 10, 2013 9:58 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

I’m trying to get the setup here. We have distinct two balls, $a,b$ say. So let $B = \{a,b\}$ be the carrier set for the models, where $a \neq b$. The “states” are given by subsets of $B$, corresponding to which balls are lit. These are

$S_1 = \varnothing$.

$S_2 = \{a\}$.

$S_3 = \{b\}$.

$S_4 = \{a,b\}$.

And so the four “models” are:

$\mathcal{M}_1 = (B, S_1)$.

$\mathcal{M}_2 = (B, S_2)$.

$\mathcal{M}_3 = (B, S_3)$.

$\mathcal{M}_4 = (B, S_4)$.

$Sym(B) = \{Id, (ab)\}$, where $Id$ is the identity map $B \to B$, and $(ab)$ is the transposition that swaps $a$ and $b$.

Then the symmetry groups of these models are:

$Aut(\mathcal{M}_1) = \{Id, (ab)\} = Sym(B)$.

$Aut(\mathcal{M}_2) = \{Id\}$.

$Aut(\mathcal{M}_3) = \{Id\}$.

$Aut(\mathcal{M}_4) = \{Id,(ab)\} = Sym(B)$.

The pair $\mathcal{M}_2$ and $\mathcal{M}_3$ may count as “gauge equivalent”, because the transposition $(ab)$ is an isomorphism from $\mathcal{M}_1$ to $\mathcal{M}_2$. (All other pairs are not gauge equivalent.)

Is that the idea?

Jeff

Posted by: Jeffrey Ketland on November 10, 2013 3:18 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Right.

So I take it that there are four states. I may then be told that the balls can swap places from one day to the next, but the lights will only be altered on the balls at the beginning of the week. If I see just one lit on Monday, I’ll know whether or not they swapped the balls on Tuesday. However, if neither or both are lit, I can’t know whether or not they’ve been swapped.

The action of the exchange of balls on the states can be represented as a groupoid with objects $(0, 0), (0, 1), (1, 0), (1, 1)$. In addition to trivial morphisms, there is a nontrivial automorphism on $(0, 0)$ and one on $(1, 1)$, and an isomorphism between $(0, 1)$ and $(1, 0)$. This is

$[Balls, 2]//Sym(Balls).$

The analogy with GTR would now go something like: covariance demands that any laws I write be invariant under exchange of balls. For example, any quantity defined on the configuration space should respect isomorphisms. I may then think to myself that I should just form isomorphism classes

$[Balls, 2]/Sym(Balls),$

that is a set of cardinality 3. Perhaps there’s a luminosity function which records how many lights are on, which evidently respects quotienting into classes.

Now someone may think that any mention of the identity of balls is pointless. All we have are 0, 1 or 2 lights on. The equivalence class picture seems to be saying just this. But the action groupoid picture says there’s information to be retained in

$[Balls, 2]//Sym(Balls).$

A luminosity function (functor) to the natural numbers will have to be constant on each component of the groupoid, but I may need to map not into a set of values, but rather a groupoid, then a difference will show.

So there’s a question, when in physics does

$[\Sigma, \mathbf{Fields}]//Aut(\Sigma)$

make a difference?

Posted by: David Corfield on November 11, 2013 11:02 AM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

And we have an answer, which may take a little time for me to understand.

But that’s why I’m so excited by what’s going on. We may just have in our hands a formalism which not only deals beautifully with the mathematics, but also lines up with important physical principles. It forces you to think the right way. Violate proper homotopy quotienting and you’ll destroy locality in your physics.

This relates to what has been discussed above. I’ve never found the typical tools in the philosopher’s toolbox to provide anywhere near this level of guidance. Indeed, at times they seem to lead one to ask the wrong sort of question.

Posted by: David Corfield on November 11, 2013 12:32 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

I’ve never found the typical tools in the philosopher’s toolbox to provide anywhere near this level of guidance. Indeed, at times they seem to lead one to ask the wrong sort of question.

The tools that I see used by philosophers in papers and talks include: first-order logic, type theory, lambda-abstraction, set theory, computable functions, formalised systems of arithmetic, formalized syntax, diagonalization, confirmation theory, mereology, higher-order logic, non-classical logics, epistemic, tense and modal logics, Kripke frames, model theory, abstraction principles, graph theory, differential geometry, category theory, etc., etc. It’s extremely diverse, wide-ranging and both conceptually and doctrinally pluralistic. In 18 months at Munich, there were talks on all sorts of things like this. So, I don’t get what you’re referring to, I’m afraid.

I think your perception of things is coloured by your being a fighter in the Set/Cat War. And people shy away from this, I guess because it reminds them of Sayre’s law, “the stakes are so low”. Though sometimes they do: e.g., the 2011 paper by Linnebo & Pettigrew I mentioned upthread or Burgess’s forthcoming book. Plenty of people use the methods you’re interested in: offhand, Albert Visser, Elaine Landry, Jeremy Butterfield, Jonathan Bain and Hans Halvorson do.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 4:30 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Sorry, that was heavy-handed of me. I didn’t mean to suggest a lot of perfectly good work isn’t going on as you suggest. I just tend to err on the side of being suspicious when people take up certain formalisms to do philosophical work.

As a paid-up fan of Bayesianism and category theory, I’m happy to see them used well. For example, I’d be delighted if the categorical work on modal logic of Awodey, Kishida and Kotzsch takes off.

But often in a talk I find myself wishing there would be a little more reflection on how much work is being done by a formalism, or whether there might not be a better formalism available.

I’m excited in this case because something foundational for maths is lining up beautifully with something foundational for physics.

Posted by: David Corfield on November 11, 2013 6:36 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

David,

I’m excited in this case because something foundational for maths is lining up beautifully with something foundational for physics.

There are two things that seem to me might become more widely discussed in phil of maths and physics in the next few years:

1. Does HoTT/CT provide a good version of mathematical structuralism?
2. Does HoTT/CT shed light on the spacetime substantivalism/relationism debate?

But whether the answers to these are yes or no isn’t very clear, at least to me; still, it’s because of these two (related) issues that I took a greater interest in this stuff (though I’m a neutral on the whole Set/Cat thing – too boisterous!).

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 11, 2013 7:35 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Great. These are just the sorts of areas in HoTT’s range.

It may well be that though that expectations of what counts as an answer will be modified in the encounter, rather as certain things had to give when coming to see what quantum mechanics told us about the world.

Posted by: David Corfield on November 11, 2013 10:49 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

Thanks David – and to Urs, Mike and John too – for answers, interesting ones, on these rather philosophical points about foundations of physics & maths - applicability, representation, urelements/comprehension, Leibniz equivalence/gauge equivalence in GR, role of underlying logic, meaning of “$=$”, etc. I learnt a lot (and have been reading Urs’s monograph at the same time too).

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 12, 2013 12:38 PM | Permalink | Reply to this

### Re: The HoTT Approach to Physics

And thank you too, Jeff, for your part in the discussions, and making it clearer what kinds of places we might try to construct bridges towards from HoTT.

Posted by: David Corfield on November 13, 2013 8:46 AM | Permalink | Reply to this
Read the post The Covariance of Coloured Balls
Weblog: The n-Category Café
Excerpt: covariance through coloured balls
Tracked: November 19, 2013 1:06 PM

Post a New Comment