# 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
• CommentTimeJan 5th 2013
• (edited Jan 5th 2013)

I am back to working on geometry of physics. I’ll be out-sourcing new paragraphs there to their own $n$Lab entries as much as possible (because the length of the page makes saving and hence previewing it take many minutes, so I need to work in smaller sub-entries and then copy-and-paste).

In this context I now started an entry prequantum field theory. To be further expanded.

This comes with a table of related concepts extended prequantum field theory - table:

extended prequantum field theory

$0 \leq k \leq n$ transgression to dimension $k$
$0$ extended Lagrangian, universal characteristic map
$k$ (off-shell) prequantum (n-k)-bundle
$n-1$ (off-shell) prequantum circle bundle
$n$ action functional = prequantum 0-bundle
• CommentRowNumber2.
• CommentAuthorTodd_Trimble
• CommentTimeJan 5th 2013

Great!! I’m looking forward to reading, and there’s a good chance I’ll be asking naive questions.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeApr 27th 2013
• (edited Apr 27th 2013)

Next week I’ll be giving a lecture series on Higher Chern-Simons theory in Pittsburgh at this workshop. I am starting now to type some lecture notes into the entry prequantum field theory (later to be merged into geometry of physics).

Tonight I started with the first part, which is

But I am not done yet. So don’t look at it yet (unless you feel like joining in with editing and fine-tuning…).

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeApr 27th 2013
• (edited Apr 27th 2013)

There is now an intro-section

prompted by David C.’s question in another thread.

• CommentRowNumber5.
• CommentAuthorjim_stasheff
• CommentTimeApr 27th 2013
I may have skimmed too quickly, but I see only spaces of fields without any idea of what a field IS. Of course physicists don't need to know.
• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeApr 27th 2013
• (edited Apr 27th 2013)

This is the definition which is announced as the central definition in the entry.

For more discussion of what a physical field is, see field (physics).

• CommentRowNumber7.
• CommentAuthorjim_stasheff
• CommentTimeApr 28th 2013
Thanks - especially for the parag about field bundles

now how do I cite this as a refernce?
• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeApr 29th 2013

You could cite that specific nLab page as

field (physics), $n$Lab entry (ncatlab.org/nlab/show/field+(physics))

Since this has been written as part of a more comprehensive set of lecture notes, you could also cite as

