Exponential in a presheaf category

ID: exponential-in-a-presheaf-category

For categorical presheaves on a small category, restrictions in the displayed exponential object act by precomposition with . Evaluation sends at to . The currying of sends to the natural transformation whose value on is . Evaluation and currying are inverse and natural, proving the Cartesian closed category structure.

New to topics? Read the docs here!