Just for the record:

with an insight from Joost Nuiten we finally found a neat way to at least organize the data of “consistent orientations in pull-push quantization” that made me start this thread here. There is a description now in section 7.3 of my notes.

It’s encoded as a lax natural transformation out of what is essentially that pull-push “monad-oid”/”polyad” that I was wondering about above (only that in the present form of the notes I don’t actually consider the monadic products yet). Hence I suppose this is, or would be, indeed an element of the “collage” of that, as Mike pointed out above in #5.

]]>Just a comment to myself, for completeness:

there is some kind of relation of the above also to relative monads and their Kleisli categories. It is now slowly dawning on me that Thorsten Altenkirch’s discussion of quantum computation in terms of (relative) monads is not so unrelated to the pull-push that I am looking at in “Type-semantics for quantization”. But I need to think more about it.

]]>@David: Yes. More generally, if $(x:A)\vdash (B(x):LType)$ is a dependent linear type (with $A$ nonlinear) and $\cdot \vdash (C:LType)$ is any non-dependent linear type, then we have

$\Big(\prod_{x:A} (B(x)\multimap C)\Big) = \Big(\sum_{x:A} B(x) \Big) \multimap C.$ ]]>Re #29, does this mean that linear dependent sum and linear dependent product are intertwined by weak duality?

Oh I see. It’s something like

$\product_{x:A}[B, I] \cong [\sum_{x:A} B, I].$ ]]>The linear type theory doesn’t sit inside the nonlinear type theory of the tangent category, not in a fully dependent way. For instance, the tensor product is not (as far as I know) a type-theoretic operation on the nonlinear type theory of the tangent category, because it doesn’t act in all contexts. If $(x:X)\vdash (A(x):Type)$ and $(x:X)\vdash (B(x):Type)$ are two dependent types therein, can you define $(x:X)\vdash (A(x)\otimes B(x):Type)$?

]]>I have added to *dependent linear type theory* in a new section *Properties – The canonical co-modality* a remark on what you (Mike) said above in #22, now that I see it in Ponto-Shulman12.

(But maybe we should rather discuss this further in the thread on dependent linear type theory…)

]]>Hm, while there is more dependence than a naive axiomatization might presuppose, it does decompose and the internal logic sees this: those homotopy types which are stable homotopy types are the linear ones. So the internal logic knows about stable homotopy types depending on stable homotopy types. Just that in general the dependence can also be more intrincate.

Of course you may want a specific axiomatization that does not allow this. I just thought since you were wondering about semantics this might be worth looking into. We already know that tangent homotopy type theory is relevant/has a good *raison d’être* and we see that it combines linear and non-linear dependent types, so it might be worth turning the question around and asking which syntaxt captures this kind of tangent semantics.

It would seem to me also to be desireable to embed linear type theory this way into ordinary type theory instead of making it branch off by itself, for it would mean that all the power of ordinary type theory can be used to analyze the linear type theory inside it.

No?

]]>In the internal logic of a tangent $\infty$-topos, *all* types are nonlinear. It’s only when you “decompose” that $\infty$-topos into an indexed monoidal category over the base $\infty$-topos that you see a bifurcation into linear and nonlinear.

Maybe you are thinking of iterating the tangent construction? I think then we would have three-sort contexts $\Gamma | \Theta | \Delta$ in which $\Gamma$ is nonlinear and both $\Theta$ and $\Delta$ are linear, and each context can depend on the context to the left, so you would have the linear types in $\Delta$ depending on the linear types in $\Theta$. That might be interesting to think about. But you still wouldn’t have linear types depending on linear types *of the same sort*, or nonlinear types depending on linear types, so I don’t yet see a “linear-over-linear” dependent sum that would have a meaningful first projection.

a term inhabiting a nonlinear type in a nonempty linear context, and the type theory I have in mind doesn’t allow such things — because I don’t know what they would mean semantically.

Consider a tangent $\infty$-topos. Its types are already in themselves linear types dependent on non-linear types in some way. Now go to the slices of that and find a semantics that has linear and non-linear types depend on linear and non-linear types.

At least this is so after one declares a monoidal product on the linear types depending on the non-linear types. But we know it exists, it’s the relative smash product of spectrum objects.

(I am wondering if maybe we can build for each $E_\infty$-ring $E$ an $E$-tangent $\infty$-topos whose objects are parameterized $E$-modules…)

]]>And if anyone figures out what Goodwillie is talking about, I’d love to hear it. (-:

]]>The dependent sum that I mentioned is definitely a positive type, and Urs is right that the “other pushforward” is a dependent product rather than a dependent sum. It’s an interesting question whether there is a negative linear dependent sum type! I don’t see what it would mean semantically in terms of indexed monoidal categories, or how to define it in this sort of dependent linear type theory. Note that the positive dependent sum I described above is only “half linear”: it is the sum of a family of *linear* types indexed over a *nonlinear* type, and it is itself a *linear* type. The “first projection”, which seems essential to make sense of a negative dependent sum, would therefore have to be a term inhabiting a nonlinear type in a nonempty linear context, and the type theory I have in mind doesn’t allow such things — because I don’t know what they would mean semantically. Maybe if we knew what it meant for a linear type to depend on *another* linear type, then we could make sense of both polarities of dependent sum.