geometry of physics, II.2) Fields, $n$Lab entry (ncatlab.org/nlab/show/geometry+of+physics#PHYSICS)

Since I wrote the article on fields for a lecture series that I gave in Singapore in January, you could also cite it as such:

Urs Schreiber, Higher Chern-Simons theory, lecture series at Workshop on Topological Aspects of Quantum Field Theories, Singapore (14 - 18 Jan 2013) lecture notes available at geometry of physics, II.2) Fields, nLab entry (ncatlab.org/nlab/show/geometry+of+physics#PHYSICS

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeMay 4th 2013

I have been further working on the entry prequantum field theory. Now the section

is converging, I think. Apart from a little polishing and expanding here and there, maybe the only thing really missing is a picture of some caps and cups and spheres and saddles, where they appear as spans. Not sure how I should do that…

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeMay 6th 2013
• (edited May 6th 2013)

I have been adding a good bit more stuff to prequantum field theory and to geometry of physics. But I need to do some last touches on the new material for it to be really consumable in at least quasi-linear fashion. I’ll try to do that tomorrow. Then I’ll announce the material here in more detail.

(This here just as information for those of you who are scanning the RecentlyRevised page and are wondering…)

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeMay 10th 2013

There is now a new section prequantum field theory – Higher Chern-Simons local prequantum field theory.

That means to be an exposition of how we find higher Chern-Simons type prequantum field theories as precisely the boundary field theories of an pretty canonical thing which I started calling the “universal higher Yang-Mills theory” (this draws on joint discussion with Domenico Fiorenza and Alessandro Valentino, as linked to there).

Currently this covers roughly the material that I brought to the board in lectures in Pittsburgh last week. I had wanted to polish the writeup further and provide more of the picture. But for the moment I am out of steam and out of time, it seems.

(The material in prequantum field theory makes a section at geometry of physics.)

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeOct 16th 2015

I am writing a more comprehensive exposition of prequantum field theory, born out of joint work with Igor Khavkine. A series of small expositional chapters is now on PhysicsForums:

I have included these links also in the $n$Lab entry prequantum field theory now.

• CommentRowNumber13.
• CommentAuthorNikolajK
• CommentTimeOct 16th 2015

The definition in supermanifold seems to leave it open what the “dimension p|q” really denotes. The p gets lost.

In the first physics forum article, I think I’ve spotted the type spacial for spatial, and how the word “excitation” is used here is a little open to me.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeOct 16th 2015

Thanks!

I have briefly edited at supermanifold, have fixed the spatial typo, and have first replaced “excitation” with “configuration” and then decided to remove that half-sentence altogether for the moment. Because saying this properly really needs an entry in its own right, explaining the story at vortex atoms – Similarity to concepts of moder particle physics

• CommentRowNumber15.
• CommentAuthorNikolajK
• CommentTimeOct 16th 2015

Is there a formalized notion of moving between models of the (modal homotopy) type theory, which would then amount to switching between different physical theories/different scales?

• CommentRowNumber16.
• CommentAuthorUrs
• CommentTimeOct 16th 2015
• (edited Oct 16th 2015)

The ambient model of the modal homotopy theory fixes the general nature of geometric objects, for instance whether there is fermionic geometry or not, but once this is fixed, then different physical theories which might be effective at different scales would be to be found all within that one modal homotopy theory.

• CommentRowNumber17.
• CommentAuthorDavidRoberts
• CommentTimeOct 16th 2015

This is a really great series, Urs. Is it going to turn into a single document/article at some point?

• CommentRowNumber18.
• CommentAuthorUrs
• CommentTimeOct 17th 2015

Parts of this will go into my contribution to New Spaces in Mathematics and Physics.

• CommentRowNumber19.
• CommentAuthorDavid_Corfield
• CommentTimeOct 17th 2015

As I’ve said elsewhere, I find something curious about this ’prequantum’ idea. Seemingly, we have a (historical) story where we pass from the classical realm to the quantum realm. There were some cookbook recipes for doing this. A useful check makes us take the classical limit of a quantum theory. But something is missing. There’s more to the quantum realm than that which is deformed classical.

So in the new story, we think that already the classical was pointing to something beyond itself towards a full global coherent setting. We call this the prequantum. And this is doubly good because the axioms for the quantum allowed far more in than we needed, and it seems that the good quantum is that which comes from the prequantum.

most (or maybe all?) quantum field theories of interest in actual physics (as opposed to as devices of pure mathematics) are not random models of these axioms, but do arise under a process called quantization from a (local/extended) Lagrangian, hence from an action functional, defined on a configuration space of quantum fields, or else arise as holographic duals of quantum field theories that arise by quantization.

Then looking back at the classical we see further signs that the prequantum was already in the classical:

But in the context of higher geometry and higher geometric quantization this prequantization step is already part of the data of the Lagrangian itself:

Ok, so could we run history in a more rational fashion, where we arrive at the prequantum more directly (and so give it a better name)?

In your diagram showing $Prequantum \to Full quantum$ and $Prequantum \to Classical$, is there an arrow back from $Full quantum \to Prequantum$, so that we can see how taking the classical limit factors through it and ’disregarding global information’?

• CommentRowNumber20.
• CommentAuthorUrs
• CommentTimeOct 17th 2015

where we arrive at the prequantum more directly

That’s indeed what the formulation in cohesive homotopy theory does. In that context saying “Lagrangian” already comes out not as “horizontal $p+1$-form” but as “Euler-Lagrange $p$-gerbe”. That will be the punchline of the series, once it gets to the abstract formulation: prequantum geometry is geometry in differential cohesive homotopy theory.

(and so give it a better name)?

While maybe not the best name, it the closest to an established name that there is. Together with “quantomorphism” and “diffeology” it is part of the terminology that originates with Soriau, who was the one to first see the need for all this clearly.

• CommentRowNumber21.
• CommentAuthorUrs
• CommentTimeOct 17th 2015
• (edited Oct 17th 2015)

is there an arrow back from $Full quantum \to Prequantum$

I doubt that this will exist. But to say this with certainty, first the other map “$Prequantum \to FullQuantum$” needs to be understood completely. I know the impatience that you are feeling, after all, this impatience has been in the whole field for decades, but here my whole point is that before we rush to formalizing higher quantization, we need to be careful about what its correct domain really is. One step after the other.

To my mind, the prequantum story is now sorted out satisfactorily. When I am done with writing it up, the next task is to go back to the “motivic” quantization process via pull-push in twisted generalized cohomology and figure out how to properly extend it to full codimension (presently I only know it up to codimension 2). Then once this is really understood, we should be able to properly answer questions such as to which extent a quantum theory remembers the prequantum theory that it came from.

• CommentRowNumber22.
• CommentAuthorDavid_Corfield
• CommentTimeOct 18th 2015

Oh I guess that takes us back to our dualities in physics discussions. Then of course we wouldn’t expect an arrow back.

• CommentRowNumber23.
• CommentAuthorUrs
• CommentTimeOct 19th 2015

Yes, exactly.

On the other hand there is of course there is a long tradition to speak of forming the “classical limit” of a quantum theory. But in speaking so, one tacitly assumes that one starts not from a single quantum theory, but from a family of them, parameterized by some $\hbar$, for which a limit may be taken. This is of course much more information. Moreover, for genuine non-perturbative quantum theories, even that situation is more subtle than often appreciated, since $1/\hbar$ will be quantized itself.

• CommentRowNumber24.
• CommentAuthorUrs
• CommentTimeOct 22nd 2015

Here is the next exposition in the series

I have added a pointer to this at gauge field

• CommentRowNumber25.
• CommentAuthorUrs
• CommentTimeOct 26th 2015
• (edited Oct 26th 2015)

Here is the next one

I have added a pointer to this at higher gauge theory.

• CommentRowNumber26.
• CommentAuthorUrs
• CommentTimeOct 28th 2015
• (edited Oct 28th 2015)

And here the second-but-last in the series

• CommentRowNumber27.
• CommentAuthorUrs
• CommentTimeNov 1st 2015

And here the last one:

• CommentRowNumber28.
• CommentAuthorUrs
• CommentTimeNov 3rd 2015

• CommentRowNumber29.
• CommentAuthorDavid_Corfield
• CommentTimeNov 3rd 2015

I’ll copy here typo from Physics Forums as it’s still there in new document:

“The bouquet which emanates form these…” should be FROM. (p. 45 in this document)

And question:

Have you seen any other interesting bouquets? What would happen in the complex analytic world? I see there is some gauge theoretic interest in complex analytic superspaces, $mathbb{C}^{p|q}$, such as p. 12 of http://arxiv.org/abs/1507.03048.

• CommentRowNumber30.
• CommentAuthorDavid_Corfield
• CommentTimeNov 3rd 2015

P. 43 there is

$\mathbf{B}^{p+1}(\mathbb{R}/\mathbb{R}).$
• CommentRowNumber31.
• CommentAuthorUrs
• CommentTimeNov 3rd 2015

David,

sorry, I had entirely missed you PF comment. Somehow I didn’t receive an alert for it. I did now react there.

Thanks for catching typos! All fixed now.

• CommentRowNumber32.
• CommentAuthorDavid_Corfield
• CommentTimeNov 4th 2015

It seems easier to converse over here.

superstring perturbation theory in principle is all about complex analytic supergeometry, due to it being all about super Riemann surfaces.

Is there any suggestion of a larger role for the complex analytic, maybe a nonperturbative one?

Is there any pattern to appearances of the complex analytic in physics? Alongside the perturbation theory via super Riemann surfaces you mention and the obvious case of superposition, there is conformal field theory, twistor string theory, Kähler manifold, analytically continued Chern-Simons theory, holomorphic Chern-Simons theory, generalized complex geometry, analytically continued Wess-Zumino-Witten theory, …

Does any of this complex analytic physics simply arise from your

abstract differential cohomology in cohesive homotopy theory combined with the abstract manifold theory and abstract PDE theory of differential cohesive homotopy theory

interpreted in the complex analytic world?

• CommentRowNumber33.
• CommentAuthorUrs
• CommentTimeNov 4th 2015

Yes, so for instance homolomorphic/analytically continued (and super, if you wish) Chern-Simons theory should just be Chern-Simons theory in the complex analytic $\infty$-topos (hence same for complex WZW etc.)

But it gets more interesting there, and I don’t fully understand it yet. Namely by the discussion here it is known that the Chern-Simons 2-gerbe on $\mathbf{B}G$ does not exist, when $G$ is complex reductive, as a holomorphic 2-gerbe. So complex analytic CS theory, when extended down to the point at least, must have coefficients in a generalized differential cohomology theory, not just in plain differential cohomology.

As also indicated at the above link, there are various hints as to what it should be: it should be complex algebraic K-theory $\mathbf{K}$ instead.

Indeed that seems to make sense, we get a morphism of stacks

$\mathbf{B}G \longrightarrow \mathbf{K}$

from the datum of a $G$-representation, and that is just the datum to be specified for specifying the CS Lagrangian.

Then the more ordinary differential form version of the complex analytic CS Lagrangian should be obtained by applying the Beilinson regulator, as a morphism of spectra, to this, to get

$\mathbf{B}G \stackrel{\mathbf{L}_{CS}}{\longrightarrow} \mathbf{K} \stackrel{\mathbf{r}^{Bei}}{\longrightarrow} \mathbf{H} \,,$

(where the regulated coefficient $\mathbf{H}$ is whatever it is, some sheaf of spectra built out of mixed Hodge complexes, etc.).

Again, this matches expectations: complex analytic CS on hyperbolic 3-manifolds is supposed to give their “complex volume” and that in turn is equivalently given by the Borel regulator (see at Bloch group).

So I think this will be roughly the story of prequantum complex analytic CS theory in complex analytic cohesion. But as you see from the above ingredients, unwinding it gets a bit more involved. Also more interesting, of course.

• CommentRowNumber34.
• CommentAuthorDavidRoberts
• CommentTimeNov 4th 2015
• (edited Nov 4th 2015)

known that the Chern-Simons 2-gerbe on BG does not exist, when G is complex reductive, as a holomorphic 2-gerbe.

No, in fact it does exist, and I think Brylinski-McLaughlin discuss this in their two-part paper. We even diacussed this in Edinburgh! Because G is reductive, it is Stein, and so topological and holomorphic cohomology coincide. The basic gerbe on G exists holomorphically by Brylinski’s preprint, and it is multiplicative by pairing Steinness with Konrad’s paper.

The CS 2-gerbe is not an algebraic gerbe over the related algebraic reductive group, since the relevant etale cohomology group is torsion. I am of the opinion, though, that there should be an algebraically-inspired cohomology theory where it does exist: we just haven’t found it yet. Log-stacks are close, but I don’t think quite right. But Deligne-Beilinson cohomology (in the holomorphic case) definitely uses the log-structure on G to get at some of this.

• CommentRowNumber35.
• CommentAuthorDavid_Corfield
• CommentTimeNov 4th 2015

More typos:

abstracty; furhter

“prop. 3.18 that the integration axiom”,

missing a word, perhaps ’states’?

• CommentRowNumber36.
• CommentAuthorUrs
• CommentTimeNov 4th 2015

@David Roberts,

ah, true, thanks for reminding me, that’s embarrassing for me. Did you leave any notes anywhere on this issue?

I am too busy right this moment with getting something else out of the way, but I do want to get back to the complex analytic story, for various reasons. Thanks to you and David C. for prodding me.

$\,$

@David Corfield,

thanks! Fixed now.

• CommentRowNumber37.
• CommentAuthorDavidRoberts
• CommentTimeNov 4th 2015
• (edited Nov 4th 2015)

I don’t think I did. I was semi planning to write a paper on this with Ray Vozzo, to get the connection version at least over $SL_n$ (or even $SL_2$, since we wanted to be quite explicit!)), but I’m not sure we have enough to go on.

