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
   • CommentTimeDec 9th 2013
   • (edited Dec 9th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexFollowing discussion in some other threads, I thought one should make it explicit and so I created an entry * _[[dependent linear type theory]]_. 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.

   Following discussion in some other threads, I thought one should make it explicit and so I created an entry

   • dependent linear type theory.

   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.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeDec 9th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexCould also link to [[indexed monoidal category]], though I'm not sure where.

   Could also link to indexed monoidal category, though I’m not sure where.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeDec 9th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, right, i'll cross link further in a moment. It would be good if we could link to closed ind. Mon. Cats.

   Thanks, right, i’ll cross link further in a moment. It would be good if we could link to closed ind. Mon. Cats.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeDec 10th 2013
   • (edited Dec 10th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOkay, 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](#Shulman12)). > If in addtion all fibers are [[symmetric monoidal category|symmetric monoidal]] one might also call this a system of [[Wirthmüller contexts]] of [[six operations]]. If furthermore all fibers have all [[dual objects|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 [[dual object|duals]]. ***

   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.

   ---

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeDec 10th 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexSomething 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).

   Something seems a little bit off here, at least terminologically. If dependent linear type theory is intended to mean that that the fibers are $!A = \sum_{E: V} (E \to A}\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).

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeDec 10th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexPersonally, 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorTodd_Trimble
   • CommentTimeDec 10th 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexMike: 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeDec 10th 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeDec 10th 2013
   • (edited Dec 10th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOkay, 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](#Seely89)), following ([Girard 87](#Girard87)), 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 monoidal category|cartesian]] [[symmetric monoidal category|symmetric]] [[closed monoidal category]]. Indeed, this still follows the original motivation for the term "linear" as introduced in ([Girard 87](#Girard87)), 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.

   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.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013
    • (edited Dec 11th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexFollowing various recent discussion here, I have edited my pdf note a bit further, now it's called * _[[schreiber:Type-semantics for quantization]]_. 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.

    Following various recent discussion here, I have edited my pdf note a bit further, now it’s called

    • Type-semantics for quantization (schreiber).

    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.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 10th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexMy 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.

    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.

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have added to _[[dependent linear type theory]]_ in a new section _[Properties -- The canonical co-modality](http://ncatlab.org/nlab/show/dependent+linear+type+theory#TheCanonicalComodality)_ a remark on how Girard's "$!$"-modality is canonically induced in dependent linear type theory.

    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.

13. • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 10th 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexThanks 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.

    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.

14. • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 11th 2013
    • (edited Dec 11th 2013)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRe _Type-semantics for quantization_, in Example 2.4, * $X$ and $Y$ became $X_1$ and $X_2$ * The Frobenius reciprocity equivalence has its $A$ and $B$ reversed with respect to Remark 2.3, making it a little harder to compare * The pullback on the right of the pasting law equivalence should be $B \times_{X_2} A$. Remark 2.6: has $X$ and $A$.

    Re Type-semantics for quantization, in Example 2.4,

    • $X$ and $Y$ became $X_1$ and $X_2$
    • The Frobenius reciprocity equivalence has its $A$ and $B$ reversed with respect to Remark 2.3, making it a little harder to compare
    • The pullback on the right of the pasting law equivalence should be $B \times_{X_2} A$.

    Remark 2.6: has $X$ and $A$.

15. • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 11th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexTypos * discuss a ageneral * embodies a higher analog integral transformations

    Typos

    • discuss a ageneral
    • embodies a higher analog integral transformations
16. • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeDec 11th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks 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.

    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.

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeDec 22nd 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexThe 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](http://boole.stanford.edu/pub/ql.pdf), [web](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.7817)) * Ugo Dal Lago, Claudia Faggian, _On Multiplicative Linear Logic, Modality and Quantum Circuits_ ([arXiv:1210.0613](http://arxiv.org/abs/1210.0613)) Can anyone help with further pointers? I was asked to say what the stuff at _[[schreiber:Type-semantics for quantization]]_ 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 _[[schreiber:Type-semantics for quantization]]_ the path integral, as any other integral kernel, is essentially given by $f_!$ hence by $\sum_f$. So 1. in non-linear logic we have: "there is a path" 1. in non-linear homotopy type theory we have "the space of all paths and their phases" 1. 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.

    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

    1. in non-linear logic we have: “there is a path”

    2. in non-linear homotopy type theory we have “the space of all paths and their phases”

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

18. • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeDec 23rd 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, this reference here is good, should have known about that: * [[Ross Duncan]], _Types for quantum mechanics_, 2006 ([pdf](http://homepages.ulb.ac.be/~rduncan/papers/rduncan-thesis.pdf))

    Ah, this reference here is good, should have known about that:

    • Ross Duncan, Types for quantum mechanics, 2006 (pdf)
19. • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 23rd 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRegarding Girard, he has collected together some lectures in his book [The Blind Spot](http://books.google.co.uk/books?id=eVZZ0wtazo8C). 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.

    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.

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeDec 23rd 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks 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.

    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.

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeDec 23rd 2013
    • (edited Dec 23rd 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexJust for the record: the integral kernel construction in [[dependent linear type theory]] which is discussed in _[[schreiber:Type-semantics for quantization]]_ appears in a special case in Construction 4.0.7 of the recent * Hopkins, Lurie, _[[ Ambidexterity in K(n)-Local Stable Homotopy Theory]]_

    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

    • Hopkins, Lurie, Ambidexterity in K(n)-Local Stable Homotopy Theory
22. • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeDec 24th 2013
    • (edited Dec 24th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have added an example 4.12 to _[[schreiber:Type-semantics for quantization|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.

    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.

23. • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 24th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexIn the right entry of the diagram at 4.12 you have $Func(Y, \mathcal{X})$.

    In the right entry of the diagram at 4.12 you have $Func(Y, \mathcal{X})$.

24. • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 24th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexAlso 'statetement' in abstract.

    Also ’statetement’ in abstract.

25. • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeDec 25th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks! Fixed now. And happy Christmas to everybody here.

    Thanks! Fixed now.

    And happy Christmas to everybody here.

26. • CommentRowNumber26.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 25th 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexFrohe Weihnachten!

    Frohe Weihnachten!

27. • CommentRowNumber27.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 25th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexMerry Christmas!

    Merry Christmas!

28. • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2014
    • (edited Jan 5th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexA 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?

    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?

29. • CommentRowNumber29.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 5th 2014
    • (edited Jan 5th 2014)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexAren'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".)

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

30. • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, 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](http://ncatlab.org/nlab/show/Eilenberg-Moore+category#LocalPresentability)_. Cross-linked with _[[topos of algebras over a monad]]_.

    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.

31. • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexHave now written out the content of #28 at _[Wirthmüller context -- Examples -- On pointed objects](http://nlab.mathforge.org/nlab/show/Wirthmüller+context#PointedObjects)_.

    Have now written out the content of #28 at Wirthmüller context – Examples – On pointed objects.

32. • CommentRowNumber32.
    • CommentAuthorZhen Lin
    • CommentTimeJan 6th 2014
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexAnother 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)$.

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

33. • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, thanks. You should add that (best with proof and/or citation) to _[[accessible category]]_. Thanks!

    Okay, thanks. You should add that (best with proof and/or citation) to accessible category. Thanks!

34. • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014
    • (edited Jan 6th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexLet'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?

    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?

35. • CommentRowNumber35.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 6th 2014
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI'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’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.

36. • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014
    • (edited Jan 6th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI see in [this discussion](http://webcache.googleusercontent.com/search?q=cache:E32EFgJf6vMJ:permalink.gmane.org/gmane.science.mathematics.categories/5931+&cd=9&hl=en&ct=clnk&gl=de&client=opera) Richard Garner mentioning that pullback of accessible categories along isofibrations being again accessible.

    I see in this discussion Richard Garner mentioning that pullback of accessible categories along isofibrations being again accessible.

37. • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, [this prop 3](http://ncatlab.org/nlab/show/accessible+category#StabilityUnderInverseImage) at _[[accessible category]]_ should answer #34 positively.

    Ah, this prop 3 at accessible category should answer #34 positively.

38. • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeJan 6th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRe: #28, two references (without proofs) are examples 12.13 and 13.7 of [0706.1286](http://arxiv.org/abs/0706.1286) and example 2.33 of [1212.3914](http://arxiv.org/abs/1212.3914). I don't think you need an AFT for $f_\ast$, you should be able to just construct it by hand.

    Re: #28, two references (without proofs) are examples 12.13 and 13.7 of 0706.1286 and example 2.33 of 1212.3914. I don’t think you need an AFT for $f_\ast$, you should be able to just construct it by hand.

39. • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014
    • (edited Jan 7th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, Mike! That's excellent. I have now added these pointers to your articles to _[Wirthmüller context -- Examples -- Pointed objects with smash product](http://ncatlab.org/nlab/show/Wirthmüller+context#PointedObjects)_ (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.

    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.

40. • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIn #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.)

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

41. • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeJan 28th 2014
    • (edited Jan 28th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexA 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?

    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?

42. • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeJan 28th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, it's the dependent version of the monoidal adjunction between linear/nonlinear types that gives rise to the ! modality on linear types.

    Yes, it’s the dependent version of the monoidal adjunction between linear/nonlinear types that gives rise to the ! modality on linear types.

43. • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeJan 29th 2014
    • (edited Jan 29th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexLet me give you the concrete example that I have in mind -- which does happen to have some similarity with the [!-modality](http://ncatlab.org/nlab/show/dependent+linear+type+theory#TheCanonicalComodality), 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$. )

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

44. • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeFeb 9th 2014
    • (edited Feb 9th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHere 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?

    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?

45. • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2014
    • (edited Feb 10th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexMike, 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...

    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…

46. • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 10th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex* 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.

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

47. • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2014
    • (edited Feb 11th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, in particular for the fourth! That helps.

    Thanks, in particular for the fourth! That helps.

48. • CommentRowNumber48.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexAdded to _[[dependent linear type theory]]_ a pointer to the new * [[Matthijs Vákár]], _Syntax and Semantics of Linear Dependent Types_ ([arXiv:1405.0033](http://arxiv.org/abs/1405.0033)) and re-worked the Idea-section a little to reflect its existence.

    Added to dependent linear type theory a pointer to the new

    • Matthijs Vákár, Syntax and Semantics of Linear Dependent Types (arXiv:1405.0033)

    and re-worked the Idea-section a little to reflect its existence.

49. • CommentRowNumber49.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeMay 2nd 2014
    • PermaLink
    Author: Noam_Zeilberger
    Format: MarkdownItexI haven't read the paper very carefully yet, but the author seems to be unaware of [CLF](http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf), 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.

    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.

50. • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, Noam!! Please do add a note to the nLab entry, I'd be most interested.

    Thanks, Noam!!

    Please do add a note to the nLab entry, I’d be most interested.

51. • CommentRowNumber51.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeMay 2nd 2014
    • PermaLink
    Author: Noam_Zeilberger
    Format: MarkdownItexokay, I added a note and a reference.

    okay, I added a note and a reference.

52. • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014
    • (edited May 2nd 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks. I'd need to look into this further, but maybe you can quickly help me: Would the syntax of [Pfenning06](http://ncatlab.org/nlab/show/dependent+linear+type+theory#Pfenning96)+[WCFW03](http://ncatlab.org/nlab/show/dependent+linear+type+theory#WCFW03) be anything close to having semantics in [indexed closed monoidal categories](http://ncatlab.org/nlab/show/indexed+monoidal+category#Closed)? How do you see Matthijs Vákár syntax in relation to that of Pfenning+WCFW03 ?

    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 ?

53. • CommentRowNumber53.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeMay 2nd 2014
    • PermaLink
    Author: Noam_Zeilberger
    Format: MarkdownItexI 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 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.

54. • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexI see, thanks. Looks like somebody like RAG Seely is needed once more to come and sort out the syntax-semtantics relation cleanly.

    I see, thanks.

    Looks like somebody like RAG Seely is needed once more to come and sort out the syntax-semtantics relation cleanly.

55. • CommentRowNumber55.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014
    • (edited May 2nd 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexBas Spitters kindly points out that a dependent linear version of [[system L]] had once been considered in * [[Arnaud Spiwak]], section 5 of _A dissection of L_, Logical Methods in Computer Science 1998 [pdf](http://assert-false.net/arnaud/papers/A%20dissection%20of%20L.pdf) Have now added a pointer (just a pointer) to that to the entry, too.

    Bas Spitters kindly points out that a dependent linear version of system L had once been considered in

    • Arnaud Spiwak, section 5 of A dissection of L, Logical Methods in Computer Science 1998 pdf

    Have now added a pointer (just a pointer) to that to the entry, too.

56. • CommentRowNumber56.
    • CommentAuthorMatthijs Vákár
    • CommentTimeMay 5th 2014
    • PermaLink
    Author: Matthijs Vákár
    Format: TextHi, Thank you for the pointer, Noam! Indeed, I completely missed the CLF paper. In general, I'm much more of a category theorist than a syntactician. Just having had a quick glance at the paper, both syntaxes do indeed look quite similar. Obviously, the CLF syntax has been designed with computation in mind, while what I wrote down was meant to be a bit more towards the pure maths side of things, hoping to find a correspondence with certain categories. In particular, it should be a fairly straightforward generalisation of (rather bare) dependent type theory so we can use it to obtain a game semantics for dependent types, by taking the natural interpretation in a category of games and strategies. I haven't been able to have a sufficient look at CLF and am still a bit daunted by all the 'weird symbols'. It is very nice to see, however, that a similar system has been developed that has a good syntactic metatheory. I'd be very interested to see as well if we can find a correspondence with some variant of my categorical semantics. Urs, regarding the syntax-semantics correspondence here: I think I have a pretty good idea of most of it. Perhaps things would be clearer to you if we have syntax in which the categorical aspect of comprehension is also modular? (I think all other things are modular in my syntax/semantics, basically.) I'd be happy to write down this syntax for you if that would clarify things. What you do is you just take an intuitionistic (non-dependent) type theory and a linear type theory in each intuitionistic context with substitution operations by intuitionistic terms that go from one linear type theory to the other. (Basically, this is a strict indexed symmetric multicategory.) Than you can add rules that allow you to glue linear types to intuitionistic contexts and linear terms to intuitionistic context morphisms. (This is your comprehension.) You get a conservative extension of my syntax that now also talks explicitly about intuitionistic terms. This is a real internal language for strict indexed symmetric multicategries (without/with comprehension). If you add tensor and I types to your syntax, you get the case of strict indexed symmetric monoidal categories. Thanks, Bas and Urs, for the pointer to Spiwak's paper. I also didn't know that one. Haven't properly looked at it, but, it seems it considers one particular quite rich system very thoroughly from the syntactic point of view. I'm hoping this'll answer some of my questions about the computational properties of the syntax. :-) On the other hand, it looks specifically classical (rather than intuitionistic) and therefore not so close to the categories we're interested in, but I may be wrong. I'm trying to finish some notes on the model in terms of coherence spaces, now. Hopefully, that should provide some intuition for people who are familiar with coherence spaces or domain theory. At least, I think it's quite an intuitive model, myself, that is reasonably faithful to capturing the essence of the syntax. Certainly much better than the 'free models' I briefly discussed in the paper. After I finish these notes, I'll return to the syntax. :-) Matthijs

    Hi,
    
    Thank you for the pointer, Noam! Indeed, I completely missed the CLF paper. In general, I'm much more of a category theorist than a syntactician. Just having had a quick glance at the paper, both syntaxes do indeed look quite similar. Obviously, the CLF syntax has been designed with computation in mind, while what I wrote down was meant to be a bit more towards the pure maths side of things, hoping to find a correspondence with certain categories. In particular, it should be a fairly straightforward generalisation of (rather bare) dependent type theory so we can use it to obtain a game semantics for dependent types, by taking the natural interpretation in a category of games and strategies.
    
    I haven't been able to have a sufficient look at CLF and am still a bit daunted by all the 'weird symbols'. It is very nice to see, however, that a similar system has been developed that has a good syntactic metatheory. I'd be very interested to see as well if we can find a correspondence with some variant of my categorical semantics.
    
    Urs, regarding the syntax-semantics correspondence here: I think I have a pretty good idea of most of it. Perhaps things would be clearer to you if we have syntax in which the categorical aspect of comprehension is also modular? (I think all other things are modular in my syntax/semantics, basically.) I'd be happy to write down this syntax for you if that would clarify things. What you do is you just take an intuitionistic (non-dependent) type theory and a linear type theory in each intuitionistic context with substitution operations by intuitionistic terms that go from one linear type theory to the other. (Basically, this is a strict indexed symmetric multicategory.) Than you can add rules that allow you to glue linear types to intuitionistic contexts and linear terms to intuitionistic context morphisms. (This is your comprehension.) You get a conservative extension of my syntax that now also talks explicitly about intuitionistic terms. This is a real internal language for strict indexed symmetric multicategries (without/with comprehension). If you add tensor and I types to your syntax, you get the case of strict indexed symmetric monoidal categories.
    
    Thanks, Bas and Urs, for the pointer to Spiwak's paper. I also didn't know that one. Haven't properly looked at it, but, it seems it considers one particular quite rich system very thoroughly from the syntactic point of view. I'm hoping this'll answer some of my questions about the computational properties of the syntax. :-) On the other hand, it looks specifically classical (rather than intuitionistic) and therefore not so close to the categories we're interested in, but I may be wrong.
    
    I'm trying to finish some notes on the model in terms of coherence spaces, now. Hopefully, that should provide some intuition for people who are familiar with coherence spaces or domain theory. At least, I think it's quite an intuitive model, myself, that is reasonably faithful to capturing the essence of the syntax. Certainly much better than the 'free models' I briefly discussed in the paper. After I finish these notes, I'll return to the syntax. :-)
    
    Matthijs
57. • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeMay 5th 2014
    • (edited May 5th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHi 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).

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

58. • CommentRowNumber58.
    • CommentAuthorMatthijs Vákár
    • CommentTimeMay 5th 2014
    • (edited May 5th 2014)
    • PermaLink
    Author: Matthijs Vákár
    Format: TextThanks, Urs. I completely agree that I should probably rewrite the paper a bit to make it more readable. It started as my personal notes and was only a side part of my project, but I then realised that people might be interested so quickly typed it up to a form that others *might* be able to read it. In the next version I will make the suggested changes and generally move things from footnotes and proofs into actual statements in the paper. Also, the example isn't formulated optimally, now. (Although I already have a new version ready.) It, in fact, always has a comprehension. The construction is really taking the free linear predicate type theory on Set given a propositional linear type theory. (or coFree as it is right adjoint to the forgetful functor of evaluating a linear predicate type theory on Set at 1) I didn't explain this properly yet in the current version. This also explains (partly) why the example is so discrete. I'm not entirely sure yet, though, if I should go for the real internal language syntax... if I find time, I could add an appendix. Really appreciate the feedback. Thanks!

    Thanks, Urs. I completely agree that I should probably rewrite the paper a bit to make it more readable. It started as my personal notes and was only a side part of my project, but I then realised that people might be interested so quickly typed it up to a form that others *might* be able to read it.
    
    In the next version I will make the suggested changes and generally move things from footnotes and proofs into actual statements in the paper. Also, the example isn't formulated optimally, now. (Although I already have a new version ready.) It, in fact, always has a comprehension. The construction is really taking the free linear predicate type theory on Set given a propositional linear type theory. (or coFree as it is right adjoint to the forgetful functor of evaluating a linear predicate type theory on Set at 1) I didn't explain this properly yet in the current version. This also explains (partly) why the example is so discrete.
    
    I'm not entirely sure yet, though, if I should go for the real internal language syntax... if I find time, I could add an appendix.
    
    Really appreciate the feedback. Thanks!
59. • CommentRowNumber59.
    • CommentAuthorUrs
    • CommentTimeMay 5th 2014
    • (edited May 5th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, 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](http://ncatlab.org/nlab/show/axiom+of+separation#ExamplesDependentLinearTypeTheory) (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.

    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.

60. • CommentRowNumber60.
    • CommentAuthorUrs
    • CommentTimeNov 11th 2014
    • (edited Nov 11th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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.

    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.

61. • CommentRowNumber61.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2014
    • (edited Nov 12th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHave 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](http://ncatlab.org/nlab/show/dependent+linear+type+theory#FundamentalClasses)_ and of _[secondary integral transforms](http://ncatlab.org/nlab/show/dependent+linear+type+theory#SecondaryIntegralTransforms)_ in terms of dependent linear type theory. Added also the [example](http://ncatlab.org/nlab/show/dependent+linear+type+theory#ParameterizedModules) 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 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.

62. • CommentRowNumber62.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2014
    • (edited Nov 12th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHave 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 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. )

63. • CommentRowNumber63.
    • CommentAuthorUrs
    • CommentTimeNov 13th 2014
    • (edited Nov 13th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHave 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

    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

64. • CommentRowNumber64.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 17th 2017
    • (edited Jul 17th 2017)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex[[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.

    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.

65. • CommentRowNumber65.
    • CommentAuthorUrs
    • CommentTimeJul 17th 2017
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks for the alert. I had not seen that yet.

    Thanks for the alert. I had not seen that yet.

66. • CommentRowNumber66.
    • CommentAuthorMike Shulman
    • CommentTimeOct 26th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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 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.

    (-:

67. • CommentRowNumber67.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 2nd 2018
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI added this recent reference * [[Martin Lundfall]], _A diagram model of linear dependent type theory_, ([arXiv:1806.09593](https://arxiv.org/abs/1806.09593)) <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/3">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/3">v3</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    I added this recent reference

    • Martin Lundfall, A diagram model of linear dependent type theory, (arXiv:1806.09593)

    diff, v3, current

68. • CommentRowNumber68.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 10th 2018
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexAfter 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.

    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.

69. • CommentRowNumber69.
    • CommentAuthorMike Shulman
    • CommentTimeOct 12th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, that sentence seems like it should probably be moved to the "Semantics" section.

    Yes, that sentence seems like it should probably be moved to the “Semantics” section.

70. • CommentRowNumber70.
    • CommentAuthorMike Shulman
    • CommentTimeJul 7th 2020
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAdded reference * Peng Fu, Kohei Kishida, Peter Selinger, _Linear Dependent Type Theory for Quantum Programming Languages_, in LICS 2020; [DOI](https://dl.acm.org/doi/10.1145/3373718.3394765), [PDF](https://depend.cs.uni-saarland.de/lics-icalp/papers/B5.F), [video](https://www.youtube.com/watch?v=GUT8j4V6Nzg). <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/8">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/8">v8</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    Added reference

    • Peng Fu, Kohei Kishida, Peter Selinger, Linear Dependent Type Theory for Quantum Programming Languages, in LICS 2020; DOI, PDF, video.

    diff, v8, current

71. • CommentRowNumber71.
    • CommentAuthorUrs
    • CommentTimeFeb 16th 2021
    • PermaLink
    Author: Urs
    Format: MarkdownItexAdded arXiv number and comlete publication data to * {#FKS20} [[Peng Fu]], [[Kohei Kishida]], [[Peter Selinger]], _Linear Dependent Type Theory for Quantum Programming Languages_, LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440–453 ([arXiv:2004.13472](https://arxiv.org/abs/2004.13472), [doi:10.1145/3373718.3394765](https://dl.acm.org/doi/10.1145/3373718.3394765), [pdf](https://depend.cs.uni-saarland.de/lics-icalp/papers/B5.F), [video](https://www.youtube.com/watch?v=GUT8j4V6Nzg)) added pointer to: * [[Peng Fu]], [[Kohei Kishida]], [[Neil Ross]], [[Peter Selinger]], _A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper_, in I. Lanese, M. Rawski (eds.) _Reversible Computation_ RC 2020. Lecture Notes in Computer Science, vol 12227 ([arXiv:2005.08396](https://arxiv.org/abs/2005.08396), [doi:10.1007/978-3-030-52482-1_9](https://doi.org/10.1007/978-3-030-52482-1_9)) and added cross-links with the new entry _[[quantum programming language]]_ <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/10">v10</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    Added arXiv number and comlete publication data to

    • {#FKS20} Peng Fu, Kohei Kishida, Peter Selinger, Linear Dependent Type Theory for Quantum Programming Languages, LICS ’20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440–453 (arXiv:2004.13472, doi:10.1145/3373718.3394765, pdf, video)

    added pointer to:

    • Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger, A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper, in I. Lanese, M. Rawski (eds.) Reversible Computation RC 2020. Lecture Notes in Computer Science, vol 12227 (arXiv:2005.08396, doi:10.1007/978-3-030-52482-1_9)

    and added cross-links with the new entry quantum programming language

    diff, v10, current

72. • CommentRowNumber72.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2021
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAdded some references for other kinds of DLTT. <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/11">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/11">v11</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    Added some references for other kinds of DLTT.

    diff, v11, current

73. • CommentRowNumber73.
    • CommentAuthorMike Shulman
    • CommentTimeMar 27th 2021
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAnd one more: * [[Mike Shulman]], _A type theory for fibred functors and polynomials_. Unfinished note, 2018. [pdf](http://home.sandiego.edu/~shulman/papers/functors.pdf) <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/11">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/11">v11</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    And one more:

    • Mike Shulman, A type theory for fibred functors and polynomials. Unfinished note, 2018. pdf

    diff, v11, current

74. • CommentRowNumber74.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 27th 2021
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI seem to be seeing polynomial functors wherever I look these days.

    I seem to be seeing polynomial functors wherever I look these days.

75. • CommentRowNumber75.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2021
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded 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](https://arxiv.org/abs/1501.05016), [doi:10.1007/978-3-662-46678-0_7](https://doi.org/10.1007/978-3-662-46678-0_7)) * [[Matthijs Vákár]], Section 3 of: *In Search of Effectful Dependent Types* ([arXiv:1706.07997](https://arxiv.org/abs/1706.07997), [uuid:e91e19b3-7e10-4fda-9433-f23b469e4049](https://ora.ox.ac.uk/objects/uuid:e91e19b3-7e10-4fda-9433-f23b469e4049)) <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/13">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/13">v13</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    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)

    diff, v13, current

76. • CommentRowNumber76.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2021
    • (edited May 13th 2021)
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded pointer to the thesis * [[Martin Lundfall]], *Models of linear dependent type theory*, 2017 ([pdf](https://ncatlab.org/nlab/files/LundfallModelsOfLinerDTT.pdf)) (which became the preprint [Lundfall 18](https://ncatlab.org/nlab/show/dependent+linear+type+theory#Lundfall18), [arXiv:1806.09593](https://arxiv.org/abs/1806.09593) -- both, apparently, unpublished) <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/14">v14</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    added pointer to the thesis

    • Martin Lundfall, Models of linear dependent type theory, 2017 (pdf)

    (which became the preprint Lundfall 18, arXiv:1806.09593 – both, apparently, unpublished)

    diff, v14, current

77. • CommentRowNumber77.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 25th 2022
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexProvided links to slides at [Bounded Linear Logic Workshop](https://www.cs.bham.ac.uk/~drg/bll.html). <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/19">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/19">v19</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    Provided links to slides at Bounded Linear Logic Workshop.

    diff, v19, current

78. • CommentRowNumber78.
    • CommentAuthorUrs
    • CommentTimeSep 14th 2022
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded pointer to: * [[Mitchell Riley]], *Linear Homotopy Type Theory*, HoTTEST talk (Jan 2022) &lbrack;[pdf](https://www.uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Riley-2022-01-20-HoTTEST.pdf)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/20">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/20">v20</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    added pointer to:

    • Mitchell Riley, Linear Homotopy Type Theory, HoTTEST talk (Jan 2022) [pdf]

    diff, v20, current

79. • CommentRowNumber79.
    • CommentAuthorUrs
    • CommentTimeSep 14th 2022
    • (edited Sep 14th 2022)
    • PermaLink
    Author: Urs
    Format: MarkdownItexexpanded out more details: *** * [[Mitchell Riley]], *Linear Homotopy Type Theory*, talk at: [HoTTEST Event for Junior Researchers 2022](https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_junior_2022.html) (Jan 2022) &lbrack;slides: [pdf](https://www.uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Riley-2022-01-20-HoTTEST.pdf), video: [YT](https://www.youtube.com/watch?v=o2oWhHabjdM)&rbrack; > **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. <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/20">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/20">v20</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    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.

    diff, v20, current

80. • CommentRowNumber80.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 14th 2022
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexMitchell's at your Center now? I wonder what he thinks of that series of semi-thoughts I had on [Twitter](https://twitter.com/DavidCorfield8/status/1222144464908619776) and at the [nForum](https://nforum.ncatlab.org/discussion/7830/linear-logic/?Focus=102311#Comment_102311). Thought I was glimpsing something.

    Mitchell’s at your Center now? I wonder what he thinks of that series of semi-thoughts I had on Twitter and at the nForum. Thought I was glimpsing something.

81. • CommentRowNumber81.
    • CommentAuthorUrs
    • CommentTimeSep 14th 2022
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, most [CQTS researchers](https://ncatlab.org/nlab/show/Center+for+Quantum+and+Topological+Systems#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](https://ncatlab.org/nlab/show/Center+for+Quantum+and+Topological+Systems#InitialResearcherMeeting-Schreiber), 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.

    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.

82. • CommentRowNumber82.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 15th 2022
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOne 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](https://arxiv.org/abs/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).

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

83. • CommentRowNumber83.
    • CommentAuthorUrs
    • CommentTimeSep 15th 2022
    • PermaLink
    Author: Urs
    Format: MarkdownItexThat seems to have an obvious answer: Yes, worth exploring. :-) First thing we are aiming at (as laid out in my [PlanQC talk](https://ncatlab.org/schreiber/show/Topological+Quantum+Programming+in+TED-K#video) today) is implementing the dependent type family of $\mathfrak{su}(2)_k$-conformal blocks into Agda. The formula laid out [here](https://ncatlab.org/schreiber/show/Topological+Quantum+Programming+in+TED-K#GMConAbs) 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.

    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.

84. • CommentRowNumber84.
    • CommentAuthorUrs
    • CommentTimeSep 17th 2022
    • (edited Aug 25th 2023)
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded pointer to: * [[Mitchell Riley]], *A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory*, PhD Thesis (2022) &lbrack;[ir:3269](https://digitalcollections.wesleyan.edu/object/ir%3A3269)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/21">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/21">v21</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    added pointer to:

    • Mitchell Riley, A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis (2022) [ir:3269]

    diff, v21, current

85. • CommentRowNumber85.
    • CommentAuthorperezl.alonso
    • CommentTimeAug 25th 2023
    • PermaLink
    Author: perezl.alonso
    Format: MarkdownItexRe #84: doi now redirects to some [chemistry thesis](https://digitalcollections.wesleyan.edu/islandora/development-automated-fitnmr-analytical-peak-modeling-and-investigation-miniprotein) from just this past May. Seems, at least according to the uni webpage, both have the same doi.

    Re #84: doi now redirects to some chemistry thesis from just this past May. Seems, at least according to the uni webpage, both have the same doi.

86. • CommentRowNumber86.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023
    • (edited Aug 25th 2023)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks for pointing this out. A related glitch happened before, some months back, when the DOI would be a dead link. Back then I had emailed some web-host who responded by asking for patience until some server migration was completed, and indeed the problem was fixed a few days later. But now it looks like that previous glitch may have caused the same DOI to be re-used.

    Thanks for pointing this out. A related glitch happened before, some months back, when the DOI would be a dead link. Back then I had emailed some web-host who responded by asking for patience until some server migration was completed, and indeed the problem was fixed a few days later. But now it looks like that previous glitch may have caused the same DOI to be re-used.

87. • CommentRowNumber87.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have emailed them again (`wesscholar@wesleyan.edu`). Let's hope this can still be fixed.

    I have emailed them again (wesscholar@wesleyan.edu). Let’s hope this can still be fixed.

88. • CommentRowNumber88.
    • CommentAuthorUrs
    • CommentTimeSep 1st 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexJust received a reply from `wesscholar@wesleyan.edu`: the link [doi:10.14418/wes01.3.139](https://doi.org/10.14418/wes01.3.139) has been fixed now.

    Just received a reply from wesscholar@wesleyan.edu: the link doi:10.14418/wes01.3.139 has been fixed now.

89. • CommentRowNumber89.
    • CommentAuthorUrs
    • CommentTimeOct 8th 2023
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded publication data for: * [[Neelakantan Krishnaswami]], [[Pierre Pradic]], [[Nick Benton]], *Integrating Dependent and Linear Types*, ACM SIGPLAN Notices **50** 1 (2015) 17–30 &lbrack;[pdf](https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf),[doi:10.1145/2775051.2676969](https://doi.org/10.1145/2775051.2676969)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/35">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/35">v35</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    added publication data for:

    • Neelakantan Krishnaswami, Pierre Pradic, Nick Benton, Integrating Dependent and Linear Types, ACM SIGPLAN Notices 50 1 (2015) 17–30 [pdf,doi:10.1145/2775051.2676969]

    diff, v35, current

90. • CommentRowNumber90.
    • CommentAuthorUrs
    • CommentTimeOct 8th 2023
    • (edited Oct 8th 2023)
    • PermaLink
    Author: Urs
    Format: MarkdownItexadded pointer also to * [[Conor McBride]], *I Got Plenty o’ Nuttin’*, in: *A List of Successes That Can Change the World*, Lecture Notes in Computer Science **9600**, Springer (2016) &lbrack;[doi:10.1007/978-3-319-30936-1_12](https://doi.org/10.1007/978-3-319-30936-1_12)&rbrack; and fixed up a bunch of other references that were added by others in the past, restoring chronological order <a href="https://ncatlab.org/nlab/revision/diff/dependent+linear+type+theory/36">diff</a>, <a href="https://ncatlab.org/nlab/revision/dependent+linear+type+theory/36">v36</a>, <a href="https://ncatlab.org/nlab/show/dependent+linear+type+theory">current</a>

    added pointer also to

    • Conor McBride, I Got Plenty o’ Nuttin’, in: A List of Successes That Can Change the World, Lecture Notes in Computer Science 9600, Springer (2016) [doi:10.1007/978-3-319-30936-1_12]

    and fixed up a bunch of other references that were added by others in the past, restoring chronological order

    diff, v36, current

91. • CommentRowNumber91.
    • CommentAuthorpatrick_nicodemus1
    • CommentTimeMar 4th 2024
    • PermaLink
    Author: patrick_nicodemus1
    Format: TextI do not understand why the paper "Framed bicategories and monoidal fibrations" by Michael Shulman is linked here. Can somebody edit this post to add an explanation or delete the source if it is inappropriate?

    I do not understand why the paper "Framed bicategories and monoidal fibrations" by Michael Shulman is linked here. Can somebody edit this post to add an explanation or delete the source if it is inappropriate?
92. • CommentRowNumber92.
    • CommentAuthorUrs
    • CommentTimeMar 4th 2024
    • PermaLink
    Author: Urs
    Format: MarkdownItexIndexed monoidal categories as intended semantics for dependent linear types is discussed in the section "Semantics".

    Indexed monoidal categories as intended semantics for dependent linear types is discussed in the section “Semantics”.

93. • CommentRowNumber93.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 25th 2024
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRegarding #79 and its mention of 'synthetic stable homotopy theory', presumably the idea here is to prove theorems in linear HoTT which will then be true in every tangent $\infty$-topos. Can we think of some nice low-hanging fruit as targets for this synthetic stable homotopy theory? Say might we expect some kind of general linear representation theory?

    Regarding #79 and its mention of ’synthetic stable homotopy theory’, presumably the idea here is to prove theorems in linear HoTT which will then be true in every tangent $\infty$-topos. Can we think of some nice low-hanging fruit as targets for this synthetic stable homotopy theory?

    Say might we expect some kind of general linear representation theory?