With duals for objects
With duals for morphisms
Special sorts of products
In higher category theory
A cartesian closed functor is a functor between cartesian closed categories which preserves both products and exponential objects/internal homs (all the structure of cartesian closed categories).
More precisely, if preserves products, then the canonical morphisms (for all objects ) are isomorphisms, and we therefore have canonical induced morphism — the adjuncts of the composite . is cartesian closed if these maps are also isomorphisms.
The above natural transformation is the mate of the exponential comparison natural transformation under the composite adjunctions
This is called the Frobenius reciprocity law. It is discussed, for instance, as (Johnstone, lemma 1.5.8). More generally for closed monoidal categories (not necessarily cartesian monoidal) it is discussed in “Wirthmüller contexts” in
Let still and be as above.
For instance (Johnstone, corollary A1.5.9).
The functor has a left adjoint
given by postcomposition with (the dependent sum along ). Therefore by prop. 1 it is sufficient to show that for all in and that
in . But this is the pasting law for pullbacks in , which says that the two consecutive pullbacks on the left of
are isomorphic to the direct pullback along the composite on the right.
For instance section A1.5 of
- H. Fausk, P. Hu, Peter May, Isomorphisms between left and right adjoints, Theory and Applications of Categories , Vol. 11, 2003, No. 4, pp 107-131. (TAC, pdf)