• CommentRowNumber38.
• CommentAuthorDavid_Corfield
• CommentTimeNov 5th 2015

Did you leave any notes anywhere on this issue?

You and David R. left a small trail on the nForum here in discussion with Frédéric Paugam.

• CommentRowNumber39.
• CommentAuthorDavid_Corfield
• CommentTimeNov 5th 2015
• (edited Nov 5th 2015)

Typos:

“Regarding such $L$ for a moment … we may apply the de Rham differential $L$ to it.” (p. 6)

and

$L : U_i \to \Omega^p + 1_H$ (p.7)

and

field theoried

• CommentRowNumber40.
• CommentAuthorUrs
• CommentTimeNov 6th 2015

Thanks! Fixed now.

As you may have seen already, I also have talk slides now (pdf).

• CommentRowNumber41.
• CommentAuthorDavid_Corfield
• CommentTimeNov 6th 2015
• (edited Nov 6th 2015)

In the preprint, presumably Proposition 3.34, (1) should say $T^{\infty}_{\Sigma} E$ rather than $T^{\infty}_{\Sigma} \Sigma$.

Then in the slides, slide 6, the Eilenberg-Moore category shouldn’t mention $E$: $EM(J^{\infty}_{\Sigma} E)$.

Is there a result along the lines that all of $PDE_{\Sigma}$ can be recovered as the kernel of $EL$ for some $L$? If not, which part of $PDE_{\Sigma}$? And what of two Lagrangians that give the same EL-equations?

