<p>Take any small symmetric monoidal category <span class="math-container">$V$</span>.</p>
<p>Then the category of <span class="math-container">$V$</span>-valued presheaves will (a) have closed monoidal structure (via <a href="https://ncatlab.org/nlab/show/Day+convolution" rel="nofollow noreferrer">Day convolution</a>), and (b) have enough stuff (inherited from <span class="math-container">$\mathrm{Set}$</span>) to interpret dependent types.  This gives you enough structure to interpret something like our LNL calculus pretty easily, because there is a nice adjunction between <span class="math-container">$\mathrm{Set}$</span> and this category given by the constant functor (<span class="math-container">$F(X) = V \mapsto X$</span>) and the global elements functor (<span class="math-container">$G(A) = \Pi X : Obj(V). A_X$</span>).</p>
<p>Matthijs Vakar wrote a nice paper, <a href="https://link.springer.com/content/pdf/10.1007/978-3-662-46678-0_7.pdf" rel="nofollow noreferrer"><em>A Categorical Semantics for Linear Logical Frameworks</em></a>, which describes the categorical models of this style of calculus in detail.</p>

CC BY-SA 4.0
2021-01-26T22:35:13.487Z
Thanks! Unfortunately, I cannot think of any interesting and small monoidal categories yet. What about locally small monoidal categories? Will we run into issues here?
xrq
CC BY-SA 4.0
2021-01-27T22:50:03.557Z
It will work, modulo some faff with universe levels.
Neel Krishnaswami
CC BY-SA 4.0
2024-11-02T19:26:33.440Z
why limit to *symmetric* monoidal?
Max New
CC BY-SA 4.0
2024-11-04T15:00:38.077Z
@MaxNew Because that's what the question asked. But once you get your dependently-typed Lambek-style parsing stuff sorted out, shoot me a line!
Neel Krishnaswami
CC BY-SA 4.0
2021-01-26T22:31:42.543Z
2021-01-27T22:48:19.657Z
2021-01-27T22:48:19.657Z
Neel Krishnaswami
<p>Dependent-linear type theories may be a functional programmer's dream, but is it categorically interesting, i.e. is it the internal language of an &quot;interesting&quot; category? By &quot;interesting&quot;, I mean a category that arises naturally in mathematics or computer science, similar to how intuitionistic type theory is the internal logic of toposes or linear logic is the internal logic of <span class="math-container">$\mathbf{PShMod}_X$</span>, which is ubiquitous in algebraic geometry. In other words, can we give an interesting and &quot;natural&quot; categorical model of a dependent-linear type theory?</p>
<p>Any (reasonable) flavor of dependent-linear type theory is fine, as long as it has a linear layer and a dependent layer. Examples include Atkey's quantitative type theory and Krishnaswami, Pradic &amp; Benton's <a href="https://cl.cam.ac.uk/%7Enk480/dlnl-paper.pdf" rel="noreferrer">dependent-linear calculus</a> (POPL '15).</p>
<p>(Sorry, but I don't know whether this site or MathOverflow would be a better forum for this question. But it seems that I might attract more experts on this site...)</p>

<type-theory><ct.category-theory><dependent-type>
"Interesting" categories whose internal logic is a dependent-linear type theory
xrq
# "Interesting" categories whose internal logic is a dependent-linear type theory

(Asked by: username_0 on 2021-01-25)

Dependent-linear type theories may be a functional programmer's dream, but is it categorically interesting, i.e. is it the internal language of an "interesting" category? By "interesting", I mean a category that arises naturally in mathematics or computer science, similar to how intuitionistic type theory is the internal logic of toposes or linear logic is the internal logic of $\mathbf{PShMod}\_X$, which is ubiquitous in algebraic geometry. In other words, can we give an interesting and "natural" categorical model of a dependent-linear type theory?

Any (reasonable) flavor of dependent-linear type theory is fine, as long as it has a linear layer and a dependent layer. Examples include Atkey's quantitative type theory and Krishnaswami, Pradic & Benton's [dependent-linear calculus](https://cl.cam.ac.uk/%7Enk480/dlnl-paper.pdf) (POPL '15).

(Sorry, but I don't know whether this site or MathOverflow would be a better forum for this question. But it seems that I might attract more experts on this site...)

**Tags:** type-theory, ct.category-theory, dependent-type

---

## 1 answers

### Answer by username_1 on 2021-01-26. Score: 3

Take any small symmetric monoidal category $V$.

Then the category of $V$-valued presheaves will (a) have closed monoidal structure (via [Day convolution](https://ncatlab.org/nlab/show/Day+convolution)), and (b) have enough stuff (inherited from $\mathrm{Set}$) to interpret dependent types. This gives you enough structure to interpret something like our LNL calculus pretty easily, because there is a nice adjunction between $\mathrm{Set}$ and this category given by the constant functor ($F(X) = V \mapsto X$) and the global elements functor ($G(A) = \Pi X : Obj(V). A\_X$).

Matthijs Vakar wrote a nice paper, [*A Categorical Semantics for Linear Logical Frameworks*](https://link.springer.com/content/pdf/10.1007/978-3-662-46678-0_7.pdf), which describes the categorical models of this style of calculus in detail.

> **Comments:**
> **username_0**: Thanks! Unfortunately, I cannot think of any interesting and small monoidal categories yet. What about locally small monoidal categories? Will we run into issues here?  
> **username_1**: It will work, modulo some faff with universe levels.  
> **username_2**: why limit to *symmetric* monoidal?  
> **username_1**: @MaxNew Because that's what the question asked. But once you get your dependently-typed Lambek-style parsing stuff sorted out, shoot me a line!  

---

