# $\beta$ reduction equational equality

In Categories, Types and Structures, authors talk about exponential objects in section 2.3.1.

Let $$C$$ be a Cartesian category, and $$a,b \in Ob_C$$. The exponent of $$a$$ and $$b$$ is an object $$b^a$$ together with a morphism $$eval_{alb}: b^a \times a\rightarrow b$$ (evaluation map), and for every object $$c$$ an operation $$\Lambda_c : C[c\times a,b]\rightarrow C[c, b^a]$$ such that for all morphisms $$f: c\times a\rightarrow b$$, $$h:c\rightarrow b^a$$, the following equation holds:
$$\beta. eval_{a,b} \circ (\Lambda (f)\times id_a )=f$$
$$\eta. \Lambda_c(eval_{a,b}\circ(h\times id_a))=h$$

Can you please show me the steps to derive the last two equations?

• This is a (possible) definition of an exponential object; what do you want to prove exactly?
– cody
Jul 22, 2022 at 20:15

## 1 Answer

The following morphism and commuting morphisms explain why those two equations hold:

$$h:c\rightarrow b^a$$

commuting morphisms:

$$eval: b_a\times a\rightarrow b$$
$$f:c\times a\rightarrow b$$
$$h\times id: c\times a\rightarrow b^a\times a$$