For a locally small category , the covariant Yoneda lemma gives a bijection
natural in and the functor . The inverse sends to the natural transformation whose component at maps to . Naturality of at forces this formula, proving both inverseness and uniqueness.
Write for the category of elements of . Its objects are with , and an arrow is an arrow satisfying .
Given an object of the slice category , define
An arrow acts by the restriction of ; naturality of makes this restriction well-defined. A slice morphism restricts to a map between the corresponding fibers and thus gives a natural transformation on .
Conversely, given , set
and let be projection to . The functor laws and naturality follow from those for and . On morphisms use the maps on each summand. Taking a fiber of this disjoint union recovers canonically. Taking the disjoint union of the fibers of recovers by , naturally in and in the slice object. These are inverse natural isomorphisms, proving
This is the slice of a set-valued functor category construction.
Now assume is a small category, so is small. Define a diagram in a category
For in , its reverse arrow acts by precomposition . There is a cocone to with component . To verify its colimit property directly, use pointwise colimits of sets. At , a colimit element has a representative , and the induced map to sends it to . This map is surjective, since is represented by . Moreover, the element-category arrow gives precisely the colimit relation
Thus all representatives with the same image are equal in the colimit, proving injectivity. The resulting bijections are natural in . We have proved the canonical colimit presentation of a covariant set-valued functor:
A Cartesian closed category has finite products in a category and an exponential object for each pair, representing maps from a product with . In , the terminal functor and binary products are computed pointwise. Define the exponential of covariant set-valued functors by
Smallness makes this a set. If , precomposition with defines . Functoriality is immediate from associativity of composition. Its evaluation map of an exponential object is
For , naturality of shows , which is exactly the naturality equation for evaluation.
Given , define its currying at by
Naturality of proves that this is a natural transformation in , and its compatibility with arrows proves that is natural. Evaluation recovers by setting . Conversely, for , its naturality implies
so currying the evaluation composite recovers . These formulas give the required natural bijection, hence is Cartesian closed.
Finally, for every the small category has a Cartesian closed functor category by the same construction. The slice equivalence above transports its terminal object, products and exponentials to . The original functor category also has pointwise finite limits. Therefore it is locally Cartesian closed. Every construction here is explicit; no adjoint functor theorem is used.