could also say ’third column’.

Yes, have changed it. Thanks.

I’m trying to think about when we do something similar in every day reasoning,

While I am not sure about the every day of the man on the street, one could maybe say that while Einstein and his contemporaries were still struggling heavily with the idea (Einstein-Grossmann 14 is explicitly rejecting the idea), their students learned the lesson to many theoretical physicists these days “thinking covariantly” has become second nature in a way that is not unlike “thinking in a context where everything is modulo diffeomorphisms”. Of course just as often it still happens that people forget the lesson.

whether there’s something special about gravitation as a force that lends itself to this nice ’within a context’ account

Actually, no, I think it is important that “general covariance” is not specific to gravity. Back then in the article “QFT and the Jones polynomian” Witten still highlights this idea as new, that topological field theories share the same feature. Indeed, in Chern-Simons theory it is there, and the only reason why one does not see it emphasized so much is that CS-theory has yet another gauge symmetry, and that by coincidence of low dimensions it so happens that in 3d every diffeomorphism acting on a CS gauge field is equivalent to just a gauge transformation acting on that gauge field.

This fact is embodied also in the $(\infty,n)$-cobordism hypothesis/theorem: everything there is “generally covariant”.

I finally ’saw’ the truth of the principle of equivalence at about 4:18 into this clip

Nice. I have added the link to *equivalence principle (physics)*

The account in ’Generally covariant field of gravity’ is given in terms of the specific topos SynthDiff∞Grpd. How far can one just let the properties of differential cohesion do the job? I mean could there be a large chunk of general relativity present in a wide range of differential cohesive ∞-toposes?

Yes, absolutely. Indeed the point of an abstract homotopy type theoretic discussion of general covariance (or any other concept in physics) is precisely to see that and how it is independent of the specific model and is a more general principle.

I was just amplifying this to Gabriel Catren, my host in Paris this month. He is interested in describing geometric quantization via integrable real polarizations as a quotient map analogous to gauge quotients, and the construction that does this is a very fundamental one in homotopy type theory, hence is exceedingly more general than it might seem on first sight. I started making notes on that here (purely technical for the moment, will need to find time to expand on the story…)

]]>One query. The account in ’Generally covariant field of gravity’ is given in terms of the specific topos SynthDiff∞Grpd. How far can one just let the properties of differential cohesion do the job? I mean could there be a large chunk of general relativity present in a wide range of differential cohesive $\infty$-toposes?

I guess that’s to know answers to some of the issues being discussed on the other thread.

]]>So now maybe

Here the ∞-image is directly read off to be the factorization in the second column from the right of

could also say ’third column’.

All very trivial, but I’m trying to understand what perhaps is one of the most sophisticated pieces of working within a complex context in type theory. I’m trying to think about when we do something similar in every day reasoning, and whether there’s something special about gravitation as a force that lends itself to this nice ’within a context’ account. But little time today.

By the way, I finally ’saw’ the truth of the principle of equivalence at about 4:18 into this clip of feathers and ball falling in a vacuum.

]]>Yes! Thanks. I have fixed it.

]]>Just to check, where it says

The categorical semantics of the dependent type

$D^n :\mathbf{B}GL(n), T \Sigma : \mathbf{B}\mathbf{Aut}(T \Sigma): T \Sigma : Type$

is the third column from the right in the above diagram.

that should be $\vdash$ rather than :, and ’third column (from left)”?

]]>have add a paragraph to a new subsection *general covariance – Formalization in HoTT – Informal introduction*.

I have expanded and polished the section *Generally covariant field of gravity* more.

Here some rough notes further spelling out the homotopy type theoretic formula for the generally covariant configuration space of Einstein-gravity

$\vdash \prod_{D^n : \mathbf{B}GL(n)} \sum_{T \Sigma : \mathbf{B}\mathbf{Aut}(T \Sigma)} (T \Sigma \to GL(n)\sslash O(n)) : Type \,.$in more detail. (I will turn this into something more readable later. Need to quit now after a long day, but want to record these quick notes for later processing. Don’t bother if you are just following leisurely).

We spell out what this means.

We work in synthetic differential cohesion. Let there

