nLab cartesian closed 2-category



2-category theory

Limits and colimits



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 AA, BB in \mathcal{B}, there is an exponential object B AB^A, an evaluation 1-morphism, eval A,B:B A×ABeval_{A, B}: B^A \times A \to B, and for every XX an adjoint equivalence between (X,B A)\mathcal{B}(X, B^A) and (X×A,B)\mathcal{B}(X \times A, B).

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



The following 2-categories are cartesian closed:


  • 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:

Discussion of the example of generalised species:

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

Last revised on November 1, 2022 at 22:17:06. See the history of this page for a list of all contributions to it.