0
$\begingroup$

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?

$\endgroup$
0
$\begingroup$

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$

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.