"Interesting" categories whose internal logic is a dependent-linear type theory

Question

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

Answer 1

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.