# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeApr 6th 2015
• (edited Apr 6th 2015)

This week I am at a workshop in Bristol titled Applying homotopy type theory to physics, funded by James Ladyman’s “Homotopy Type Theory project”. David Corfield is also here. The program does not seem to be available publically, but among the other speakers that the $n$Lab community knows is also Jamie Vicary.

Myself, I will give a survey talk titled “Modern physics formalized in Modal homotopy type theory” (which maybe should rather have “to be formalized” in the title, depending on how formal you take formal to be). I am preparing expanded notes to go with this talk, which I am keeping at

This is still a bit rough at some points, but that’s how it goes.

I currently also have a copy of the core of this material in one section at Science of Logic, replacing the puny previous section on formalization that was there. While it’s not puny anymore, now maybe it’s too long and should be split off. But just for the time being I’ll keep it there.

If you look at it, you’ll recognize a few points that I tried to discuss here lately, more or less successfully. This here is not meant to force more discussion about this – we may all be happier with leaving it as it is – it’s just to announce edits, in case anyone watching the RecentlyRevised charts is wondering.

• CommentRowNumber2.
• CommentAuthorDavidRoberts
• CommentTimeApr 7th 2015

I fixed some typos.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeApr 7th 2015

Thanks!!

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeApr 9th 2015

I was wondering whether the way $Loc_{\mathbb{R}}$ appears by the magic of aufhebung argues against $p$-adic physics, but then remembered that MO question you posed. But I guess what you talk about there comes later in the story.

• CommentRowNumber5.
• CommentAuthorNikolajK
• CommentTimeApr 13th 2015
• (edited Apr 13th 2015)

http://i.imgur.com/YsRgKgH.png

That looks odd to me.

It also happens to me that I see a definition where \mathcal or something might be missing, but I’m not 100% sure if it’s not just a new term. Should I comment in the entry directly (not gonna make a comment like this every time).

Or here,

http://i.imgur.com/5D1Q3vY.png

there are a bunch of term (names) and I guess some should overlap or in fact exactly not overlap, but I can’t make reasonable edit.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeApr 13th 2015

Thanks for pointing out where you feel something is at odds!

If you feel certain how to fix an evident typo, then doing so right away in the entry will be appreciated. In case of doubt, it doesn’t hurt to ask for feedback here first. In any case, it’s good to announce edits here.

this is indeed meant as is, thought certainly I agree that this side-remark may be too terse to make much sense to many readers. What is going on there is that every map of types $f \colon X \to Y$ translates to a $Y$-dependent type, which may be thought of as being the preimages $f^{-1}(y)$ depending on $y \colon Y$. Precisely if $f$ is a monomorphism is this resulting dependent type a mere proposition (namely the proposition which in words reads: “is in the image of $f$”).

Regarding your second png: here I am not sure if I understand what you are pointing to. Could you say it in more detail?

