Not signed in (Sign In)

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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 nnLab 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


    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 9th 2015

    I was wondering whether the way Loc Loc_{\mathbb{R}} appears by the magic of aufhebung argues against pp-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)

    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,

    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.

    Regarding your first png:

    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:XYf \colon X \to Y translates to a YY-dependent type, which may be thought of as being the preimages f 1(y)f^{-1}(y) depending on y:Yy \colon Y. Precisely if ff is a monomorphism is this resulting dependent type a mere proposition (namely the proposition which in words reads: “is in the image of ff”).

    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


    and then link to it from here via

    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, 10,1|32\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)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:XBGc:X\to BG. Apart from cc being a term of type CC in the bottom left as well, I the diagram below has BB and EE into BGBG and I don’t know if it’s related. The XX 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 L WZW V:VB p+1𝔾 conn\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 VV-manifold XX only that it be a term L WZW X:XB p+1𝔾 conn\mathbf{L}_{WZW}^X \colon X \to \mathbf{B}^{p+1}\mathbb{G}_{conn} which suitably restricts to L WZW V\mathbf{L}_{WZW}^V on the tangent spaces, which are equivalent to the infinitesimal disk 𝔻 VV\mathbb{D}^V \to V in VV.

    But the WZW term, being constructed as a differentially twisted looping of a group cocycle c:BVB p+2𝔾\mathbf{c} \colon \mathbf{B}V \longrightarrow \mathbf{B}^{p+2}\mathbb{G} carries more structure than just the bare map L WZW V\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 𝔻 V\mathbb{D}^V-fiber bundle to being a B𝔻 V\mathbf{B}\mathbb{D}^V fiber bundle, hence a Giraud 𝔻 V\mathbb{D}^V-gerbe.

    But also, since we are talking about a group cocycle and since Grp(H)H 1 */Grp(\mathbf{H}) \simeq \mathbf{H}^{\ast/}_{\geq 1}, we should not generalize too much and demand this B𝔻 V\mathbf{B}\mathbb{D}^V-fiber bundle to have structure group Aut */(B𝔻 V)Aut Grp(𝔻 V)\mathbf{Aut}^{\ast/}(\mathbf{B}\mathbb{D}^V)\simeq \mathbf{Aut}_{Grp}(\mathbb{D}^V) instead of all of Aut(B𝔻 V)\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 d1,1|N\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) 0|1\mathbb{R}^{0|1} as the predicate. But there turn out to be some exceptional judgements with subject 0|q\mathbb{R}^{0|q} and predicate B d\mathbf{B}^d \mathbb{R}.

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

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeApr 22nd 2015

    Hm, that’s a good question. I haven’t thought about this yet…

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

    Regarding the localization issue and 0|1\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 0|1\mathbb{R}^{0|1} that is of relevance, and it should be equivalent to the bosonic modality \rightsquigarrow.

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

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)