Hmm, don’t we need the positive/negative polarity aspect to get at the full range of linear logic connectives? Multiplicative conjunction and additive disjunction are both positive types, while the additive conjunction and multiplicative disjunction are negative types. Wouldn’t we expect then two kinds of dependent sum as a kind of generalised product? Could it be that all the six operations without identification are needed?

About Goodwillie, for what it’s worth, the full abstract is

]]>Title: Geometric Language for the Functor/Function Analogy

Abstract: This talk is about a point of view. Functors TOP—SPECTRA that preserve weak homotopy equivalences may be considered as global functions on the variety TOP. We sketch a dictionary for this kind of geometry. Functors TOP/B—SPECTRA on the category of spaces over a fixed space B serve as functions in a neighborhood of the point B. The tangent space of TOP at B is the category of parametrized spectra over B. There are cotangent vectors, tensor fields both covariant and contravariant, and differential operators.

There are precisely two tangent connections, both flat, and their difference is the tensor field known as smash product of spectra. I cannot find differential forms (except 0-forms and 1-forms). This has not yet led to nontrivial theorems, but I will at least say something trivial about some nontrivial examples.

@Mike, thanks, I have added that to the references here.

@David, I am not the one to say anything about the negative/positive issue, but the two different push-forwards $f_!$ and $f_\ast$ correspond to the two different quantifiers: dependent sum and dependent product.

Concerning the last question: it would surprise me if that statement of Goodwillie were an example of a general theme instead of a peculiar property of spectra. But then, that whole statement is still pretty mysterious to me, so I might be entirely wrong.

]]>Is there a general theme about when linearizing, two things become separate and we’re interested in the difference? E.g., the Goodwillie claims I’ve mentioned before:

There are in some sense exactly two tangent connections on the category of spaces (or should we say on any model category?). Both are flat and torsion-free. There is a map between them, so it is meaningful to subtract them.

and

]]>their difference is the tensor ﬁeld known as smash product of spectra.

If, as I mentioned above, dependent sum type has:

One might expect that in “dependent linear type theory” the positive and negative dependent sums would become different. However, the meaning of the quoted phrase is unclear,

and, as Mike says,

the dependent sum of a family of linear types over a nonlinear type is one of the basic operations, which corresponds categorically to pushforward,

then are we seeing again a difference of two pushforwards of the kind Urs mentioned here?:

]]>Generally, six-operations Yoga is at its heart about characterizing how in the presence of two different pullbacks $f^!$, $f^\ast$ or in the presence of two different push-forwards $f_\ast$, $f_!$, one may differ from the other only by a composite of dualizing and tensoring with a correction factor

Yes, exactly.

I think the closest type-theoretic literature I’ve found to what I’m thinking of is this. There could very well be more out there that I haven’t found, though.

]]>Ah, now i understand: it exists, but only inside you at the moment. That’s good to know.

That construction you describe applied more generally to dependent linear homotopy types will be the generalized Thom spectrum construction (as here), I suppose.

]]>I haven’t written down anything about this yet. But #21 is exactly right. When you generalize from a nonlinear/linear monoidal adjunction to an indexed monoidal category, which corresponds to introducing dependency of linear types on nonlinear ones, the “linearization” operator becomes the functor $\Sigma = \pi_! \pi^*$ from the base category to the fiber over $\ast$ discussed on p595 of Duality and traces for indexed monoidal categories.

If we denote two-sorted contexts by $\Gamma | \Theta$, where $\Gamma$ is nonlinear and $\Theta$ is linear, then given a nonlinear type

$\cdot | \cdot \vdash A : Type$we have the unit linear type

$\cdot | \cdot \vdash I : LType$which we can base change to $A$:

$(x:A) | \cdot \vdash I : LType$and then take a dependent sum (the dependent sum of a family of linear types over a nonlinear type is one of the basic operations, which corresponds categorically to pushforward):

$\cdot | \cdot \vdash \Big(\sum_{(x:A)} I\Big) : LType.$ ]]>In

- Paul-André Melliès ,
*Categorial Semantics of Linear Logic*, in*Interactive models of computation and program behaviour*, Panoramas et synthèses 27, 2009 (pdf)

and

- Andrew Graham Barber, around p. 21 of
*Linear Type Theories, Semantics and Action Calculi*, 1997 (web, pdf)

the $!$-modality is interpreted as the comonad induced from a monoidal adjunction between a cartesian and the symmetric monoidal (star-autonomous) type system.

Viewed from the point of view of tangent $\infty$-toposes, maybe the canonical choice for the monoidal

$CartesianMonoidal \longrightarrow SymmetricMonoidal$would be the suspension functor $\Sigma^{\infty}$ from the base topos to its spectrum objects. (?)

]]>Mike, that sounds just like what I would like to see (a propos: a tangent $\infty$-topos is already a lot like this, only that one still needs to add the tensor product). Where is more on this written up, if anywhere?

]]>What happens when homotopy type theory meets linear logic?

