Currying adjunction for small categories

ID: currying-adjunction-for-small-categories

A functor is uniquely a functor : fix its first coordinate and use its first-coordinate arrows as natural transformations. Uncurrying evaluates those transformations and second-coordinate arrows. The adjunction unit inserts a fixed first coordinate, and the adjunction counit is evaluation. This makes the category of small categories cartesian closed.

New to topics? Read the docs here!