### 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.