"Interesting" categories whose internal logic is a dependent-linear type theory 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 $\mathbf{PShMod}_X$, 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?
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 dependent-linear calculus (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...)
Take any small symmetric monoidal category $V$.
Then the category of $V$-valued presheaves will (a) have closed monoidal structure (via 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, which describes the categorical models of this style of calculus in detail.