# 1 Exponential object

In a category $$\cC$$ with binary products, an exponential object from $$A$$ to $$B$$ is a universal morphism $$(B^A, B^A \times A \xto{\epsilon_A} B)$$ from $$(-) \times A$$ to $$B$$.

$\begin{array}{rlclll} \text{exponential:} & (B^A, B^A \times A \xto{\epsilon_A} B) & \equiv & \forall f: C \times A \to B. & \exists! \hat{f}: C \to B^A. & f = \epsilon_A \compL (\hat{f} \times \id_A). \end{array}$

• $$\epsilon_A: B^A \times A \to B$$ is called evaluation
• $$\hat{f}: C \to B^A$$ is called the exponential transpose of $$f: C \times A \to B$$
• $$\bar{g}: C \times A \to B := \epsilon_A \compL (g \times \id_A)$$ is the exponential transpose of $$g: C \to B^A$$

$(-) \times A \adj (-)^A$

$\Hom(C \times A, B) \iso \Hom(C, B^A)$

-- function application
(\$) :: (a -> b) -> a -> b
-- reverse function application
(&) :: a -> (a -> b) -> b

A cartesian closed category has all finite products and exponentials.

In a cartesian closed category, the functor $$(-) \times A$$ is a left adjoint, which necessarily preserves all colimits, including all coproducts.

$$\Hom(A, B) \iso \Hom(1, B^A) \iso \Hom(0, B^A)$$ All objects are isomorphic.

# 2 Composition

$A \xto{f} B \xto{g} C \xto{h} D$

## 2.1 Composition

$\compL: C^B \times B^A \to C^A$

-- function composition
(.) :: (b -> c) -> (a -> b) -> (a -> c)

## 2.2 Postcomposition

$h^B: C^B \to D^B := h \compL (-)$

\begin{aligned} \begin{array}{cccc} (-)^B: & \cC & \to & \cC \\ & C & \mapsto & C^B \\ & C \xto{h} D & \mapsto & C^B \xto{h^B} D^B \end{array} \end{aligned}

## 2.3 Precomposition

$C^f: C^B \to C^A := (-) \compL f$

\begin{aligned} \begin{array}{cccc} C^{(-)}: & \cC\op & \to & \cC \\ & B & \mapsto & C^B \\ & B \xto{f\op} A & \mapsto & C^B \xto{C^f} C^A \end{array} \end{aligned}

# 3 Transpose

## 3.1 Partial application

$\partf: C^{A \times B} \times A \to C^B$

## 3.2 Currying and uncurrying

$\curry: C^{A \times B} \iso (C^B)^A :\curry\inv$

$\Hom(A \times B, C) \iso \Hom(A, C^B)$

curry   :: ((a, b) -> c) -> a -> b -> c
uncurry :: (a -> b -> c) -> (a, b) -> c 

# 4 Product

## 4.1 Product codomain

$\angles{p_1^A, p_2^A}: (B \times C)^A \iso B^A \times C^A$

$\Hom(A, B \times C) \iso \Hom(A, B) \times \Hom(A, C)$

## 4.2 Coproduct domain

$\angles{C^{i_1}, C^{i_2}}: C^{A + B} \iso C^A \times C^B$

$\Hom(A + B, C) \iso \Hom(A, C) \times \Hom(B, C)$

# 5 Locally cartesian closed category

A locally cartesian closed category $$\cC$$ is a category such that every slice category $$\cC \comma C$$ is cartesian closed.

A slice category $$\cC \comma C$$ of a locally cartesian closed category $$\cC$$ is locally cartesian closed.

A slice of a slice $$(\cC \comma C) \comma (A \xto{a} C)$$ is isomorphic to a slice $$\cC \comma A$$.

A locally cartesian closed category $$\cC$$ with a terminal object $$1$$ is cartesian closed and finitely complete.

Exponentials in $$\cC \comma 1$$ are exponentials in $$\cC$$. Products in $$\cC \comma C$$ are pullbacks in $$\cC$$. Pullbacks and a terminal object imply all finite limits.