The n-Category Café

So, last week I happened to be reading a paper by John Norton entitled General covariance and the foundations of general relativity: eight decades of dispute, and I ran across the following passage.

There is a presumption in much modern interpretation of Einstein… that much of what he says cannot be taken at face value. (Why does Einstein make such a fuss about introducing arbitrary spacetime coordinates? We have always been able to label spacetime events any way we please!)… [My] proposal… is that our modern difficulty in reading Einstein literally actually stems from a change… in the mathematical tools used…

In recent work… we begin with a very refined mathematical entity, an abstract differentiable manifold… We then judiciously add further geometric objects only as the physical content of the theory warrants….

In the 1910s, mathematical practices in physics were different…. one used number manifolds — $R^n$ or $C^n$ for example. Thus Minkowski’s ‘world’… was literally $R^4$, that is it was the set of all quadruples of real numbers.

Now anyone seeking to build a spacetime theory with these mathematical tools of the 1910s faces very different problems from the ones we see now. Modern differentiable manifolds have too little structure and we must add to them. Number manifolds have far too much structure…. the origin $\langle 0,0,0,0\rangle$ is quite different from any other point, for examples… The problem was not how to add structure to the manifolds, but how to deny physical significance to existing parts of the number manifolds. How do we rule out the idea that $\langle 0,0,0,0\rangle$ represents the preferred center of the universe…?

Felix Klein’s Erlangen program provided precisely the tool that was needed. One assigns a characteristic group to the theory… Only those aspects of the number manifold that remain invariant under this group are allowed physical significance…. As one increases the size of the group, one strips more and more physical significance out of the number manifold.

This passage places the two viewpoints on tensors in a larger context, both historically and mathematically. It’s not just about coordinates: it’s about whether we are adding structure to something excessively abstract, or subtracting structure from something excessively concrete. The “transformation rule” approach to tensors corresponds to the Erlangen subtractive approach: when we consider only structures invariant under our characteristic group, we can only use measurements that transform in some well-defined way under that group action.

Now, suppose that we are working in HoTT, and we want to define “the type of Minkowski spacetimes”. The modern mathematician who knows some type theory would go about this in a fairly straightforward way: a Minkowski spacetime is a 4-dimensional real affine space equipped with a certain kind of bilinear form, and we can express this in type theory in the usual way as an iterated $\Sigma$-type (in proof assistants, a “record”):

$$Mink \coloneqq \sum_{M:Type} \sum_{v:RealAffineSpace(M)} \sum_{b:BilinearForm(M,v)} Dim(v,4) \times Nondeg(b) \times Symm(b) \times Sig(b,(+,+,+,-))$$

Applying univalence, we conclude that for $M,N:Mink$, the identity type $M=N$ is equivalent to the type of affine isomorphisms $M\cong N$ preserving the metrics, as we would expect. In particular, $Mink$ is a 1-type.

Now, however, note that $Mink$ is also connected. That is, for any two $M,N:Mink$ there exists such an isomorphism; we can construct it by choosing origins and bases of $M$ and $N$ that put their metrics in canonical form. (Since $M$ and $N$ are not equipped with such bases, this is the truncated “there exists”, i.e. “there merely exists”; in symbols what we have is $\Vert M=N\Vert$.) Since $Mink$ is also clearly inhabited (by the standard $\mathbb{R}^{3,1}$), it is a $K(G,1)$. And what is $G$? It’s just the Poincare group $ISO(3,1)$.

But, we may now notice, there is another way to construct $K(G,1)$s for any group $G$ in HoTT, using higher inductive types. (These two approaches to classifying spaces also came up in another recent post.) Specifically, the HIT $K(G,1)$ is generated by the following constructors: a point $x$, a path $g:x=x$ for each $g\in G$, 2-paths imposing the multiplication table of $G$, and a 1-truncation constructor to make it a 1-type. Since $K(G,1)$s are unique up to equivalence, if in this construction we take $G$ to be the Poincaré group, we obtain a very different-looking construction of a type that is nevertheless equivalent to $Mink$; let’s call it $Mink'$.

The point is that $Mink'$ can be regarded as the 1910s Erlangen version of the type of Minkowski spacetimes, where instead of starting from an abstract thing with too little structure (an affine space) and adding stuff (a metric), we start from a concrete thing with too much structure ($\mathbb{R}^4$) and impose invariance under some automorphism group (the Poincaré group). The basepoint $x:Mink'$ can be thought of as representing $\mathbb{R}^4$, and the added automorphisms $g:x=x$ “force everything we say about $x$ to be invariant under the Poincaré transformation group”.

Of course, the point $x$ is not literally $\mathbb{R}^4$. But from the fact that the Poincaré group acts on $\mathbb{R}^4$ (which is of course necessary for this approach to get off the ground), we get a canonical map $Mink' \to Type$ sending $x$ to $\mathbb{R}^4$. (This is basically immediate from the universal property of $Mink'$ as an HIT, plus univalence to identify paths $\mathbb{R}^4=\mathbb{R}^4$ with automorphisms.) We could even declare this map to be an implicit coercion, so that we can informally identify $x$ with $\mathbb{R}^4$. Finally, of course, this map also factors through our original type $Mink$ by the canonical equivalence $Mink' \simeq Mink$.

I’m still pondering what conclusion to draw from all of this. It seems that modern mathematics, perhaps driven by set theory’s axiom of extensionality, has gone to the extreme of defining everything so that the already-present notion-of-sameness becomes the desired one. For instance, this is how we define the quotient of an equivalence relation in set theory: we take the elements of the quotient to be the equivalence classes, so that by the axiom of extensionality, if $x\sim y$ then their equivalence classes are equal (for the already-present notion of “equal” in set theory). The same is true for higher sorts of “sameness” in category theory: we define things like “Minkowski space” using complicated notions like vector space, bilinear form, and signature so that the “natural” sort of sameness for such gadgets, namely isomorphism in the appropriate category (which in the presence of univalence can be identified with equality in the appropriate type), is what we want it to be.

But it doesn’t have to be that way. For instance, Bishop proposed that to specify a set we should be obligated to specify not only its elements but also what it means for two of those elements to be equal. While I believe that he (and the closely related literature on “setoids” in type theory) didn’t go far enough — with HITs we can make our “specified equality” be the actual equality, so that we don’t need to worry about proving or hypothesizing that it is preserved by functions — this is a valid step in the other direction. Our above example of $Mink'$ shows that we can also define higher types this way: we defined (something equivalent to) “Minkowski spacetimes” without making any reference to a metric!

So perhaps one way to state the conclusion is that HITs unify Bishop’s ideas on sets with the Erlangen approach to geometry. Bishop said that when we define a set, we are free to specify under what conditions two of its elements are the same as each other. And the Erlangen program says that when we define a type of structures, we are free to specify in what ways such a structure is the same as itself. Of course, to a higher category theorist this shouldn’t be at all surprising, since both are a quotient construction — the quotient of an equivalence relation and the homotopy quotient of a group action. But nevertheless, I feel like I know something that I didn’t know a week ago.