Exponent of category T is YT which represents mapping from T to Y:
T -> Y
So a mapping from one category to another has properties similar to exponent, for instance in the following mapping from set to set:
Example in Set
|If we are mapping from set T to set Y and the number of elements in T is t and the number of elements in Y is y then the number of mappings from T to Y is yt.|
This also behaves like an exponent in that YA * YB = YA+B. That is, if we have 3 categories, one of which is the sum of the other 2, each has a mapping to a 4th category then these mappings will be a product. See diagram on left:
For a generalistion of this see Yoneda embedding.
In propositional logic there is a rule called 'modus ponens':
That is: if 'B implies A' and 'B' is true then A is true.
This has a similar form to this functor:
ε: AB × B -> A
In this case we will call ε 'evaluation'.
Alternativly, for any object C:
f: C × B -> A
there is a unique arrow:
f': C -> AB
The relationship between ε, f and f' is:
ε•(f' × 1B) = f
This is represented by the following diagram:
Relation to Internal Hom-set
An internal hom-set in a cartesian closed category is an exponential object.