Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 50 of 50
Just an observation which I should have made more explicit earlier, elsewhere (did I not? maybe I didn’t):
given a abelian group object of the kind in an -topos , then there is the “tensor topos”-structure on the slice (given by first forming the cartesian product in and then using addition in ) which is the one that characterizes objects of the slice as “local Lagrangians” in the sense of Local prequantum field theory (schreiber), as recently highlighted again in Rune Haugeng’s arXiv:1409.0837.
But now under the identification of objects in with -line bundles, this tensor-topos tensor product is of course the “external tensor product” in the sense of indexed monoidal categories.
I just came to think of this again when discussing with David Corfield how the statement of the cobordism hypothesis ought to have a purely “internal logic” formulation in terms of higher “linear negation” (linear duality).
Hmm, some variant of HoTT which involves indexed monoidal categories. Where’s Mike?
Well we already know what that variant ought to be (“informally”) it is the linear homotopy type theory we had discussed. I just had not made use of the external tensor product yet. Or rather I had, but in a dual incarnation and not calling it by that name.
Maybe to be more explicit:
in “Local prequantum field theory (schreiber)” there is the tensor product on the slice -topos given by
Under passing from these classifying maps to the -line bundles which they classify, then this is the “external tensor product”.
Not a big deal, but above I felt like mentioning it.
In terms of internal linear homotopy-type theory the cobordism-hypothesis formulation of local prequantum field theory boils down to something like “there are higher order linear-negation-via-relations operations with respect to the external tensor product on the linear homotopy type theory which may be thought of as paramaterized by homotopy types of framed manifolds”. Specifically the higher order such duality operation associated with a closed manifold is the internal incarnation of the theta-line bundle construction over the moduli stack of flat fields on that manifold. That’s how there is a Langlands-like assignment of zeta functions to local systems in the “logical foundations”.
I don’t understand the quantum stuff, but what you say about the external product looks right.
Is there a standard name for this basic type of construction? In 1-category theory, given a monoid in a monoidal category , we form a new monoidal category . This construction recurs frequently but I don’t know the name of it.
I never saw a name for it, but let me just recall that we talked about this before when we all wrote the entry monoidal topos. Some people would say “tensor topos”, but in either case of course that’s more a name for the outcome than for the specific construction.
But maybe we should invent a name. At least in the situation as above when the slice tensor product is equivalently an “external tensor product” on linear dependent types, then I think this is a construction of fundamental relevance.
Well, we might just adopt the term “external tensor product”. It is “external” in that it does not happen in a single slice of the “linear hyperdoctrine” but pairs different slices. On the other hand “external” invokes many other associations which are not as appropriate. Not sure.
How about “slice monoidal category”? It’s the oplax limit of an arrow in the 2-category , with regarded as a lax monoidal functor out of 1.
That suggestion seems about as good as any to me.
To my mind, the whole point here is that there is already a canonical cartesian monoidal structure on the slice, and that one needs instead a term to make clear that one refers not to this one, but to the other one. At least in the cases of relevance in this thread so far, saying “slice monoidal structure” would run into just the problem that needs to be avoided.
Maybe one could try “phase tensor product” or “phased cartesian product”, in line with John Baez’s old suggestion of speaking of “phased sets” for the kinds of slices in question here. That’s certainly a very descriptive term for the particular application of the tensor product as in the thread above, because that’s exactly what is happening: the tensor product adds up phases of action functionals on cartesian products of field spaces.
What kinds of names are used in pure mathematical instances of this summation?
as a slight aside but related to Todd’s comment in #6 and Urs’s comment in #10, the article external tensor product gives a definition in terms of a cartesian monoidal base, but I believe it makes sense in general to speak of the external tensor product in situations (such as a domain (bi)fibration ) where the base is not necessarily cartesian. This allows one to (sometimes) define an “internal” tensor product on the fiber over either as a pullback of the external tensor product along a comonoidal structure on , or as a pushforward of the external tensor product along a monoidal structure on (e.g., the latter recovers the Day convolution product in the case of presheaves).
@David, re #11: as I said in #7, it seems to me that there is no established term for this… except that in homotopy theory and with suitable coefficients, then it is equivalent to what is known as the external tensor product.
I didn’t mean an establish general abstract term. I was just wondering about a particular appearance of that structure in, say, arithmetic, if some kind of phase addition had been found there. Is there ever consideration of an external tensor in some ?
On the one hand of course people all the time pull back two bundles to a common base space and tensor them there. This is an elementary operation that non-category theorist will hardly bother to give a name to. For instance this is used when one extracts the formal group from a complex-oriented cohomology theory and in tons of other places.
In the general-abstract context which we are discussing the operation is mentioned in remark 3.2.3 of Lurie’s “Classification of TFTs”. Again there is no special name given to it.
Also, I think giving this a name is the least interesting aspect of what this thread started with ;-) So I’ll just declare hereby that it be called the phased product from now on.
I don’t understand what is wrong with “slice monoidal structure”. You start with a monoidal category and then there is an induced monoidal structure on for a monoid . Of course there is also a cartesian monoidal structure (if E has pullbacks) but that’s true for any monoidal category that happens to have cartesian products, and it doesn’t usually cause any problems.
It’s not wrong, it just won’t work well for my purpose. Sorry for getting into debates on terminology, it’s not so important.
To get back to the discussion that I had tried to start in #1:
so my feeling is that by putting ourselves into a context of linear homotopy type theory and then pondering dualizability with respect to the external tensor product, then we will find an internal incarnation of much of the content of the cobordism hypothesis for coefficients in -fold phased correspondences, i.e. what externally is .
Namely under the translation between the phased tensor product and the external tensor product highlighted in #1 above, then the statement is that the right concept for duality for the external tensor product is via pullback along the diagonal.
I am talking about the fact that the unit/counit for the duality of the phased tensor product in is the correspondence
and its reverse, respectively. Translated to the external tensor product this says that for considering unit/counit of one is to pull back along the diagonal and then use the unit/counit of the fiberwise (the “internal”) tensor product.
So in a way we discover the need to consider correspondences as above in order to express duality for the external tensor product of a linear homotopy type theory.
But then once we are at this point, we discover that these correspondences have their own higher duals and so forth, and so we discover higher correspondences from the external tensor product of a linear homotpy type theory.
Then finally we notice that this in turn implies that there is induced by the external tensor product actually a higher order duality which gives many higher order duality/unit/counit-operations parameterized by homotopy types of suitable manifolds.
In some sense we recover an internal persepective of the cobordism hypothesis with coefficients in from pondering just the internal linear homotopy type theory language of , it seems to me.
Does anyone see what i am trying to get at? I am still struggling a bit with saying it very clearly, in fact I am trying to sharpen my thoughts about this by talking about it.
Let’s not get distracted by terminology, as we were above. There is something really interesting to be found here, it seems to me. Would be nice to eventually extract it.
Not really sure what you’re after. Is it that just as there’s a way of passing between internal and external perspectives in the case of a simple form of duality, so there should be such a translation for higher forms? And then, since the external perspective is easier to grasp in the case of these higher dualities, so it should be possible to use them to derive the internal perspective?
Not really sure what you’re after.
Okay, thanks for the feedback. Then allow me to try to say it better:
Remember how recently in another thread we highlighted how some super-sophisticated looking modern concepts become very simple and “naive” once regarded in the internal logic of an infinity-topos.
Here the idea is to apply this to the cobordism hypothesis. Externally it looks like a huge machine whose setting up first requires defining (infinity,n)-categories, then symmetric monoidal (infinity,n)-categories, then those with all adjoints, then those with all duals, then monoidal (infinity,n)-functors and then the statement of the theorem only begins. It seems intractable to ever implement this in homotopy type theory in any useful way. But at the same time, the cobordism hypothesis clearly expresses something very fundamental about (directed) homotopy theory.
But consider the special case where the coefficient -category is for some infinity-topos . Then the statement of the cobordism hypothesis becomes a simpler looking – or at least more natural looking – statement internal to , or rather internal to the linear homotopy type theory of . It takes a form that one could more easily imagine to become part of the very axiomatics of linear homotopy type theory, i.e. a form that reduces it more to concepts of “pure linear logic”.
Namely we observe that in the linear homotopy type theory of we have not just all those tensor products (linear conjucntion) in the linear type theories over each type . But we also have that “global” tensor product which is sometimes known as the “external tensor product” (with the “external” here having no relation to the previous external/internal distinction, unfortunately) but which one might also call the “phased tensor product”.
But taken at face value, the phased tensor product which takes an -line over and an -line over to the -line over has very few ordinary dualizable objects. Naively every dualizable object over needs to have .
But then we notice that if we just relax the concept of unit and counit a little (to “relational” units/counits) then every -line over every becomes dualizable with respect to the phased tensor product.
And once we are at this point, we notice that this opens up a whole new universe of duality which just comes to us: namely we find (all by just studying linear homotopy type theory) that
the relational units/counits of the phased tensor product are themselves dual to each other, via higher order relational units/counits and so ever on ad infinitum;
this tower of higher order dualities of the phased tensor product is such that it allows a system of higher order trace operations that are parameterized by homotopy types of manifolds.
and indeed, one finds that the looped -lines obtained by the higher order trace on some over some which is labeled by a manifold is a “theta line” obtained by transgression of .
All this just from looking at linear homotopy type theory in a purely logical fashion. Study of linear homotopy type theory would eventually lead to these considerations even if one had never heard of the cobordism hypothesis.
Internally in the internal homotopy logic of , the statement of the cobordism hypothesis is the statement that a certain global linear conjunction in the linear homotopy logic of naturally comes with a higher dimensional system of concepts of linear duality where higher dimenisional linear traces are labeled by homtopy types of manifolds.
higher dimensional linear traces are labeled by homotopy types of manifolds
Is something of this visible in the diagrams appearing in Mike’s work with Kate Ponto, Duality and traces for indexed monoidal categories?
The end of this blog message by Mike raises the issue of dualizability of linear types dependent on nonlinear types. We see the unit and counit.
Hmm, not sure I got the point of the warning of the final paragraph.
re #21:
I suppose something like full dualizability in the sense of the cobordism hypothesis, with the higher concepts of trace that full dualizability induces, may be going on in Ponto-Shulman, but I don’t really have extracted it in much detail. Mike may have more to say.
What I could point out is the following: the construction of theorem 5.2 in Ponto-Shulman 12 looks under the translation wich I have been emplyiong here as follows:
so I consider the linear homotopy type theory of -line bundles. Then for this case the kind of bicategory in that theory 5.2 is the one which in terms of looks as follows: objects are types equipped with the trivial -2-line bundle
morphisms are correspondences over between these whose tip is the product
and composition is compositon of correspondences followed by integrating out the middle factor.
In view of this I suppose it is likely that one of the bicategorical traces in Ponto-Shulman is structurally essentially the trace induced via the cobordism hypothesis in which is labeled by the 2-sphere . But I haven’t checked in detail.
(I could write this for more general cases than I am displaying here, but I am already spending much time typesetting the diagrams that I do display…).
re #22:
Not sure, but I suppose in that comment at the end Mike is alluding to the fact that it needs an actual 2-category (bicategory) of spans equipped with linear types depending on the span tips to do what they do in Ponto-Shulman, and that it is not clear what the corresponding 2-categorical (“directed”) linear homotopy type theory would be.
If so, then this is related what I am trying to get at here (in a fresh attempt at making myself understandable in #20 above):
for linear dependent type theories such as those which are the internal language of (for an -ring object in ), then what matters of the corresponding -categorical version, which would be the internal language of equipped with the phased tensor product, is the higher trace structure induced via the cobordism hypothesis on each of its objects. For describing this it seems that one does not need or even want what would be the full language of -directed linear homotopy type theory. One would just need and want a native language of these higher duality operations.
What I am trying to say here is a bit along the lines of Nils Baas’s “hyperstructures” idea: for describing how objects in a symmetric monoidal -category “bond”-together, the language of symmetric monoidal -category is actually fairly laborious, and one may rather want to find the direct “native language of bonding”.
For instance, to make it more explicit:
given any product of spheres, I know what the -shaped higher trace on any object in is, expressed as an iterative sequence of certain homotopy pullbacks in the -topos . To deduce this I use externally the theory of monoidal -categories and the cobordism hypothesis, but once I am done, I am reduced to a construction that has a natural description by natural operations in just the ordinary linear homotopy type theory of .
And so I envision that I forget about the route via monoidal -categories by which I arrive at these higher duality operations labeled by and just axiomatize these higher duality operations directly in the linear homotopy type theory.
For a product of spheres (e.g. a torus etc.) this is actually easily done. For more general I am not sure yet, but there ought to be a way.
Just to check, “correspondence” means “span”, right?
And means the -category of spans, spans-between-spans, etc.?
Yes, the (infinity,n)-category of correspondences.
What I keep referring to is essentially the content of pages 22-32 in the note
Re #25, are spheres straightforward because they’re composed of a cup and a cap? For other manifolds what’s needed - some generators and relations account?
Re #28, I guess that’s something odd in (infinity,n)-category of correspondences that the title has ’correspondences’ and then it’s ’spans’ all the way apart from a few ’correspondences’ in the middle. The policy at nLab is to treat them as completely synonymous, I take it. Wouldn’t it be better to settle on the preferred term then?
re 29:
I shouldn’t have mentioned restriction to spheres, it’s just that these are a particularly easy case of the manifold-shaped higher traces. On what is currently p. 27 of the note, the higher trace of shape the genus- surface for any is given.
(Thanks to Domenico Fiorenza for discussion of this and the rest of this document.)
Similar handle-decomposition formulas for manifold-shaped higher traces will exist in all dimensions, but of course as one climbs up it gets harder and harder to name them all.
re #30: thanks, I have fixed that now by switching consistently to one choice.
We had this discussion on terminology before. I won’t insist on either and I know that Mike has emphasized his preference for “span” before. But at some point it struck me that for such a fundamental concept with this important foundational role in type theory (generalized relations) the word “span” seems unfortunate in its focus on naming a choice of notation instead of a concept. From then on I liked “correspondence” much better, and still do. But it’s just terminology and not really important. I won’t insist on one way or the other.
A quick revisit to check on levels of understanding (I can report that they are improving) found these typos:
enocde; univseral; pre-qauntized; univresal; by by; woth; the the; idenitfied
Thanks, David! These fixed now.
I have worked this morning on improving the relevant sections 3.2.1 and 3.2.2 of that lpQFT file. Should be a bit better now.
Talking of TQFTs and defects, there was an MO question you might care to answer.
Regarding check on levels of understanding:
let me know what your picture is by now, that will help me to further adjust what I may say about it.
So in summary, the point is that when we are in a homotopy type theory in the context of an “abelian type” , then for every (stably framed) manifold there is a higher dimensional trace operation on (identity morphisms on) any type in this context. If is closed of dimension , then is a type dependent on . If has a boundary then is a correspondence from to .
What exactly these higher duality/higher trace operations are is – with present technology – deduced via the proof of the cobordism hypothesis in monoidal -category theory. But the resulting operations are natural operations entirely within just the homotopy type theory of and might have a native axiomatization in there. Certainly for of dimension and this axiomatization is easily written down. For I suppose one may still write down a lot. For high it is unclear to me if there may be an axiomatization that is simpler than the full machinery of the proof of the cobordism hypothesis. (Except for simple cases of s such as higher dimensional spheres ) But maybe once one gets serious about looking at these higher dualities/higher traces from the internal point of view of the homotopy type theory, this will open up new insights as to how to proceed here.
Specifically, in situations such as for an -ring object in , then all this may naturally be formulated in terms of the linear homotopy type theory and the “external tensor product”.
What I find striking is that the higher dualities/higher traces certainly are “just there” once one starts considering HoTT in the context of an abelian group object . It’s not something external and contrived, in some way it should be part of the natice language of a future version of HoTT. It’s part of the foundations of homotopy theory, I’d think. You we don’t need a fully fledged “directed homotopy theory” to formalize it, at least not for large classes of examples of .
This is a bit as with Nils Baas’s idea of “hyperstructures”: the idea there is that if one focuses on -categories with duals, then the full theory of monoidal -categories seems like overkill, as the topic of -categories with duals has a simple beauty of its own, for which all the directionality encoded in full -category theory seems more like a nuisance than a feature. What Nils Baas (and maybe David Ayala and Nick Rozenbylum) envision is a taylor-made theory of “hyperstructures” to deal natively with the case of -categories with duals, and this looks like it may have a good chance to have in turn a native logical formulation in (linear) homotopy type theory – as a theory of higher duals/higher traces.
My cautionary remarks about manifolds above are too cautionary. We may turn this around: for every -dependent type we have a tower of higher duality correspondences that is easily written down. Every possible way to compose these gives a higher dimensional trace operation.
We may need to invoke the cobordism hypothesis to deduce that each possible such way is characterized by the homotopy type of a stably framed manifold. But to just define the higher traces in the homotopy type theory one does not need to know this. It’s a cool fact which implies that in some marvelous way homotopy types of manifolds may be found in pure logic, of sorts, but to just define the higher dimensional traces all we need is the tower of higher duality correspondences, which is easily specified.
That seems quite clear, though I don’t feel I see the overall picture well enough to guess what the natural next steps would be.
Funny how the drive to turn things into “pure logic” sounds rather like same motivating force as drove the likes of Frege and Peano, and then Russell wanting to remove the Kantian “synthetic” out of mathematics. Yet this feels rather different, perhaps as the rendering as “pure logic” here is not being taken in a reductive way.
Certainly “roof” names a notation, but I never thought of “span” as naming a notation. However we should probably not re-have that argument. (-:
Ok, after a lot of thought I’m starting to see what you’re getting at. I was thinking about a dependent linear type theory where there are two kinds of types, nonlinear and linear, with the linear ones possibly dependent on the nonlinear ones. That’s the internal language that corresponds directly to indexed monoidal categories, and in there you can formulate the relevant sort of dualities and traces we were interested in.
But in some cases, there may be a “nonlinear universe of linear types”, i.e. a nonlinear type which you’re calling such that for any nonlinear type , to give a linear type family dependent on is the same as to give a map . Then we can apply fibrant replacement and say that to give a nonlinear type together with a linear type family is the same as to give a nonlinear type dependent on . So an indexed monoidal category with a nonlinear universe of linear types can equivalently be described in terms of the ordinary nonlinear type theory dependent on .
For instance, the monoidal structure on the fibers of our indexed monoidal category is incarnated on the universe by a map . In terms of families and , the phased product would be
And in terms of types and , I think it would be
Does that seem right?
I don’t quite see what this has to do with the cobordism hypothesis yet. I see how that’s saying that the traces with respect to the notions of duality and higher duality that exist in a higher category of higher spans are encoded by manifolds. But I thought the monoidal structure on higher spans was cartesian, whereas on indexed monoidal categories the phased product is not generally cartesian.
I also don’t see yet how the traces Kate and I were studying could be a particular case of cobordism-hypothesis traces, because our dualities definitely are of the old familiar sort where the unit and counit are maps rather than spans. Or are you saying that if your unit and counit happen to be maps regarded as spans, then you might get out our traces as a particular case?
Thanks, Mike!
Does that seem right?
Yes, certainly.
But I should add that I wouldn’t expect that the existence of the -universe is really necessary. If one just mimics the formulas for the higher duals which one gets in the case that exists and applies them in general indexed monoidal categories with the “external tensor product” in place of the “phased tensor product”, then, I’d think, everything goes through just as well.
I don’t quite see what this has to do with the cobordism hypothesis yet.
The fact that all “phased types” are fully dualizable once we allow monoidal units and counits which are “relational” (are correspondences) means that the cobordism hypothesis implies that each of them defines a local TFT. My point here is to read the cobordism hypothesis equivalently as saying that a local TFT is really nothing but a system of such higher dimensional traces, and that on “phased types” these higher traces have a natural expression “native” to the type theory.
And the local TFTs that arise this way are precisely the “classical”/”pre-quantum” theories that are expected to yield the relevant quantum field theory by quantizing them via pull-push through these correspondences.
We want to place ourselves inside cohesive homotopy type theory and eventually talk about the full story of quantum field theory. To that end we need an internal perspective on that story. This is the perspective that I am after here. It looks like this:
Every phased type in cohesive HoTT is a local action functional. The local framed-topological pre-quantum theory it induces is nothing but the system of higher dimensional dualities/traces on it. (For -structured topological pre-quantum theory we need to choose in addition some -fixed point structure on the phased type. I am not sure yet how to express that in internal language, but it will be important to figure this out, for this will give the full structure on the theta-lines.)
And finally there is a last step which currently has some question marks to it, but which motivates all this: a local pre-quantum TFT as above is supposed to induce local topological quantum field theory by something like the linearization of these higher traces given by pull-push through the correspondences that exhibit these higher traces, the way I described in “Quantization via Linear homotopy types”.
But I thought the monoidal structure on higher spans was cartesian
Hm, the tensor product on which is induced objectwise by the cartesian product on is not cartesian as a tensor product on . The cartesian product on instead comes from the disjoint union in .
However, I know that you know this, so I must be misunderstanding what you mean above.
I also don’t see yet how the traces Kate and I were studying could be a particular case of cobordism-hypothesis traces,
I didn’t want to make any claim about this, I just tried to reply to David’s question whether there might be a relation. Since the bicategory that you construct from an indexed monoidal category with its “phased spans” as morphisms certainly has some resemblance to the structures relevant here, I wouldn’t be shocked if the 2-trace you consider turns out to be related. While I haven’t tried to wade through the algebra to check anything, I’d agree with David that it might be interesting to ponder this.
the tensor product on which is induced objectwise by the cartesian product on is not cartesian as a tensor product on .
Yes, of course, sorry. What I meant by “cartesian” is exactly that. In an indexed monoidal category, the tensor product on the fibers (hence also the external/phased tensor product) is not the cartesian monoidal structure even on the objects.
Yes, so the tensor product in is the degenerate case of the “external tensor product” where all the linear types are trivial (are the identity) and only the underlying Cartesian product remains. But for some purposes it is useful to speak of this degenerate case, in the context of field theory this is what encodes the fields themselves, before we add action functionals to them.
There is a forgetful monoidal functor
and lifting a local field theory through this
means equipping the fields with an action functional.
By the way, maybe I should say more explicitly what I mean when claiming that “all this” should go through for any external tensor product, whether exists or not.
What I mean is that the unit/counit correspondence for the phased tensor product
translates to the “relational unit/counit” of the external tensor product
and then the higher correspondences exhibiting all the higher duals of the phased tensor product similarly translate to “higher relational” higher units/counits of the external tensor product.
This becomes a bit tedious to type out here, though. But if it is unclear what I mean, I’ll do it.
Ok, so you’re saying that if you want to generalize the cobordism hypothesis from topological field theories to some fancier kind of field theory, then you need to extend the system of dualities in higher spans to talk about the phased product relative to some indexed monoidal category?
What I am trying to say (sorry for being so unclear) is that: given an indexed symmetric monoidal -category, then (I think)
there is a symmetric monoidal -category of -fold spans in the underlying cartesian monoidal -category equipped with linear data, with the same objects, and equipped with the external tensor product;
such that those objects in the indexed monoidal -category which were fully dualizable (for instance: invertible) in their fiber in the indexed monoidal category become fully dualizable in the monoidal -category with respect to the external tensor product.
So the objects in each case are pairs with non-linear and linear and dependent on .
The 1-morphisms in the -category between a are spans equipped with a morphism .
The 2-morphisms in the -category between 1-morphisms and are spans of spans equipped with a homotopy .
And so on.
The original objects for which has a full dual with respect to the monoidal structure in the slice over will be fully dualizable under the external tensor product in this -category, the full dual being .
The unit of this full dualizability structure on is the 1-morphisms given by the span and equipped with the unit in the slice over . The counit is given similarly, with the reversed span.
And so forth.
Ah, I see now finally! Thanks. What do you mean by “fully” dualizable in the fiber?
I think we need that the objects in the symmetric monoidal -categorical fibers are fully dualizable when regarding the fiber as a symmetric monoidal -category. But I suppose that actually means they must be invertible. (Which is fine.) So I suppose I should have just replaced that clause by speaking of objects invertible under .
Okay. That’s a bit disappointing to me, since most dualizable objects are not invertible. Also it’s too bad this doesn’t seem to see “total duality”.
This restriction corresponds to the condition that be an -group.
In the phased picture we may easily go beyond that restriction by allowing to be any symmetric monoidal -category itself, internal to the ambient -topos. This is the generality in that Rune Haugseng’s article is written.
In the picture of indexed monoidal categories, this would correspond to generalizing to indexed monoidal -categories. The construction which I indicated in #45 would still apply, now with homotopies between 1-morphisms generalized to 2-morphisms, and so on.
Spoke with Eric Finster today. It seems that his opetopic type theory produces (on top of a whole lot more) precisely the syntax for higher dimensional traces that I was envisioning here.
This is really neat. The vision of having a homotopy type theory with native higher dimensional traces via -fold correspondences, hence having fully formal synthetic local prequantum field theory, is getting close to reality here.
1 to 50 of 50