• CommentRowNumber42.
• CommentAuthorUrs
• CommentTimeNov 6th 2015
• (edited Nov 6th 2015)

In the preprint, presumably Proposition 3.34, (1) should say $T^{\infty}_{\Sigma} E$ rather than $T^{\infty}_{\Sigma} \Sigma$.

Ah, no, this is actually a $\Sigma$ on purpose. $T^\infty_\Sigma \Sigma$ is the formal disk bundle of $\Sigma$, but for general bundles $E$ over $\Sigma$ instead $T^\infty_\Sigma E$ is the pullback of $E$ to the formal disk bundle of $\Sigma$. Since that general thing does not seem to have been considered much, the text only mentions the special case that admits comparison to traditional literature.

Then in the slides, slide 6, the Eilenberg-Moore category shouldn’t mention $E$: $EM(J^{\infty}_{\Sigma} E)$.

Thanks! Fixed now.

Is there a result along the lines that all of $PDE_{\Sigma}$ can be recovered as the kernel of $EL$ for some $L$? If not, which part of $PDE_{\Sigma}$? And what of two Lagrangians that give the same EL-equations?

That’s exactly the question that Helmholtz asked and answered, way back. The modern incarnation of his result is the Euler-Lagrange complex. Its local exactness says that a PDE given by vanishing of a $(p+1,1)$ vertical form $\alpha$ is locally variational, hence is locally of the form $ker(EL)$, precisely if the “Helmholtz form” $\delta_V \alpha$ vanishes.