$\vdash D^n : Type$denote the first-order infinitesimal neighbourhood of the origin in $\mathbb{R}^n$. Observing that the general linear group is

$GL(n) \simeq \mathbf{Aut}(D^n)$we will write the unique term of $\mathbf{B}GL(n)$ as

$\vdash D^n : \mathbf{B} GL(n) \,.$For $\Sigma$ a smooth $n$-dimensional manifold, we write

$\Sigma \stackrel{\vdash T \Sigma}{\to} \mathbf{B} GL(n)$for the map modulating the $GL(n)$-principal bundle to which the tangent bundle is associated.

Accordingly we have

$D^n : \mathbf{B}GL(n) \vdash \mathbf{B}\mathbf{Aut}(T \Sigma) : Type$with unique term

$D^n : \mathbf{B}GL(n) \vdash T \Sigma : \mathbf{B} \mathbf{Aut}(T \Sigma) \,.$Let then $\mathbf{orth} : \mathbf{B} O(n) \to \mathbf{B}GL(n)$ be given by the inclusion of the maximal compact subgroup. We have a fiber sequence

$\array{ GL(n)/O(n) &\to& \mathbf{B}O(n) \\ && \downarrow^{\mathrlap{orth}} \\ && \mathbf{B}GL(n) }$and so the syntax for $\mathbf{orth} \in \mathbf{H}_{/\mathbf{B}GL(n)}$ is

$D^n : \mathbf{B}GL(n) \vdash (GL(n)/O(n))(D^n) : Type \,.$Next we need to determine $\mathbf{B} \mathbf{Aut}(T \Sigma) \in \mathbf{H}_{/\mathbf{B}GL(n)}$.

Observe that if $Type \in \mathbf{H}$ is the small object classifier of $\mathbf{H}$, then for any $X \in \mathbf{H}$ the projection

$\array{ Type \times X \\ \downarrow \\ X }$is the small object classifier in $\mathbf{H}_{/X}$. To see this notice that slice types over $e : E \to X$ are obtained by the pullback (all our diagrams are in $\mathbf{H}$)

$\array{ H &&\to&& \widehat{Type} \times X \\ \downarrow &&\swArrow&& \downarrow \\ E &&\stackrel{(\vdash H , e)}{\to}&& Type \times X \\ & {}_{\mathllap{e}}\searrow &\swArrow& \swarrow \\ && X } \,.$Hence in our case

$\array{ \Sigma &&\to&& \widehat{Type} \times \mathbf{B}GL(n) \\ {}^{\mathllap{}}\downarrow &&\swArrow&& \downarrow \\ \mathbf{B}GL(n) &&\stackrel{(\vdash \Sigma, id)}{\to}&& Type \times \mathbf{B}GL(n) \\ & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow \\ && \mathbf{B}GL(n) } \,.$This allows us to determine $\mathbf{B} \mathbf{Aut}(T \Sigma) \in \mathbf{H}_{/\mathbf{B}GL(n)}$. For the delooping of the automorphism group of an object is the image factorization of its name. This image factorization for the name of $T \Sigma$ in the slice is the factorization in the second column from the right in

$\array{ T \Sigma &\to& \Sigma &\to& (T \Sigma \sslash \mathbf{Aut}(T\Sigma)) \times \mathbf{B}GL(n) &\to& \widehat{Type} \times \mathbf{B}GL(n) \\ \downarrow && {}^{\mathllap{}}\downarrow && \downarrow&& \downarrow \\ * &\to& \mathbf{B}GL(n) &\stackrel{}{\to}& \mathbf{B}\mathbf{Aut}(T \Sigma) \times \mathbf{B}GL(n) &\to& Type \times \mathbf{B}GL(n) \\ && & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow \\ && && \mathbf{B}GL(n) } \,,$where each square and hence each rectangle is a pullback.

the internal hom in the slice now is semantically

$\array{ \mathbf{Aut}(T \Sigma)\backslash\backslash[T \Sigma, GL(n)\sslash O(n)] \sslash GL(n) \\ \downarrow \\ \mathbf{B}\mathbf{Aut}(T \Sigma) \times \mathbf{B}GL(n) }$So now

