nLab doubly closed monoidal category

Idea

Generally, by a “doubly closed monoidal category” one may mean a category equipped with not just one but two different closed monoidal category-structures [O’Hearn & Pym (1999), §3; O’Hearn (2003), §2.2].

A common and relevant special case is that of a cartesian closed category which is equipped with further non-cartesian closed monoidal category-structure, in which case one may speak of cartesian doubly closed monoidal categories [O’Hearn & Pym (1999), §3; Jeltsch (2016), Def. 3]. Yet more specially, if the underlying category is a topos one may speak of a (doubly) monoidal topos (see there for more).

Examples of doubly closed monoidal categories commonly arise as “parameterized” generalizations of plain closed monoidal categories. For example, categories VectBund of finite rank vector bundles over base spaces taken from convenient categories of topological spaces (or just over Sets), whose morphisms admit base change, are cartesian doubly closed monoidal with the further non-cartesian tensor product being the external tensor product of vector bundles. In the same vein, tangent $\infty$-toposes of parameterized (module-)spectra form cartesian doubly closed monoidal $\infty$-categories (and in fact doubly monoidal $\infty$-toposes).

By the general relation between category theory and type theory, the internal language of such cartesian double closed monoidal categories is a combination of classical (intuitionistic) type theory for the cartesian closed fragment, and some kind of linear type theory for the non-cartesian closed fragment: Where a context in intuitionistic type theory is an iterated cartesian (dependent) product type $(-)\times (-)$ and a context in linear type theory is an iterated multiplicative conjunction $(-) \otimes (-)$, so a context in the internal language of cartesian doubly monoidal categories is obtained as an alternation of these two construction principles, forming a tree with nodes or “bunches” labeled either “$\times$” or “$\otimes$” — this is the topic of bunched type theory.

Related concepts

• closed monoidal category

• doubly monoidal topos

• bunched type theory

References

Discussion of doubly closed monoidal categories as categorical semantics for bunched logic/bunched type theory:

• Peter O'Hearn, David J. Pym, §3 in: The Logic of Bunched Implications, The Bulletin of Symbolic Logic 5 2 (1999) 215-244 [pdf, doi:10.2307/421090]

• Peter O'Hearn, §2.2 in: On bunched typing, Journal of Functional Programming 13 4 (2003) 747-796 [doi:10.1017/S0956796802004495]

• Wolfgang Jeltsch, Abstract categorical semantics for resourceful functional reactive programming, Elsevier Journal of Logical and Algebraic Methods in Programming 85 6 (2016) 1177-1200 [doi:10.1016/j.jlamp.2016.07.001]

Discussion of cartesian doubly closed monoidal $\infty$-categories of parameterized (module-)spectra as categorical semantics of bunched linear homotopy type theory:

• Mitchell Riley, A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis (2022) [doi:10.14418/wes01.3.139, ir:3269, pdf]