For the presheaf category, define the exponential in a presheaf category by
For , its restriction sends to . Composition of these restriction maps follows from composition of the , so this is a categorical presheaf. Define evaluation map of an exponential object by
For , naturality of gives
Thus is a natural transformation.
Given a natural transformation , define its currying by
Naturality of proves that is a natural transformation . For , the same formula proves that is natural. Evaluating at gives .
Conversely, if and , then
by naturality of . Hence the two constructions are inverse and natural in . Products are available pointwise, including the terminal singleton presheaf, so the presheaf category is Cartesian closed. The exponential uses natural transformations out of ; simply exponentiating the individual values generally does not give this object.

Articles by others on the same topic (0)

There are currently no matching articles.