• CommentRowNumber43.
• CommentAuthorDavid_Corfield
• CommentTimeNov 8th 2015

Can we return to that question of whether, with hindsight, the classical physicists of the nineteenth century glimpsed something of this prequantum physics? Put it another way if we could go back and give them your super-slick prequantum geometry, and they understood it, are there some phenomena they could now deal with?

Is there anything they could have done with supergeometry? Clearly a problem for almost all time was the stability of matter. Is it really only after quantization that supergeometry, in the guise of Pauli exclusion, can explain it?

• CommentRowNumber44.
• CommentAuthorUrs
• CommentTimeNov 10th 2015

Is it really only after quantization that supergeometry, in the guise of Pauli exclusion, can explain it?

That’s a good question. Pauli exclusion is there already for classical spin fields, due to their supergeometric nature. Whether this already gives stability of matter is maybe more subtle, as to have matter in the sense one needs here one needs bound states of fields (protons,neutrons, etc.) and it seems unlikely that this would exist classically. Though these bound states are a notorious subtle issue.

(Thanks to Igor Khavkine, who I had a quick exchange with regarding this question.)

• CommentRowNumber45.
• CommentAuthorDavid_Corfield
• CommentTimeNov 10th 2015

Thoughts about the stability of matter would make for an intriguing history.

Supposedly Niels Bohr said:

My starting point (for the development of the Bohr model) was not at all the idea that an atom is a small-scale planetary system and as such governed by the laws of astronomy. I never took things as literally as that. My starting point was rather the stability of matter, a pure miracle when considered from the standpoint of classical physics.

I wonder about the extent to which nineteenth century physicists were troubled by it. There was some sense of near completeness, such as Michelson in 1894:

… it seems probable that most of the grand underlying principles have been firmly established … An eminent physicist remarked that the future truths of physical science are to be looked for in the sixth place of decimals.

(There’s debate about whether this referred to Kelvin.) Odd thing to say given how they couldn’t even explain the most basic property of matter.

• CommentRowNumber46.
• CommentAuthorUrs
• CommentTimeNov 10th 2015
• (edited Nov 10th 2015)

That quote by Bohr is a good example of the distinction that is necessary: the stability of the hydrogen atom is an effect not due to Pauli exclusion, but purely one of quantum ground states. It’s the stability of metals and Neutron stars that is governed by Pauli exclusion.

So it’s subtle. But I think the key point that you were after is true: classical spin fields could have been considered by classical physicists before quantum theory, and it would have revealed at least some effects that are usually attributed to quantum physics.

