= Currying adjunction for small categories
{title2=$-\times\mathcal C\dashv[\mathcal C,-]$}
A <functor> $\mathcal D\times\mathcal C\to\mathcal E$ is uniquely a <functor> $\mathcal D\to[\mathcal C,\mathcal E]$: 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.
Back to article page
