### General Covariance in Homotopy Type Theory

#### Posted by Urs Schreiber

In physics, the term general covariance is meant to indicate the property of a physical system or model (in theoretical physics) whose configurations, action functional and equations of motion are all equivariant under the action of the diffeomorphism group on the smooth manifold underlying the spacetime or the worldvolume of the system. The archetypical example of a generally covariant system is of course Einstein-gravity / “general relativity”.

I indicate here how general covariance has a natural formalization in homotopy type theory, hence internal to any $\infty$-topos. For background and all details see at *general covariance* on the $n$Lab, and the links given there.

Of course a basic idea of traditional dependent type theory is that types $A$ may appear in context of other types $\Gamma$. The traditional interpretation of such a dependent type

$x : \Gamma \vdash A(x) : Type$

is that of a $\Gamma$-parameterized family or bundle of types, whose fiber over $x \in \Gamma$ is $A(x)$.

But in homotopy type theory, types are homotopy types, of course, and, hence so are the contexts. A type in context is now in general something more refined than just a family of types. It is really a family of types equipped with *equivariance* structure with respect to the homotopy groups of the context type.

Specifically, if the context type is connected and pointed, then it is equivalent to the delooping $\Gamma \simeq \mathbf{B}G$ of an $\infty$-group $G$. One finds (this is discussed here) – that the context defined by the type $\mathbf{B}G$ is that of $G$-equivariance: every type in the context is a type in the original context, but now equipped with a $G$-∞-action. In a precise sense, the homotopy type theory of $G$-∞-actions is equivalent to plain homotopy type theory in context $\mathbf{B}G$.

Consider this for the case that $G$ is an automorphism $\infty$-group of a type $\Sigma$ which is regarded as representing spacetime or a worldvolume. We show that in this context the rules of homotopy type theory automatically induce the principle of general covariance and naturally produce configurations spaces of generally covariant field theories: for $\mathbf{Fields}$ a moduli object for the given fields, so that a field configuration is a function $\phi : \Sigma \to \mathbf{Fields}$, the configuration space of covariant fields is the function type $(\Sigma \to \mathbf{Fields})$ but formed in the “general covariance context” $\mathbf{B}\mathbf{Aut}(\Sigma)$. When interpreted in smooth models, $\mathbf{Conf}$ is the smooth groupoid of field configurations and diffeomorphism gauge transformations acting on them, the Lie integration of the BRST complex whose degree-1 elements are accordingly called the *diffeomorphism ghosts*.

More precisely, I show the following (and thanks again to Mike, for discussion of this here).

**Definition.** Consider in homotopy type theory two types $\vdash \Sigma, \mathbf{Fields} : Type$, to be called *spacetime* and *field moduli*. Let

$\vdash \mathbf{B}\mathbf{Aut}(\Sigma) : Type$

be the image of the name of $\Sigma$, with essentially unique term

$\vdash \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \,.$

Perform the canonical context extension of $\Sigma$ and trivial context extension of $\mathbf{Fields}$ to get types in context

$\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma : Type$

and

$\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \mathbf{Fields} : Type \,.$

Form then the type of field moduli “$\mathbf{Conf} \coloneqq (\Sigma \to \mathbf{Fields})$” in this context:

$\mathbf{Conf} \coloneqq \;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Fields}) : Type \,.$

**Proposition.** The categorical semantics of $\mathbf{Conf}$ in the model of smooth cohesion, and for $\Sigma$ a smooth manifold, is given by the diffeological groupoid

$\mathbf{Conf} = [\Sigma, \mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma)$

whose objects are field configurations on $\Sigma$ and whose morphisms are diffeomorphism gauge transformations between them. In particular the corresponding Lie algebroid is dual to the (off-shell) BRST complex of fields with diffeomorphism ghosts in degree 1.

## Re: General Covariance in Homotopy Type Theory

This looks great. So you’re interested in $(X \to Y)$ with equivalences under automorphisms of $X$? Are there other unobvious instances of this phenomenon?

Going back to basics, in a discrete setting, there are simple combinatorial situations where you work out how many distinct ways there are of colouring a die with, say, at most four colours. So you take all $4^6$ colourings and let $S_4$ act on the cube.

Does anything interesting happen with $X$ having higher homotopy?