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

  • $\begingroup$ 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? $\endgroup$
    – xrq
    Jan 26, 2021 at 22:35
  • $\begingroup$ It will work, modulo some faff with universe levels. $\endgroup$ Jan 27, 2021 at 22:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.