With braiding
With duals for objects
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
With duals for morphisms
monoidal dagger-category?
With traces
Closed structure
Special sorts of products
Semisimplicity
Morphisms
Internal monoids
Examples
Theorems
In higher category theory
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.
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:
Last revised on April 19, 2023 at 08:08:51. See the history of this page for a list of all contributions to it.