nLab cartesian closed 2-category

Idea

The notion of cartesian closed 2-category is the analog in 2-category theory (hence the categorification) of the notion of cartesian closed category in category theory:

A cartesian closed 2-category is a 2-category, $\mathcal{B}$, with finite products and a cartesian closed structure: For any $A$, $B$ in $\mathcal{B}$, there is an exponential object $B^A$, an evaluation 1-morphism, $eval_{A, B}: B^A \times A \to B$, and for every $X$ an adjoint equivalence between $\mathcal{B}(X, B^A)$ and $\mathcal{B}(X \times A, B)$.

The concept was introduced in (Makkai 96). There is no connection to the concept of cartesian bicategory.

Examples

{Examples}

The following 2-categories are cartesian closed:

• the 2-categories Cat($\mathcal{C}$) of internal categories or Grpd$(\mathcal{C})$ of internal groupoids internal to a cartesian closed category $\mathcal{C}$ (e.g. Niefield & Pronk 2019);

• the 2-category of generalized species (FGHW);

• the 2-category of cartesian distributors;

• the 2-category of coloured operads and bimodules.

Related concepts

• cartesian closed category

References

• Michael Makkai, Avoiding the axiom of choice in general category theory, Journal of Pure and Applied Algebra, 108(2):109 – 173, 1996.

On cartesian closed 2-categories of internal categories or internal groupoids:

• Susan B. Niefield, Dorette A. Pronk, Internal groupoids and exponentiability, Cahiers de topologie et géométrie différentielle catégoriques, LX 4 (2019) (pdf)

• Enrico Ghiorzi, Section 1.2 of: Complete internal categories (arXiv:2004.08741)

Discussion of the example of generalised species:

• M. Fiore, Nicola Gambino, Martin Hyland, G. Winskel, The cartesian closed bicategory of generalised species of structures, (pdf)

On the example of coloured operads:

• Nicola Gambino and André Joyal, On operads, bimodules and analytic functors, Vol. 249. No. 1184. American Mathematical Society, 2017.

Discussion of syntax for cartesian closed 2-categories in type theory:

• Marcelo Fiore, Philip Saville, A type theory for cartesian closed bicategories, (arXiv:1904.06538)

• Philip Saville, Cartesian closed bicategories: type theory and coherence, (PhD thesis, arXiv:2007.00624)