nLab
cartesian closed category

Definition

A cartesian closed category (sometimes: ccc) is a category with finite products which is closed with respect to its cartesian monoidal structure.

Examples

• Any topos or quasitopos, such as Set, is cartesian closed.

• Cat is also cartesian closed.

• Many nice categories of topological spaces are also cartesian closed, particularly the convenient categories of spaces.

Inheritance by reflective subcategories

In showing that a given category is cartesian closed, the following theorem is often useful (cf. A4.3.1 in the Elephant):

Theorem

If $C$ is cartesian closed, and $D\subseteq C$ is a reflective subcategory, then the reflector $L:C\to D$ preserves finite products if and only if $D$ is an exponential ideal (i.e. $Y\in D$ implies $Y^X\in D$ for any $X\in C$). In particular, if $L$ preserves finite products, then $D$ is cartesian closed.

Remarks

• In a cartesian closed category, the product functors $A\times -$ have right adjoints, so they preserve all colimits. In particular, a cartesian closed category that has finite coproducts is a distributive category.

• The internal logic of cartesian closed categories is the typed lambda-calculus?.