# 6.Exponentation and Cartesian Closed Categories

## 04.06.2020

### Contents/Index

1. Definition
2. Dual Category
3. Mono-, Epi- and Isomorphisms
4. Initial and Terminal Objects
5. Products and Coproducts
@6. 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.