$\vdash \prod_{D^n : \mathbf{B}\mathbf{Aut}(D^n)} \sum_{T \Sigma : \mathbf{B} \mathbf{Aut}(T \Sigma)} \vdash T \Sigma \to GL(n)/O(n) : Type$is seen to reduce to a familiar statement in words:

a vielbein = metric is a reduction of the structure group of the frame bundle exhibited by a $GL(n)$-equivariant map $T \Sigma \to GL(n)/O(n)$ and two such metrics are to be equivalent if they are related by a diffeo.

]]>@Eric: Probably missing fonts. I’m on a borrowed computer now and am seeing several boxes, although at least mine are helpfully filled with Unicode numbers so I can look them up!

]]>It is likely just my iPhone, but the symbol for action groupoid is coming out like a square.

]]>It seems to take me a bit to converge to the optimal way of expressing myself here. But now I have finally made more explicit, at *general covariance*, that for the example of Einstein gravity, the generally covariant configuration space is in full beauty in type theory syntax:

and more background on reading this expressin is now at *infinity-action – Notions in representation theory*

Just for the record, since I mentioned it above: I now had a chance to turn these notes into something more coherent: *Erlangen2012 (schreiber)*.

So the first one has a canonical $\mathbf{B}^{n-1}\mathbb{G}$-connection on it (trvially so), the second one does not. But the second one is the actual quantomorphism group.

]]>No need to apologise. And don’t wear yourself out!

So $\sum_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$…

Do you mean

]]>So $\product_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$… ?

Right, I should have said this

(And I am sorry for spreading confusion that contradicts the whole point of what I myself just said a few entries before, I shouldn’t post in certain states of tiredness and travelling and certainly not when both coincide, sorry. I ran out of my lecture yesterday, biked to the train station, jumped on the night train to Erlangen. Was a good bit exhausted. Somehow my fingers started typing (out of habit, I suppose) but my brain hadn’t caught up yet. )

So $\sum_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$ is a differential refinement of the action groupoid of

invertible maps $\nabla \to \nabla$ from the prequantum $n$-bundle to itself that need

*not*respect either the connection or the principal structureby the conjugation action of these by $\mathbf{B}^{n-1} \mathbb{G}$.

And that this carries a canonical $\mathbb{G}$-$n$-connection is actually not surprising.

I have begun last night to create notes on related topics for the talk of mine that I gave this morning just a few minutes back. I ran out of steam at 3:30 last night, this is how far I got so far:

Will be further working on that now.

]]>So, after #10, what changes in #9 now we know it’s product not sum we need?

]]>Hm, sorry, I seem to have dependent sum and dependent product mixed up in the above.

Let’s see, the quantomorphism $n$-group is characterized by having $U$-probes for $U \in \mathbf{H}$ given by

$\mathbf{H}(U, \mathbf{QuantMor}_\nabla) = \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}}( U \times X, X )_\simeq \,,$hence the $U$-families of prequantum $n$-bundle auto-equivalences. This is

$\begin{aligned} \cdots & \simeq \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}} \left( \left( \left(\mathbf{B}^n \mathbb{G}_{conn}\right)^* U \right) \times \nabla, \nabla \right)_\simeq \\ & \simeq \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}}\left( \left(\mathbf{B}^n\mathbb{G}_{conn}\right)^* U, [\nabla,\nabla]_\simeq \right) \\ & \simeq \mathbf{H}( U, \prod_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla,\nabla]_\simeq ) \end{aligned}$and so Mr. Yoneda says that

$\mathbf{QuantMor}_\nabla \simeq \prod_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$instead of dependent sum.

]]>There are more internal homs in $\infty$-slices that are of interest in physics – and for some of them the fact that homotopy type theory automatically makes them live in the slice again seems to yield previously unknown or at least un-evident structures.

For instance, in cohesive homotopy type theory, if $\nabla : X \to \mathbf{B}^n \mathbb{G}_{conn}$ is a differential $n$-cocycle regarded as a prequantum n-bundle on $X$, then the totaö space of the subobject of the internal hom on the invertible endomorphisms

