Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeJan 9th 2014
   • (edited Jan 9th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHere 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 _[[schreiber:Type-semantics for quantization]]_ 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](http://ncatlab.org/nlab/show/W-type#DependentWTypesCategoricalSemantics). 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...)

   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…)

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJan 9th 2014
   • (edited Jan 9th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOver 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 [[schreiber:Type-semantics for quantization|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.

   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.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 9th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexProbably a daft question, but if you're talking about co-algebras, why not [[M-types]] rather than [[W-types]]?

   Probably a daft question, but if you’re talking about co-algebras, why not M-types rather than W-types?

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 9th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexOf course, there's a substantial literature relating coalgebra to state spaces on which operators act, as in the introductory [text](http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf) by Bart Jacobs -- _Introduction to Coalgebra. Towards Mathematics of States and Observations_. Abramsky explored coalgebras and quantum mechanics [here](http://arxiv.org/abs/0910.3959).

   Of course, there’s a substantial literature relating coalgebra to state spaces on which operators act, as in the introductory text by Bart Jacobs – Introduction to Coalgebra. Towards Mathematics of States and Observations. Abramsky explored coalgebras and quantum mechanics here.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeJan 9th 2014
   • (edited Jan 9th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexYes, 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](http://www.imn.htwk-leipzig.de/WST2013/papers/paper_16.pdf))

   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)

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeJan 9th 2014
   • (edited Jan 9th 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHere 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](http://ncatlab.org/nlab/show/Sweedler+coring#ComonadicDescent)_.

   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.

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 9th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexRe #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](http://golem.ph.utexas.edu/category/2010/01/quasicoherent_stacks.html)?

   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?

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeJan 9th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexThese 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).

   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).

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeJan 10th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexSo 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]]."

   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.”