category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
monoidal dagger-category?
A cartesian closed category (sometimes: ccc) is a category with finite products which is closed with respect to its cartesian monoidal structure.
The internal hom $[S,X]$ in a cartesian closed category is often called exponentiation and is denoted $X^S$.
A cartesian closed functor between cartesian closed categories $C$, $D$ is a functor $F \colon C \to D$ that is product-preserving and that is also exponential-preserving, meaning that the canonical map
corresponding to the composite
is an isomorphism.
Any topos or quasitopos, such as Set, is cartesian closed.
See also closed monoidal structure on presheaves.
Cat is also cartesian closed.
Many nice categories of topological spaces are also cartesian closed, particularly the convenient categories of spaces.
A category is cartesian closed if it has finite products and if for any two objects $X$, $Y$, there is an object $Y^X$ (thought of as a “space of maps from $X$ to $Y$”) such that for any object $Z$, there is a bijection between the set of maps $Z \to Y^X$ and the set of maps $Z \times X \to Y$, and this bijection is natural in $Z$.
There is an evaluation map $ev_{X, Y}: Y^X \times X \to Y$, which by definition is the map corresponding to the identity map $Y^X \to Y^X$ under the bijection. Using the naturality, it may be shown that the bijection $\hom(Z, Y^X) \to \hom(Z \times X, Y)$ takes a map $\phi: Z \to Y^X$ to the composite
and the universal property of $Y^X$ may be phrased thus: given any $\psi: Z \times X \to Y$, there exists a unique map $\phi: Z \to Y^X$ for which $\psi = ev_{X, Y} \circ (\phi \times 1_X)$.
Taking $Z = 1$ (the terminal object), maps $1 \to Y^X$ (or “points” of $Y^X$) are in bijection with maps $X \stackrel{\pi_{2}^{-1}}{\to} 1 \times X \to Y$. So the “underlying set” of $Y^X$, namely $\hom(1, Y^X)$, is identified with the set of maps from $X$ to $Y$. Let us denote the point corresponding to $f: X \to Y$ by $[f]: 1 \to Y^X$. Then, by definition,
The following lemma says that the internal evaluation map $ev_{X, Y}$ indeed behaves as an evaluation map at the level of underlying sets.
Given a map $f: X \to Y$ and a point $x: 1 \to X$, the composite
is the point $f x: 1 \to Y$.
We have
where the penultimate equation uses naturality of the projection map $\pi_2$.
Internal composition $c_{X, Y, Z}: Z^Y \times Y^X \to Z^X$ is the unique map such that
One may show that internal composition behaves as the usual composition at the underlying set level, in that given maps $g: Y \to Z$, $f: X \to Y$, we have
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.
In showing that a given category is cartesian closed, the following theorem is often useful (cf. A4.3.1 in the Elephant):
If $C$ is cartesian closed, and $D\subseteq C$ is a reflective subcategory, then the reflector $L\colon 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.
The following observation was taken from a post of Mike Shulman at MathOverflow.
If $\mathcal{C}$ is small and $\mathcal{D}$ is complete and cartesian closed, then $\mathcal{D}^{\mathcal{C}}$ is also complete and cartesian closed. Completeness is clear since limits in $D^C$ are computed pointwise. As for cartesian closure, we can compute exponentials in essentially the same way as for presheaves, motivated by $\mathcal{D}$-enriched category theory:
Then we can compute
Here the antepenultimate step uses the co-Yoneda lemma. This appears to involve colimits in $\mathcal{D}$ as well, but the existence of these colimits is not actually an extra assumption: the co-Yoneda lemma tells us that $\int^{x\in \mathcal{C}} \sum_{\mathcal{C}(x,y)} H(x)$ exists and is isomorphic to $H(y)$.
Similarly, the above argument can be interpreted to say that even if $\mathcal{D}$ is not complete, then the exponential $G^F$ in $\mathcal{D}^{\mathcal{C}}$ exists if and only if the particular limits above exist, and in that case they are isomorphic.
A more abstract argument using comonadicity and the adjoint triangle theorem, which also applies to locally cartesian closed categories, can be found in Theorem 2.12 of
and is reproduced in the setting of closed monoidal categories at closed monoidal category.
Let $C$ be a cartesian closed category, and $c$ an object of $C$. Then the Kleisli category of the comonad $c \times - \colon C \to C$, denoted $C[c]$, is also a cartesian closed category.
The Kleisli category of the comonad $c \times -$ on $C$ is canonically equivalent to the Kleisli category of the monad $(-)^c$ on $C$.
of Theorem 2
Let $a$ and $b$ be objects of $C[c]$. Claim: the product $a \times b$ in $C$, considered as an object of $C[c]$, is the product of $a$ and $b$ in $C[c]$, according to the following series of natural bijections:
Claim: the exponential $a^b$ in $C$, considered as an object of $C[c]$, is the exponential of $a$ and $b$ in $C[c]$, according to the following series of natural bijections:
where in the last step, we used the prior claim that the product of objects in $C$, when viewed as an object of $C[c]$, gives the product in $C[c]$.
Observe that the object $c$ in $C[c]$ has an element $e \colon 1 \to c$, corresponding to the canonical isomorphism $c \times 1 \cong c$ in $C$. We call this element the “generic element” of $c$ in $C[c]$, according to the following theorem. This theorem can be viewed as saying that in the doctrine of cartesian closed categories, $C[c]$ is the result of freely adjoining an arrow $1\to c$ to $C$.
(Functional completeness)
Let $C$ and $D$ be cartesian closed categories, and let $F \colon C \to D$ be a cartesian closed functor. Let $c$ be an object of $C$, and let $t: F(1) \to F(c)$ be an element in $D$. Then there exists an extension of $F$ to a cartesian closed functor $\tilde{F} \colon C[c] \to D$ that takes the generic element $e \colon 1 \to c$ in $C[c]$ to the element $t$, and this extension is unique up to isomorphism.
On objects, $\tilde{F}(a) = F(a)$. Let $f \colon a \to b$ be a map of $C[c]$, i.e., let $g \colon c \times a \to b$ be the corresponding map in $C$, and define $\tilde{F}(f)$ to be the composite
It is straightforward to check that $\tilde{F}$ is a cartesian closed functor and is, up to isomorphism, the unique cartesian closed functor taking $e$ to $t$.
cartesian closed category, locally cartesian closed category
cartesian closed model category, locally cartesian closed model category
cartesian closed (∞,1)-category locally cartesian closed (∞,1)-category