The best way I’ve thought of so far to combine DTT with LTT is to have two classes of types, “linear” and “nonlinear”, where the nonlinear ones form an ordinary DTT and the linear types can depend on nonlinear types, but not on each other. There’s been some work on stuff like this from the type-theoretic side, but not I think a whole lot. Semantically, this models an indexed monoidal category (the linear types) over a cartesian base (the nonlinear ones).

]]>What happens when homotopy type theory meets linear logic? I see “linear type theory” has some hits. Even “linear dependent type theory” does.

The other way – “dependent linear type theory” – sends us to our own page dependent sum type:

One might expect that in “dependent linear type theory” the positive and negative dependent sums would become different. However, the meaning of the quoted phrase is unclear.

Also it seems to

]]>S.S. Ishtiaq and D. J. Pym. A relevant analysis of natural deduction. Journal of Logic and Computation, 8(6):809–838, 1998. (pdf).

Gr, somehow I keep thinking more about this issue here than about what I am supposed to be working on today.

Maybe to come back to David’s comment above, the thoughts that now keep haunting me go like this (copied from a post shared elsewhere):

*Grothendieck’s Yoga of Six-Operations and some Quantum Dependent Type Theory?*

Grothendieck had famously amplified that the mechanism of Verdier duality is formally captured by certain systems of adjoint pairs of functors – the “yoga of six operations”:

http://ncatlab.org/nlab/show/six+operations .

A clean analysis of these axioms and their consequences had been given by Peter May, who highlights that flavor of the axioms that he calls the “Wirthmüller context”:

http://ncatlab.org/nlab/show/Wirthmüller+context

A Wirthmüller context is simply this: an adjoint triple of functors between two closed monoidal categories such that the middle one is strong closed monoidal, hence such that *Frobenius reciprocity* holds:

http://ncatlab.org/nlab/show/Frobenius+reciprocity .

If in addition a Beck-Chevalley condition holds for consecutive such Wirthmüller morphisms

http://ncatlab.org/nlab/show/Beck-Chevalley+condition

then there is canonically induced an abstract calculus of integral transforms via integral kernels that captures a great deal of genuine quantum physics:

https://dl.dropboxusercontent.com/u/12630719/integral.pdf

notably it captures geometric quantization of symplectic manifolds, of Poisson manifolds, of Wilson loops, the quantization of strings, T-duality, D-brane charge,…, all via example 3.5 of the above note, which establishes the dictionary and then points you to

http://ncatlab.org/schreiber/show/master+thesis+Nuiten

for the details of the implementation.

But now for the special case that the monoidal categories in the Wirthmüller context are *cartesian* all this

triple of adjoint functors

the middle one is strong closed monoidal, hence satisfies Frobenius reciprocity

Beck-Chevalley condition holds

are Lawvere’s axioms on categorical logic

http://ncatlab.org/nlab/show/hyperdoctrine

The well behaved examples of this arise from base change of slice toposes. Indeed, given any topos, then its dependent type theory

http://ncatlab.org/nlab/show/dependent+type+theory

is a system of cartesian Wirthmüller six-operation contexts, the left adjoints being dependent sum, the middle functors being context extension, and the right adjoints being dependent products.

In other words: Grothendieck’s six operation yoga in Wirthmüller flavor is a non-cartesian variant of core aspects of dependent type theory.

In particular, if the closed monoidal categories here are “linear”, hence are “tensor categories”, then this is a “linear” or “quantum” analog of key ingredients in dependent type theory.

Does this resonate with anyone?

]]>Thanks for all the replies! I’ll briefly react to them here, but will have to postpone more detailed reactions until tomorrow.

@Mike: Thanks, good point, yes, maybe staying in $Cat$ is what I need. And, true, I ignored the twists so far when asking for the Kleisli category picture, for simplicity. I suppose I should throw them over to the other side of the morphisms anyway, I need to think more about this.

@Zoran, thanks for the pointer to Polishchuk! That article considers integral transforms in the “Grothendieck context” (and I have added a pointer in the References-section there now). I have focused on the dual “Wirthmüller context” for the time being, since that most directly includes the pull-push in twisted generalized cohomology. But somehow all this should have a dual description in “Grothendieck contexts”, I suppose. I was talking about this with Joost. But I need to look into this more.

@David, yes, so dependent type theory with idempotent (co-)monads is an implementation of “modal hyperdoctrines”, if you wish. I tend to avoid the word “hyperdoctrine” here since it makes something very elementary and basic sound like a big deal. But now that we are passing from indexed cartesian closed contexts to indexed linear monoidal (tensor) closed contexts, it maybe helps to highlight what’s going on.

So “before quantization” we associate to morphisms $f : X \to Y$ base change adjoint triples $(\sum_f \dashv f^\ast \dashv \prod_f)$ between toposes, being dependent sum, context extension, dependent product. Now “when quantizing” we instead associate to morphisms $f : X \to Y$ base change adjoint triples $(f_! \dashv f^\ast \dashv f_\ast)$ between closed tensor categories that constitute “Wirthmüller contexts” (Frobenius reciprocity). Clearly there is at least a strong analogy here and that’s part of the motivation for exploring the formal consequences of the latter further.

]]>