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 9 of 9
Here is an archetypical case of putting two entirely different-looking things in a common context and observing that there they are congruent. My question below will be: has any aspect of this been considered before? does this resonate with anyone?
So as you will have seen, over at Type-semantics for quantization (schreiber) I am considering what will be the categorical semantics of linear homotopy type theory (once Mike publishes the syntax :-) and observing that there is a rather neat, rather natural and rather powerful formalization of integral kernels and of quantization formalized in there.
Now, that formalization crucially involves pull-push in generalized cohomology, which in terms of linear homotopy type theory is context-extension followed by dependent sum/dependent product through spans
$\array{ && A \\ & {}^{\mathllap{h}}\swarrow && \searrow^{\mathrlap{g}} \\ C && && C } \,,$hence is the operation $\sum_g h^\ast$ on $C$-dependent linear homotopy types.
(Side remark: this pull-push is not yet the quantization process itself, in particular it is not pull push of quantum states. Rather, it is the pull-push of the cohomological twists hence of the linear bundles of which the quantum states are sections. The quantum states themselves are pull-pushed, once a certain datum is given, using a notion of “fundamental class” or “measure” that is naturally defineable in linear homotopy type theory.)
Now, one point of re-formulating physics in terms of homotopy type theory is that, while equivalent (via computational trinitarianism), the change in perspective is sometimes useful for seeing things that are otherwise hard to see.
What do we see here in pull-push of generalized cohomology through the eyes of linear homotopy type theory? Answer: we see linear dependent W-types. Right?
(Side remark 1: The above pull-push is the endofunctor that defines the W-type. The W-type itself will be something like the space of all states on wich this “quantum propagator” acts. I need to think about how to say this properly.)
(Side remark 2: of course dependent W-types involve in addition to context extension along $h$ and dependent sum along $g$ also dependent product along some $f$. But we can either think of the above as the case where $f = id$, or we observe that if we restrict attention to dualizable linear types then linear dependent sum and dependent product are dual by linear deMorgan duality anyway and so it makes not much of a difference either way.)
That’s the little observation. Does this resonate with anyone? Is there a discussion of “linear W-types” anywhere?
Finally, since it is late at night here, maybe I may close with a speculative followup-observation: ordinary W-types encode trees and the operation of sticking trees together along matching notes. Linear W-types as above can encode, among other things, quantum propagation. Together these two statements would seem to suggest that quantum propagation is related to collections of trees and all ways of gluing them together. But, this is, at least roughly, a familiar statement, this makes us think of Feynman diagrams, right. (I have no idea right now if this is more than a wild coincidence. But maybe something worthwhile to think about in some quiet moment…)
Over on g+ Mike rightly points out that above I am only talking about the endofunctor whose initial algebra would be the W-type, not the W-type itself yet.
Forwarding my reply from there:
here is one natural way in which co-algebras for the pull-push endofunctor do appear in this context, looking at around def. 4.9 in my note:
the endofunctor in the present notation is g_! h^*. An integral kernel in the discussion there is a map g_! g^* A2 –> g_! h^* A1. Moreover, a fundamental class is a map A2 tau –> g_! h^* A2 . The “densitized integral kernel” is the composite of the two.
This is all a bit more general than traditionally considered for W-types, but if we consider the special case that the twist (tau) and the dependencies (to make g_! h^* actually an endofunctor) are trivial, then that “desitized integral kernel” is a co-algebra for the endofunctor.
I still need to think about what the terminal such “densitized integral kernel” would be.
Yes, what I said last would relate to co-W-types aka M-types. Either way, I have to see what these would be in the linear setting and what their natural role for the application I am looking at would be.
There are some evident guesses, but I need to look into it more.
One article I have found which mentions inductive types in the context of linear logic, but I am not sure if it is of any help here:
Stéphane Gimenez, “Towards Generic Inductive Constructions in Systems of Nets” (pdf)
Here is a simple observation:
linear algebras/W-types of a pull-push operation as considered above are closely related to co-monadic descent, as fairly manifest from the little discussion at Sweedler coring – Comonadic descent.
Re #6, is there something related to the tangent category happening there, and then beyond all that to stuff I never understood 4 years ago here?
These things connect to each other, but right now it’s about something different.
So “linear homotopy type theory” is effectively what in higher/derived algebraic geometric is the theory of modules, coherent modules, quasicoherent modules, namely stable monoidal $\infty$-categories that can be pushed and pulled around in a good way.
Now given such, we can then ask what structures exist in such a context. And I guess interpreted logically, the usual story of comonadic descent for such structures translates into something related to inductive types.
This needs a bit more thinking, I suppose we are not dealing with free monads here but with what would give genuine “linear HIT”s.
I need to take care of some other things now, hope to be able to come back to this a little later today (tonight).
So maybe the suggestion that the initial/terminal algebras here are interesting is a dead-end.
I suppose another way to say what I actually tried to say above is just that “In linear dependent type theory a dependent linear polynomial functor is essentially an integral transform.”
1 to 9 of 9