$\mathbf{QuantMor}(\nabla) \coloneqq \sum_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla, \nabla]_{\simeq} \simeq \exp(\mathfrak{poisson}_{F_\nabla})$is the corresponding quantomorphism $n$-group, the cohesive $n$-group that Lie integrates the Poisson bracket Lie $n$-algebra $\mathfrak{poisson}_{F_\nabla}$.

Now homotopy type theory says, trivially, that $[X,X]_\simeq$ itself is in context $\mathbf{B}^n \mathbb{G}_{conn}$.

But this tautological spatement now means:

There is a canonical $\mathbb{G}$-principal $n$-bundle with connection on the quantomorphism $n$-group $\mathbf{QuantMor}(\nabla)$.

This is somewhat curious. I am not aware that this has been noticed before in the literature, for $n = 1$. The most sophisticated discssion of the quantomorphism group that I am aware of (listed at quantomorphism group) struggles to get to the point that it establishes a smooth structure on the group in the first place (which is another thing that homotopy type theory gives for free). I am not aware that anyone did anything nontrivial with this smooth structure, such as constructing a connection over it. (But if anyone here knows more, I’d be most grateful for a pointer.)

So that’s a little exercise: understand what homotopy type theory is teaching us here about prequantum physics.

]]>Oh, now I see what you mean.

Okay, I have removed the first $[\Sigma, \mathbf{Fields}]$.

So I am trying to explain something starting from its naive incarnation and then successively refining it. I should just use fewer technical expressions for the “naive” version, which only serves as instance for how *not* to proceed anyway.

On the other hand, you are right with your last suggestion: The punchline of the whole entry is that if you know what $(\Sigma \to \mathbf{Fields})$ means then if you only interpret it “in context $\mathbf{B}\mathbf{Aut}(\Sigma)$” then it is $[\Sigma, \mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma)$, whereas if you falsely interpret it in global context, then it is just the naive $[\Sigma, \mathbf{Fields}]$. But this I can’t really say at that point of the introduction yet, I guess.

]]>Oh, so should it be

]]>here, the configuration space $(\Sigma \to Fields)$ of physical fields over a smooth manifold $\Sigma$ is not quite the space of Riemannian metrics on $\Sigma$ itself, but is the quotient $[\Sigma,Fields]/Diff(\Sigma)$ of this space…

That was the minor point. The slightly more major point was that in

here, the configuration space $[\Sigma,Fields]$ of physical fields over a smooth manifold $\Sigma$ is not quite the space of Riemannian metrics on $\Sigma$ itself, but is the quotient $[\Sigma,Fields]/Diff(\Sigma)$ of this space…

it seems to say

]]>$[\Sigma,Fields]$ is $[\Sigma,Fields]/Diff(\Sigma)$

Woops. Thanks for catching that!

You can tell that I kept changing my mind as to which symbol to use. I have turned those $X$s in paragaraph 3 and 6 now into $\Sigma$s. Thanks.

]]>Paragraph 3 seems to say “the configuration space blah is not quite … but is blah/Diff”. And presumably all $X$s should be $\Sigma$s, and in paragraph 6.

]]>I have further tried to prettyfy the notation at *general covariance*, in particular concerning the type-theoretic syntax.

It’s kind of neat:

we are entirely entitled to write $\Sigma \sslash \mathbf{Aut}(\Sigma)$ as a dependent type over $\mathbf{B}\mathbf{Aut}(\Sigma)$ simply as

$\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma : Type$and we are similarly entirely entitled to write the $\mathbf{Fields}$-moduli object equipped with the tivial $\mathbf{Aut}(\Sigma)$-action as

$\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \mathbf{Fields} : Type \,.$The end result is then that the configuration space of *generally covariant* fields on $\Sigma$ is formed entirely as we’d do naively for non-covariant fields. namely simply $\mathbf{Conf} \coloneqq : \Sigma \to \mathbf{Fields}$, only that now we do it in the $\mathbf{B}\mathbf{Aut}(\Sigma)$-context to get

It’s tautological. And that’s beautiful: the theorem is that if you unwind the categorical semantics of this type in the smooth model, then it is the correct answer: the Lie integration of the BRST complex of gravity with diffemorphism ghosts over $\Sigma$.

]]>