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

1 Answer

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.

• 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 Jan 26 at 22:35
• It will work, modulo some faff with universe levels. – Neel Krishnaswami Jan 27 at 22:50