By the way, one alternative option for pointing to precise paragraphs in an nLab entry is to prefix the paragraph with a

  {#label}


and then link to it from here via

ncatlab.org/nlab/show/page+name#label

Then following the link shows the intended paragraph highlighted by gray shading.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeApr 13th 2015

I have now added also a bit of genuine content in the last section, Gravity.

After a bit of distraction, I’ll now be focusing on this again, this is the story of higher parameterized WZW terms that I left off a while back.

I still need to lay out the full story regarding solutions of sugra here more clearly. Maybe the next thing I should do is write out more precisely how underlying the étale 3-stack spacetime locally modeled on the supergravity Lie 3-group there is an ordinary spacetime locally modeled on its 0-truncation, $\mathbb{R}^{10,1\vert \mathbf{32}}$.

• CommentRowNumber8.
• CommentAuthorNikolajK
• CommentTimeApr 14th 2015
• (edited Apr 14th 2015)

The reversed turnstyle is not familiar to me, and if it’s read as in logic (alla $\Gamma\vdash\alpha$ and $\alpha,\Psi\vdash\vartheta$ let’s you write $\Gamma,\Psi\vdash\vartheta$ (cut elimination)), then I’d expect not $f^{-1}(a)$ but a whole judgement with $:$. It might be related to adjunctions, but you have no category lingua before.

In the second pic you write. $c:X\to BG$. Apart from $c$ being a term of type $C$ in the bottom left as well, I the diagram below has $B$ and $E$ into $BG$ and I don’t know if it’s related. The $X$ doesn’t pop up below that point.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeApr 14th 2015
• (edited Apr 14th 2015)

Now I see what you mean! These were typos. I have fixed them now. Thanks.

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeApr 15th 2015
• (edited Apr 15th 2015)

I am beginning to see how to narrow in the argument about the appearance of Lorentzian structure more.

Given a WZW term $\mathbf{L}_{WZW}^V\colon V \to \mathbf{B}^{p+1}\mathbb{G}_{conn}$ I used to demand of a definite globalization of it over a $V$-manifold $X$ only that it be a term $\mathbf{L}_{WZW}^X \colon X \to \mathbf{B}^{p+1}\mathbb{G}_{conn}$ which suitably restricts to $\mathbf{L}_{WZW}^V$ on the tangent spaces, which are equivalent to the infinitesimal disk $\mathbb{D}^V \to V$ in $V$.

But the WZW term, being constructed as a differentially twisted looping of a group cocycle $\mathbf{c} \colon \mathbf{B}V \longrightarrow \mathbf{B}^{p+2}\mathbb{G}$ carries more structure than just the bare map $\mathbf{L}_{WZW}^V$; that group cocycle itself is manifestly part of the structure that induces this map.

Hence it makes sense to demand that a definite globalization of the WZW term is something stronger, namely that it also comes with a definite globalization of that group cocycle itself.

For that to make sense, we need in the first place that the tangent bundle lifts from being a $\mathbb{D}^V$-fiber bundle to being a $\mathbf{B}\mathbb{D}^V$ fiber bundle, hence a Giraud $\mathbb{D}^V$-gerbe.

But also, since we are talking about a group cocycle and since $Grp(\mathbf{H}) \simeq \mathbf{H}^{\ast/}_{\geq 1}$, we should not generalize too much and demand this $\mathbf{B}\mathbb{D}^V$-fiber bundle to have structure group $\mathbf{Aut}^{\ast/}(\mathbf{B}\mathbb{D}^V)\simeq \mathbf{Aut}_{Grp}(\mathbb{D}^V)$ instead of all of $\mathbf{Aut}(\mathbf{B}\mathbb{D}^V)$.

That makes good sense, doesn’t it.

But this then gives the condition that the structure group of the frame bundle stabilizes both the group/Lie algebra structure on $\mathbb{R}^{d-1,1\vert N}$ as well as the 3-cocycle on there. And so this then constrains it to be (a higher extension of) the Lorentz Spin group.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeApr 15th 2015

Yes, I think that’s it, should have thought of this earlier. A WZW term is a limiting cone over a certain big diagram (p. 399 in dcct pdf) and so in globalizing it one should ask to globalize that whole diagram. In its top part this means globalizing the Lie algebra cocycle, in the bottom part this means lifting to group structure and globalizing the group cocycle. Even the fact that this is to happen while sliced under the point is implied then.

• CommentRowNumber12.
• CommentAuthorDavid_Corfield
• CommentTimeApr 22nd 2015

There are no non-trivial judgements with (a delooping of) $\mathbb{R}$ as the subject and (a delooping of) $\mathbb{R}^{0|1}$ as the predicate. But there turn out to be some exceptional judgements with subject $\mathbb{R}^{0|q}$ and predicate $\mathbf{B}^d \mathbb{R}$.

Could there be non-trivial judgements with (deloopings of) $\mathbb{R}^{0|1}$ as both the subject and the predicate?

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeApr 22nd 2015

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeApr 23rd 2015
• (edited Apr 23rd 2015)

Regarding the localization issue and $\mathbb{R}^{0|1}$: I had myself oscillating between localization and co-localization, and then I got myself mixed up. Thanks to Dave Carchedi for catching this. If anything then it is the co-localization at $\mathbb{R}^{0|1}$ that is of relevance, and it should be equivalent to the bosonic modality $\rightsquigarrow$.

Since for supermanifolds $X$ then $Hom(X,\mathbb{R}^{0|1}) = C^\infty(X)_{odd}$, even-graded $X$ are $\mathbb{R}^{0|1}$-colocal.