Odd thing to say given how they couldn’t even explain the most basic property of matter.

My impression is (I may be wrong) that they saw the existence of lumps of matter of various density as an a priori outside of physics. Much like these days we can’t explain the basic properties of fundamental particles, and it’s a heated debate whether physics has to explain these or has to just take them for granted.

• CommentRowNumber47.
• CommentAuthorDavid_Corfield
• CommentTimeNov 10th 2015

I thought I’d start a page then on stability of matter.

As to counterfactual history on what classical physics could have made of spin fields, that’s presumably a very difficult question.

• CommentRowNumber48.
• CommentAuthorUrs
• CommentTimeNov 10th 2015

As to counterfactual history on what classical physics could have made of spin fields,

If only they had listened to the Ausdehnungslehre, they could have made it.

• CommentRowNumber49.
• CommentAuthorUrs
• CommentTimeNov 10th 2015

Tomorrow I’ll be speaking at MPI Bonn in the Higher Diff Geometry Semniar on

• CommentRowNumber50.
• CommentAuthorDavid_Corfield
• CommentTimeNov 11th 2015

Did you not say somewhere that you though the shifted symplectic language could be put better in other terms? Is that why shifted symplectic structure is rather slight?

• CommentRowNumber51.
• CommentAuthorUrs
• CommentTimeNov 11th 2015

I am not a fan of the “shifted symplectic” terminology. But since it’s fashionable among people around me, I thought I’d take the opportunity to point out that, using different words, we have worked on this all along.

• CommentRowNumber52.
• CommentAuthorNikolajK
• CommentTimeDec 3rd 2015

I asked my high school teacher how to tackle the integral $\,\,\int\frac{d }{d x}\left(7x^2\cos(x)\right)\,d x\,\,$ and he just told me to shut up and watch this video.

• CommentRowNumber53.
• CommentAuthorNikolajK
• CommentTimeDec 10th 2015

What are the first concepts one could add to a language like ITT or even HOTT, that would spoil rich semantics of the language in a smooth $\infty$-topos. I.e. I ask what not to do, if one axiomizes a theory, if one wants to keep the possibility to do this kind of physics. In which way should the language not be restricted/overloaded?

• CommentRowNumber54.
• CommentAuthorUrs
• CommentTimeDec 10th 2015
• (edited Dec 10th 2015)

First of all various classicality axioms will break the synthetic theory. If the 0-types have choice, then no non-trivial topological or smooth structure will be possible anymore. If univalence is broken or otherwise truncation to 0-types is enforced, then all synthetic gauge theory (all differential cohomology) disappears. This is the reason, incidentally, why cohesive $\infty$-toposes behave very differently from cohesive 1-toposes. There is no comparable synthetic formalization of physics in cohesive 1-toposes.

• CommentRowNumber55.
• CommentAuthorNikolajK
• CommentTimeDec 10th 2015

Thank you. Mhm, well I don’t quite get what “a type has choice” means yet, and I mostly view univalence as ’something on the outside is represented by something on the inside’ and don’t quite know $\infty$-topoi necessarily need that for geometry … but I’ll keep my eyes open to connect the dots.

• CommentRowNumber56.
• CommentAuthorUrs
• CommentTimeDec 10th 2015

I mean the axiom of choice. The higher toposes are needed because otherwise there are no $\mathbf{B}G$s and hence no gauge theory.

• CommentRowNumber57.
• CommentAuthorNikolajK
• CommentTimeDec 11th 2015
• (edited Dec 11th 2015)

I know choice means the axiom of choice for the type but as HoTT sits on top of intuitionistic type theory, which as such proves choice (the Per-Martin Löf version I read the paper about) I don’t know what spoils choice on the types (which you welcome), so that losing it again would again spoil gauge theory :)

Regarding the second point, when you say there is no gauge theory you mean there is no gauge theory internal to the theory, right? Otherise I’d think you can do lots of type theory with topoi generally.

• CommentRowNumber58.
• CommentAuthorUrs
• CommentTimeDec 11th 2015

Nikolaj, I am not sure anymore what we are discussing. Could you try to restate what your question is? I think the points I mentioned above are self-evident, but you seem to be mixed up, and so maybe you are after something else than I thought you were.

• CommentRowNumber59.
• CommentAuthorNikolajK
• CommentTimeDec 11th 2015

You helped me so far - I’ll come back to it once I have the vocabulary to express a question. Urs.