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.
Following discussion in some other threads, I thought one should make it explicit and so I created an entry
Currently this contains some (hopefully) evident remarks of what “dependent linear type theory” reasonably should be at least, namely a hyperdoctrine with values in linear type theories.
The entry keeps saying “should”. I’d ask readers to please either point to previous proposals for what “linear dependent type theory” is/should be, or criticise or else further expand/refine what hopefully are the obvious definitions.
This is hopefully uncontroversial and should be regarded an obvious triviality. But it seems it might be one of those hidden trivialities which deserve to be highlighted a bit more. I am getting the impression that there is a big story hiding here.
Thanks for whatever input you might have.
Could also link to indexed monoidal category, though I’m not sure where.
Thanks, right, i’ll cross link further in a moment. It would be good if we could link to closed ind. Mon. Cats.
Okay, am back online (the previous telegraphic message was from my phone).
I have added to indexed monoidal category the paragraph
If all the fibers are not just monoidal but closed monoidal categories and the base change morphisms are not just strong monoidal but also strong closed monoidal functors , then the indexed monoidal category is an indexed closed monoidal category (Shulman 12, theorem 2.14).
If in addtion all fibers are symmetric monoidal one might also call this a system of Wirthmüller contexts of six operations. If furthermore all fibers have all duals, then this is also what should be called categorical semantics for dependent linear type theory.
and added the Shulman12 references and made indexed closed monoidal category a redirect.
Then to dependent linear type theory I have added at the relevant spot:
Equivalently this is an indexed closed monoidal category with fiberwise duals.
Something seems a little bit off here, at least terminologically. If dependent linear type theory is intended to mean that that the fibers are $\ast$-autonomous categories, then this means something different from assuming the fibers have monoidal duals (the latter would be a special case). Star-autonomous categories have two symmetric monoidal products, $\otimes$ and $\wp$, and “dual” in the sense of $\ast$-autonomous categories means we have maps $\top \to x \wp x^\ast$, $x^\ast \otimes x \to \bot$ that interact appropriately. If the monoidal products $\otimes$ and $\wp$ and monoidal units $\bot$ and $\top$ coincide, then we get duals in the sense of monoidal duals.
I expect you simply don’t mean $\ast$-autonomous categories here, but what I am accustomed to calling a compact closed categories (there are other adjectives that sometimes get used, such as “rigid” and “autonomous”, although I think these can refer to more refined situations which involve braidings and twists).
Personally, I think “linear type theory” should refer to any type theory without contraction and weakening, corresponding to any noncartesian monoidal category. Giraud’s original linear type theory corresponded to $*$-autonomous categories, but from an applied category-theorist’s point of view, $*$-autonomous categories are fairly rare.
Mike: yes, I would agree with that; it’s just that the articles linear type theory, dependent linear type theory, etc. refer specifically to $\ast$-autonomous categories, which is probably not really appropriate for the intended applications. “Linear logic” was invented by Girard, and then given categorical semantics in $\ast$-autonomous categories, but somewhere along the line people found it useful to use the word “linear” more generally than that to refer to general symmetric monoidal contexts.
I even think that the more general meaning follows naturally from the original motivation for “linear”, which if I understand correctly is that each variable must appear exactly once in a term (as in $f(x) = a x$ rather than $g(x) = a x^2 + b x + c$). Nothing in that explanation has to do with $*$-autonomy.
I think sometimes people say “classical linear logic” to indicate the presence of an involutive “negation” (since ordinary classical logic has an involutive negation, unlike ordinary intuitionistic logic), which is the $*$-autonomous version, and “intuitionistic linear logic” when it is absent. It’s probably a bit misleading, but not too bad terminology.
Okay, thanks for the comments. I am happy about using “linear logic” in this more general sense, as this happens to be what arises in the applications that I keep talking about here. I just had thought I’d better stick with what seemed to me to be the established terminological conventions. But if it’s not, all the better. But notice that the old $n$Lab entry linear logic follows just this convention, too (or did follow, I have now edited the introduction there, too).
At linear type theory I have now made the entry paragraph read as follows:
Linear type theory is the linear logic-version of type theory. In the sense of (Seely 89, prop. 1.5), following (Girard 87), this is the internal language of/has categorical semantics in star-autonomous categories. But more generally linear type theory came to refer to the internal type theory of any possibly-non-cartesian symmetric closed monoidal category. Indeed, this still follows the original motivation for the term “linear” as introduced in (Girard 87), since the non-cartesianness of the tensor product means the absense of a diagonal map and hence the impossibility of functions to depend on more than a single (linear) copy of their variables.
Is that better? Otherwise, please feel invited to edit, or else erase it and start afresh.
Following various recent discussion here, I have edited my pdf note a bit further, now it’s called
I have allowed myself to link to this from dependent linear type theory and from integral transform. In fact I thought maybe it should rather be an nLab entry. Please regard it as such and don’t hesitate to criticize. Maybe eventually I’ll turn it into one.
My impression is that there are still some circles in which “linear type theory” or “linear logic” refers by default to the $*$-autonomous sort. But I think the more general choice is now common enough not to be a radical departure, and it makes sense for the nLab.
I have added to dependent linear type theory in a new section Properties – The canonical co-modality a remark on how Girard’s “$!$“-modality is canonically induced in dependent linear type theory.
Thanks Urs (#10); this is looking better. I think any lingering dissatisfaction I may have is mostly to do with the state of linear logic – not your fault and not the focus of the present discussion! I hope to do some work on this a little later.
Re Type-semantics for quantization, in Example 2.4,
Remark 2.6: has $X$ and $A$.
Typos
Thanks for catching typos! (that example 2.4 had been quite a bit of a mess, admittedly) Have fixed them now, and have added an acknowledgement.
The fact alone that linear logic is the internal language of tensor categories makes clear that it is related to quantum mechanics. There should be a wealth of literature on the relation of linear logic to quantum logic and quantum computing. I saw it stated that Girard himself in 1989 started playing with this. But I don’t seem to have found lots of good references on this relation yet. The following two I saw
Vaughan Pratt, Linear logic for generalized quantum mechanics, in Proc. of Workshop on Physics and Computation (PhysComp’92) (pdf, web)
Ugo Dal Lago, Claudia Faggian, On Multiplicative Linear Logic, Modality and Quantum Circuits (arXiv:1210.0613)
Can anyone help with further pointers?
I was asked to say what the stuff at Type-semantics for quantization (schreiber) may have to say about resolving old confusion about “interpretation of quantum mechanics” in terms of modern maths. That made me think that there might be more value hidden in reading the linear push-forwards $f_!$ and $f_\ast$ very explicitly as logical operations $\sum_f$ and $\prod_f$.
One might argue that this gives for instance a nice story of quantum interference in the path integral as follows:
by the discussion at Type-semantics for quantization (schreiber) the path integral, as any other integral kernel, is essentially given by $f_!$ hence by $\sum_f$. So
in non-linear logic we have: “there is a path”
in non-linear homotopy type theory we have “the space of all paths and their phases”
in linear homotopy type theory we have “the linear space of all paths and all their phases added up and interfered”.
It’s clear from the formalism that this is indeed what is happening, but maybe the way to say what is going on here in everyday language can be further improved.
Ah, this reference here is good, should have known about that:
Regarding Girard, he has collected together some lectures in his book The Blind Spot.
I like this idea of (linear) homotopy type theory allowing the expression of something puzzling in natural language, where a misconception comes from reading it out of context, literally in the case of covariance.
Thanks for the pointer to his Lectures on Logic! Interesting, Girard enjoys voicing strong opinion. (Not in each case is it fully clear to me what the polemic is aimed at, though.)
In particular he indulges in trashing vonNeumann-style quantum logic and clearly means linear logic to be the right substitute.
Just for the record: the integral kernel construction in dependent linear type theory which is discussed in Type-semantics for quantization (schreiber) appears in a special case in Construction 4.0.7 of the recent
I have added an example 4.12 to Type-semantics for quantization which spells out how the Hopkins-Lurie notion of integration is directly a special case of the general abstract notion in dependent linear homotopy type theory.
In the right entry of the diagram at 4.12 you have $Func(Y, \mathcal{X})$.
Also ’statetement’ in abstract.
Thanks! Fixed now.
And happy Christmas to everybody here.
Frohe Weihnachten!
Merry Christmas!
A thought and a question, concerning examples of semantics for dependent linear type theory.
Given a topos $\mathbf{H}$ and an object $X \in \mathcal{C}$, write
$\mathcal{C}_X \coloneqq \mathbf{H}_{/X}^{X/}$for the category of pointed objects in the slice of $\mathbf{H}$ over $X$. Regard this as a closed symmetric monoidal category with the smash product $\otimes_X \coloneqq \wedge_X$.
Then for $f \colon X \longrightarrow Y$ any morphism in $\mathbf{H}$, pullback $f^\ast : \mathbf{H}_{/Y} \to \mathbf{H}_{/X}$ preserves pointedness and hence induces $f^\ast \colon \mathcal{C}_Y \to \mathcal{C}_X$. Moreover, using that $f^\ast$ preserves the Cartesian closed structure, that the pointed closed structure is a fiber product of that, and that in the topos colimits and hence the smash product are preserved by pullback, it follows that this $f^\ast$ is strong closed monoidal.
Also the functor $f_! \colon \mathbf{H}^{/X} \to \mathbf{H}^{/Y}$ given by pushout restricts to $\mathcal{C}_X \to \mathcal{C}_Y$ and provides a left adjoint to $f^\ast$. Finally it is clear that $f^\ast$ preserves colimits. So that almost shows that we have
$(f_! \dashv f^\ast \dashv f_\ast) : \mathcal{C}_X \longrightarrow \mathcal{C}_Y$with $f^\ast$ strong closed monoidal, hence satisfying Frobenius reciprocity. I’d just need to think more about the existence of $f_\ast$, since with $\mathcal{C}_X$ not locally representable the adjoint functor theorem is not quite immediate.
In any case, to the extent to which I am not mixing things up, this must be standard. What would be a reference?
Aren’t $\mathcal{C}_X$ and $\mathcal{C}_Y$ locally presentable, so that $f^\ast$ has a right adjoint iff it is cocontinuous?
You can think of $\mathcal{C}_X$ with its forgetful functor $\mathcal{C}_X \to \mathbf{H}/X$ as being the category of algebras in $\mathbf{H}/X$ for the monad $1 + (-): \mathbf{H}/X \to \mathbf{H}/X$, where $1$ denotes the terminal object in the locally presentable category $\mathbf{H}/X$. This monad is accessible, so the category of algebras is locally presentable.
I don’t know of a specific reference in the literature for the facts you are after.
(Edit: By “topos”, I took it you meant “Grothendieck topos”.)
Ah, thanks, Todd!
I have given accessible monad a stand-alone entry to remember this fact, and also added it to Eilenberg-Moore category – local presentability. Cross-linked with topos of algebras over a monad.
Have now written out the content of #28 at Wirthmüller context – Examples – On pointed objects.
Another fact (also non-trivial) is that over- and undercategories of accessible categories are accessible. More generally, if $F$ and $G$ are accessible functors, so is the comma category $(F \downarrow G)$.
Okay, thanks. You should add that (best with proof and/or citation) to accessible category. Thanks!
Let’s see if we can further push the example of #28 with such technology.
So in the context of #28 I am considering now furthermore an endofunctor $\oint \colon \mathbf{H} \to \mathbf{H}$ of which I assume that it preserves limits and colimits and has the structure of an idempotent monad (it is an infinitesimal shape modality).
Then I want to consider the restriction of the adjoint triples $(f_! \dashv f^\ast \dashv f_\ast) : \mathbf{H}_{/X}^{X/} \to \mathbf{H}_{/Y}^{Y/}$ to the full subcategories
$F_X \hookrightarrow \mathbf{H}_{/X}^{X/}$on those objects in the slice over $X$ whose underlying morphism $(E \to X)$ is sent to an equivalence by $\oint$.
It is immediate to check that $f_!$ and $f^\ast$ preserve these subcategories. Also one can see that the inclusions $F_X \hookrightarrow \mathbf{H}_{/X}^{X/}$ preserve colimits. Therefore to see that also $f_\ast$ restricts to the system of subcategories it would be sufficient to see that also $F_X$ is locally presentable.
Is it?
I’m having trouble putting my hands on Makkai-Reyes at the moment, but I seem to recall they have even more general results, e.g., that the 2-category of accessible categories and accessible functors admits lax 2-limits.
I see in this discussion Richard Garner mentioning that pullback of accessible categories along isofibrations being again accessible.
Ah, this prop 3 at accessible category should answer #34 positively.
Thanks, Mike! That’s excellent.
I have now added these pointers to your articles to Wirthmüller context – Examples – Pointed objects with smash product (and to my pdf note).
Given this, might you have a comment on #34, too? Might something like this also be in your articles, or be a direct consequence of some statements there?
I had tried to think for a bit about how to describe $f_\ast$ here more explicitly , but then gave up. Probably I should try again.
In #34, it’s easy to see by mates that if $f^*:F_Y \to F_X$ has a right adjoint, then that right adjoint is the restriction of $f_*$ iff the reflectors commute with the $f^*$s. I suspect that the latter condition should be sufficient for $f_*$ to restrict to the $F$s (hence be a right adjoint to $f^*:F_Y \to F_X$), but I don’t have time right now to verify it. (It should be true because if the reflectors commute with the $f^*$s, then we have a “reflective sub-indexed-category”, which should therefore be “closed under limits”, including the “indexed products” that are the $f_*$s.)
A question on (possible) terminology:
given that a symmetric monoidal category serves as semantics for a fragment of linear type theory, what would be an incarnation in the logic/type theory literature of a (lax) monoidal functor?
Specifically, given a dependent linear type theory Mod with underlying category of types $\mathbf{H}$, and given any type $X \in \mathbf{H}$, then what would you logically/type theoretically make of a lax monoidal functor from $X$-dependent types to $X$-dependent linear types
$\mathbf{H}_{/X} \longrightarrow Mod(X)$?
A functor of this form in itself is of the kind as appears in the Lawvere-ian interpretation of comprehesion as we just discussed recently in another thread. Now specifically for $Mod$ here a hyperdoctrine of linear types and for this functor being lax monoidal, does that remind you (anyone) of anything that has been considered from the point of view of logic/type theory?
Yes, it’s the dependent version of the monoidal adjunction between linear/nonlinear types that gives rise to the ! modality on linear types.
Let me give you the concrete example that I have in mind – which does happen to have some similarity with the !-modality, so maybe there is something here; let me know if the following makes you see a useful connection:
(Ah, I shouldn’t have said that generally I want the same context $X$ on both sides…)
So with Joost I am looking at Jacob Lurie’s A Survey of Elliptic Cohomology and we are trying to relate this to some of the constructions that we have been exploring elsewhere.
Consider, if you have a second, theorem 3.2 there, and specifically its proof. This is about functors $\mathcal{F}_T$ for suitable groups $T$ that take objects in an orbit category, hence some $T/T_0$ in $\mathbf{H}_{/\mathbf{B}T}$, to $Mod(M_T)$ (for some type $M_T$) by pushing the tensor unit along a map $M_{T_0} \longrightarrow M_T$.
According to the discussion in the middle of p. 25 this is monoidal. And according to the hints in section 5.1 there this is supposed to generalize to slices over types more general than of the form $\mathbf{B}T$.
(The idea is that for $X$ a $T$-space then the global sections of $\mathcal{F}_T(X) \in Mod(M_T)$ “are” the $T$-equivariant elliptic cohomology of $X$. )
Here are some questions for Mike (most likely, but of course also for anyone else who feels like replying):
How much exactly does the coherence of the string diagram calculus in indexed monoidal categories that satisfy Frobenius reciprocity depend on Beck-Chevalley? As you emphasize in your article with Kate Ponto, you apply BC only to a few types of diagrams. Is there a point in considering the case where BC only holds for these?
Do you have a name for the case where we have Frobenius reciprocity but not Beck-Chevalley, and do you think it deserves one? I see in your articles you always assume BC and then later add reciprocity/projection formula. But for the purposes of quantization that I am looking into, I seem to only need Frobenius reciprocity to set up the process of quantization as such, and Beck-Chevalley I seem to only need then to prove that the resulting propagation functor is monoidal (from cobordisms to $Mod(\ast)$).
Do you have a word for the condition that an $\mathbf{H}$-indexed monoidal category $Mod(-)$ satsifies $Mod(X \times Y)\simeq Mod(X) \otimes_{Mod(\ast)}Mod(Y)$ for $X, Y \in \mathbf{H}$, where on the right we have a suitable tensor product of “2-modules”, as it were, over $Mod(\ast)$? Do we maybe have some other good conditions that already imply this?
Mike, I have another small question:
By that crucial lemma 3.2 in your article with Kate Ponto, we know that (pullback and) dependent sum respects the external product.
Now I would like to say that the adjunction counit is natural under this equivalence, hence that its component at some external product is the external product of its components.
It’s probably dead simple…
Yes, there is a point, and we even gave it a name (“indexed homotopy coproducts”). I think the only BC condition which is absolutely crucial for meaningfulness of the string diagram calculus is the one we called “commutativity with reindexing”, since it translates into an isotopy. But I can’t be precise about that, because we don’t have a coherence theorem for these string diagrams!
No, I don’t have a name for it.
No.
I think that’s basically the definition of mates.
Thanks, in particular for the fourth! That helps.
Added to dependent linear type theory a pointer to the new
and re-worked the Idea-section a little to reflect its existence.
I haven’t read the paper very carefully yet, but the author seems to be unaware of CLF, which solved the problem of extending LLF with positive connectives ($\otimes,1,!,\exists$). The ideas introduced by CLF were quite influential in some circles (particularly at CMU), so I think it would be worth adding a reference here (I could do that myself) to make people more aware of its existence.
Thanks, Noam!!
Please do add a note to the nLab entry, I’d be most interested.
okay, I added a note and a reference.
Thanks. I’d need to look into this further, but maybe you can quickly help me:
Would the syntax of Pfenning06+WCFW03 be anything close to having semantics in indexed closed monoidal categories?
How do you see Matthijs Vákár syntax in relation to that of Pfenning+WCFW03 ?
I suspect that a semantics of CLF in indexed closed monoidal categories would be sound but not complete. One of the key ideas of CLF was to maintain a syntactic separation between negative (or “asynchronous”) and positive (or “synchronous”) types, with the positive fragment “encapsulated in a monad” as the abstract of that tech report says (it might be better to say that the two categories of types are related by an adjunction; note that this is a bit different from the idea of a “linear-non-linear adjunction”, since here both categories of types are linear). Formally, this separation is used in order to derive a very simple equational theory: terms are only quotiented by $\alpha$-equivalence, together with a simple notion of “permutative conversion” which expresses that the monad is commutative (in fact this latter condition could be dropped and the theory would still hang together, but it is useful for the intended applications to modelling concurrency). Notice that I have not mentioned $\beta$ or $\eta$! Those are not taken as axioms—rather, the type theory is structured to maintain the invariant that all terms are fully $\beta$-reduced and $\eta$-expanded. (This was a very innovative idea at the time, since it entirely side-stepped one of the traditional thorny issues in dependent type theory.)
Since the monad/adjunction is actually present in the type theory (i.e., there is a corresponding type constructor), a complete semantics would presumably reflect this. Perhaps one could obtain a sound semantics in indexed closed monoidal categories by instantiating to the identity monad, though I haven’t checked this and don’t know if anyone else has.
As for the paper by VÃ¡kÃ¡r, well, it seems that he considers various different corners of the design space for “intuitionistic linear dependent type theory”. The specific theory ILDTT, though, does seem quite close to CLF in expressive power—in particular the restriction to types dependent on an intuitionistic context—and so I would be very interested if he could adapt his semantics to CLF (keeping in mind what I said above about the “missing monad”). This might help to resolve the conjectures listed on p.19, since these are precisely the kinds of issues which the CLF approach was designed to circumvent.
I see, thanks.
Looks like somebody like RAG Seely is needed once more to come and sort out the syntax-semtantics relation cleanly.
Bas Spitters kindly points out that a dependent linear version of system L had once been considered in
Have now added a pointer (just a pointer) to that to the entry, too.
Hi Matthijs,
thanks, again, for dropping by, also here!
I understand, and my only suggestion is that it would be useful — for readers, for “the community”, for purposes of references — to state the syntax/semantics equivalences that are clearly very clear to you personally also very clearly in text.
Currently you have, somewhat hidden inside the proof of your theorem 9, a throwaway remark that the relevant fragment of your syntax is indeed the internal language of strict indexed symmetric monoidal categories. I missed this statement on first reading, and it is easy to miss, being inside the proof of another statement which is only fragmentarily related.
A text on the syntax and semantics of dependent linear type theory I would ideally hope to have a tabulated list of the form:
the syntax for strict indexed symmetric monoidal categories is precisely A
the syntax for strict indexed closed symmetric monoidal categories is precisely A+B
the syntax for strict indexed symmetric monoidal categories with comprehension is precisely A+C
etc.
Think of it this way: I would like to exapnd the table on the page relation between type theory and category theory by including entries with fragments of “dependent linear type theory” on the left and on the right pointers to the literature.
In fact I’ll add a row to that table now, pointing to your article. But as it stands the reader may have a bit of trouble isolating the statement in your article (as I had, on first reading).
Okay, thanks. I really think it would be worthwhile, but I should say: don’t let me distract you too much from what I guess your advisor/coauthors would want you to do instead!
While we are at it, here is a trivial typo which I spotted:
p. 10 in “Judgements”, below “…of the following six forms”:
the second line needs “$\sigma$” to be replaced by $A$;
the third item needs a capitalization of the second “$a$”
Another comment: I gather your discussion of comprehension in the linear dependent context is an elaboration on the observation that I had made here (and on p. 48 of “Quantization via Linear homotopy types”), right? I think your readers might really appreciate it if you made it clearer what is going on here. Presently your article jumps right into some fairly non-obvious syntax on p. 6 and p. 21, and I think the reader who doesn’t already know what you are after here will find this somewhat mysterious and unmotivated. (I may be very wrong here, after all I am not a logician and I realize that logicians are a very different species ;-) In footnote 18 you start giving what I would consider an actual explanation of what’s going on with comprehension here. Maybe some such explanation could be moved right to a prominent position in the main text, to help the reader follow you? Just an idea.
I am filling content into dependent linear type theory.
Now it says the entry is locked by an anonymous. This used to be a spurious message appearing all the time in the old days, and was a bug. Now I am not sure. If anyone reading here is really editing then: please wait – I am in the middle of editing.
Have edited a good bit more at dependent linear type theory. Will continue tomorrow.
The main new addition so far is maybe that I added the definition of fundamental classes and of secondary integral transforms in terms of dependent linear type theory. Added also the example which shows (or states at least) that for parameterized modules this reproduces matrix calculus.
Maybe I’ll further expand the included table twisted generalized cohomology in linear homotopy type theory – table now, but then I need to quit for today.
Have edited a bit more.
I’ll have to leave it the way it is for the moment, have to rush off now. I am going to use part of this as a script for a talk to the type theory group at Paris-Diderot today, around Paul-André Melliès. My goal is to
first convince the audience that six-functor Yoga in Wirthmüller style is precisely what ought to be regarded as the semantics for dependent linear (homotopy-)type theory (i.e. any proposed syntax ought to have that as its semantics),
then to indicate that in such contexts one may elegantly axiomatize “secondary integral transforms”,
point out that these capture/generalize the exponential modality construction,
highlight that it is manifestly a path-integral-like construction
and finally to indicate that in the model of parameterized modules this gives matrix calculus,
and to claim that in the model of parameterized spectra it gives pull-push in bivariant tiwsted generalized cohomology.
We’ll see how it works.
(I’ll duly highlight Mike’s many contributions to this. )
Have added two new references to dependent linear type theory:
Matthijs Vákár has new talk notes [2] expanding on his article [3] and Neelakantan Krishnaswami with Pierre Pradic and Nick Benton have an article in preparation [4].
[2] http://users.ox.ac.uk/~magd3996/research/10-11-2014-Oxford-Linear%20dependent%20types.pdf
[3] http://arxiv.org/abs/1405.0033
[4] http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf
Matthijs Vákár’s thesis is out, so I’ve added that to his page. I don’t know whether its separate strands supersede individual publications, such as the one in #48.
Thanks for the alert. I had not seen that yet.
I wish I had time to read Vákár’s thesis carefully. It looks like he may be solving the problem in the non-homotopy case, specifying a syntax and a semantics and proving that they match up (p81):
The structure we obtain is that of a strict indexed symmetric monoidal category with comprehension
We also get a mention (p71):
Although in the last while some suggestions have been made on the nLab and nForum of possible connections between the syntactic and semantic work, no account of the correspondence was published.
(-:
I added this recent reference
After the “great split” where much of this page was sent over to indexed monoidal (infinity,1)-category, the links in
What should be the categorical semantics of dependent linear type theory was discussed in (Shulman 08, Ponto-Shulman 12, Shulman 12, Schreiber 14)
no longer work.
A simple fix is possible, but without wishing to provoke the tensions which tend to arise in these parts from differences of opinion on the necessity for syntax when one speaks of a type theory, is the page due a make-over? Why was that quoted sentence in the section ’Syntax’ in any case?
Alternatively we wait for the roll out of the LSR program when all modal dependent type theories will be given their proper setting.
Yes, that sentence seems like it should probably be moved to the “Semantics” section.
Added arXiv number and comlete publication data to
added pointer to:
and added cross-links with the new entry quantum programming language
And one more:
I seem to be seeing polynomial functors wherever I look these days.
added these two pointer:
Matthijs Vákár, A Categorical Semantics for Linear Logical Frameworks, In: A. Pitts (ed.), Foundations of Software Science and Computation Structures FoSSaCS 2015. Lecture Notes in Computer Science, vol 9034. Springer 2015 (arXiv:1501.05016, doi:10.1007/978-3-662-46678-0_7)
Matthijs Vákár, Section 3 of: In Search of Effectful Dependent Types (arXiv:1706.07997, uuid:e91e19b3-7e10-4fda-9433-f23b469e4049)
added pointer to the thesis
(which became the preprint Lundfall 18, arXiv:1806.09593 – both, apparently, unpublished)
Provided links to slides at Bounded Linear Logic Workshop.
added pointer to:
expanded out more details:
Mitchell Riley, Linear Homotopy Type Theory, talk at: HoTTEST Event for Junior Researchers 2022 (Jan 2022) [slides: pdf, video: YT]
Abstract. Some ∞-toposes support constructions that are inherently ’linear’, such as the external smash product of parameterised spectra. These cannot be added axiomatically to ordinary HoTT, because there is no way to enforce this linearity: there are no restrictions on variable uses. This talk describes an extension of HoTT with linear tensor and hom type formers, as a kind of ’binary modality’ and its right adjoint. Trying to stay compatible with existing results in HoTT naturally leads us to a novel kind of bunched dependent type theory. Our type theory is intended to be as human-usable as possible, with an eye towards synthetic stable homotopy theory.
and linked to it from the beginning of the Idea-section where “linear homotopy type theory” is first mentioned.
Yes, most CQTS researchers have arrived and settled in (only Marwa and Tatiana yet to arrive in person). Yesterday and today we had the initial researcher’s meeting, with everyone presenting their work. (10 min ago I just wrapped up the meeting here, after somewhat of a marathon session.)
I see that you are eager to get feedback on your remarks, but maybe help us a bit: Could you phrase a concrete question or proposal? I am still a little uncertain as to what kind of feedback to give.
One question at least, for linear HoTT, is it worth exploring the idea of $\Sigma^\infty \Omega^\infty$ as exponential, $!$, by looking at that synthetic treatment of the component maps in arXiv:2102.04099?
$\Omega^{\infty} E := \natural (\mathbb{S} \to E)$ and $\Sigma^{\infty} E := E \wedge \mathbb{S}$, then $! E = \Sigma^\infty \Omega^\infty E = \mathbb{S} \wedge \natural (\mathbb{S} \to E).$
One line of thought here, given the adjunction of pointed maps they mention under definition 3.17, $- \wedge A \vdash A \to_{\ast} -$, the composite looks like a variation on the store comonad, $D X = W \times [W, X]$, (whose coalgebras are lenses).
That seems to have an obvious answer: Yes, worth exploring. :-)
First thing we are aiming at (as laid out in my PlanQC talk today) is implementing the dependent type family of $\mathfrak{su}(2)_k$-conformal blocks into Agda. The formula laid out here gives this as a plain dependent type. But of course it is (or ought to be) a linear dependent type. Hence an application of $\Sigma^\infty \Omega^\infty$ must be “undone”. This will be a consequence of understanding the Eilenberg-MacLane type entering the formula as the image under $\Sigma^\infty \Omega^\infty$ of the EM-spectrum type.
Once the resulting (linear) dependent type of conformal blocks is coded into Agda, we have a first (not so-)rudimentary “anyon-hardware-aware topological quantum simulator”. I’ll keep you all posted about progress.
added pointer to:
1 to 84 of 84