Exponentation and Cartesian Closed Categories

We begin by studying $ Set $. For two objects, $ A $ and $ B $, we have the set $$ B^A = \{ f : A \rightarrow B \} $$ of size $$ |B|^{|A|} $$ We can shortly reason about this. Say we have the objects given as $$ A = \{ a,b,c \} $$ and $$ B = \{ 1,2 \} $$ OK. The element $ a \in A $ can map to either $ 1 $ or $ 2 $. For each choice $ b \in A $ has the same two possible targets. Hence we have $ 2 \cdot 2 \cdot 2 $ choices in total.

We want to charectarize $ B^A $ in terms of arrows instead of elements. Now observe this special evaluation function $$ eval : (B^A \times A) \rightarrow B $$ given as $$ eval(f,a) = f(a) $$ Given $ f : A \rightarrow B $ and $ a \in A $ we have that $ f(a) \in B $. Given some function $$ g : (C \times A) \rightarrow B $$ we have exactly one function $$ curry(g) : C \rightarrow B^A $$ Such that $$ eval \circ (curry(g),id_A) = g $$ This $ curry $ function is just one that applies an argument, $ c $, to a function $ g $. This concept is known from functional programming languages where a function with more than one argument applies them one at a time, and then returns a new function. That is it is given by $$ curry(g)(c) = g_c $$ We can prove the above. Let $ c \in C,a \in A, f : A \rightarrow B \in B^A $. Now $$ (eval \circ (curry(g),id_A ))(c,a) = eval(g_c,a) = g(c,a) $$

Definition - Exponential Object

Now. Let $ \mathcal{C} $ a category with all binary products. Let $ A,B $ objects of $ \mathcal{C} $. An object $ B^A $ is an exponential object if there is an arrow $$ eval_{AB} : (B^A \times A) \rightarrow B $$ such that for any object $ C $ and arrow $ g : (C \times A) \rightarrow C $ there is a unique arrow $ curry(g) : C \rightarrow B^A $ such that $$ eval_{AB} \circ (curry(g) \times id_A) = g $$

If $ \mathcal{C} $ has an exponential $ B^A $ for every pair of objects $ A $ and $ B $, then $ \mathcal{C} $ is said to have exponentiation.

Definition - Cartesian Closed Category (CCC)

A $ \textbf{CCC} $ is a category with a terminal object, binary products and exponentiation.