nLab doubly closed monoidal category

Contents

Context

Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

Contents

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.

References

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

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.