brushed up the first few lead-in sentences, cross-linking more with quantum probability.

]]>Urs, thanks. This is a natural idea. Of course, the two levels only show up once we go to AQFT. The use of DTT in topos theory is well-understood, but sometimes a bit hidden in the presentation.

Would you like to add something to the page?

BTW another place where these multi-layers show up recently is in our guarded cubical type theory. We are currently working on a version which brings this out even more clearly.

]]>How can one speak of being “measured simultaneously” in a spacetime region?

I used “simultaneous” not to refer to the time inside the spacetime, but to us discussing it. But in a sensible local net of observables for an actual quantum field theory, the spacetimes on which we evaluate are globally hyperbolic, meaning that they have a Cauchy surface, and the algebra of observables assigned to the spacetime is that to this spatial slice (or any one of them, up to isomorphism).

Re #6, is that what the discussion of the Cauchy problem contributes, that you have a time slice with which to define simultaneity?

Yes!

]]>Re #6, is that what the discussion of the Cauchy problem contributes, that you have a time slice with which to define simultaneity?

]]>Interesting! Multi-layer dependent type systems seem to be popping up all over the place these days. Cohesive type theory has crisp/cohesive contexts, simplicial and cubical type theory have a separate context of cubes/simplices and their faces, etc.

]]>How can one speak of being “measured simultaneously” in a spacetime region? Do you mean the observables commute? Does this need the kind of thing Joost Nuiten discusses about ’strong locality’ (p. 19 of his 2011)?

]]>I came back to thinking about Bohr toposes, now in the context of homotopical algebraic quantum field theory.

Where an ordinary Bohr topos is a topos internal to which we find a locale such that ordinary probability distributions on it are, externally, quantum states, so a higher Bohr topos should probably contain internally a 1-localic topos, hence just a topos, thought of as a classifying topos of a localic groupoid internal to the to the Bohr topos, where the morphisms in that localic groupoid would be the gauge transformations.

The ambient Bohr topos itself is, in the ordinary case, the presheaves on the category of “classical contexts”, namely of *types* of things that may be measured simultaneously without quantum uncertainty.

A topos internal to that is equivalently just a presheaf of toposes on that category of classical contexts, isn’t it?

This made me think the whole Bohr topos idea is maybe better formulated in the language of dependent type theory/hyperdoctrines. What’s really going on is a 2-layered system of dependent types:

each spacetime region is a

*context*(of things that may be measured in this region)for each of these contexts, there is a poset of

*classical context*(of those of these things that may be measured simultaneously)for each of those, finally, there is a topos whose lattice of subterminal objects is the propositions about these measurements.

So it’s something like a poset of spacetime regions, and fibered over this a category whose fibers are posets of classical contexts, and fibered over these in turn a category whose fibers are toposes whose internal logic is that reasoning about the possible measurements in these classical contexts over these spacetime regions.

]]>I gave the Idea-section at *Bohr topos* a more informal lead-in paragraph before the first subsection of the Idea section starts.

No, that’s good. Your comment showed that something I though had been made obvious in fact wasn’t. So I went back to the entry and noticed that it didn’t say this well. So I tried to improved it.

]]>Didn’t mean to give you extra work with my question on G+, Urs!

]]>expanded the section *Idea – In brief* at *Bohr topos* just a little bit, in order to amplify the relation to Jordan algebras better (which previously was a bit hidden in entry).